The LeanDojo team and California Institute of Technology have introduced Lean Co-pilot, a collaborative tool designed for LLM-human interaction to craft 100% accurate formal mathematical proofs. 

The innovative system utilises LLMs to suggest proof tactics within the Lean theorem prover, providing a seamless environment for human intervention and modification.

Click here to check out the GitHub repository.

The challenging landscape of automating theorem proving has long been hindered by the unreliability of current LLMs in mathematical and reasoning tasks, often prone to mistakes and hallucinations. Traditionally, mathematical proofs have predominantly relied on manual derivation, demanding meticulous verification.

Lean, a powerful theorem prover, excels at formal verification but poses a laborious task for humans when writing in Lean. Lean Co-pilot addresses this issue by leveraging LLMs to automate the suggestion of Lean proof tactics, significantly expediting proof synthesis. The system allows for human inputs only when necessary, offering a balanced collaboration between machine and human intellect.

Key features of Lean Co-pilot include LLM-driven suggestions for proof steps, searching for proofs, and selecting useful lemmas from an extensive mathematical library. The tool seamlessly integrates into Lean’s Visual Studio Code workflow, ensuring a user-friendly experience. 

Users can set up Lean Co-pilot as a Lean package, utilising built-in models from LeanDojo or incorporating custom models that can run locally or on the cloud.

LeanDojo, the platform supporting Lean Co-pilot, encourages accessibility by providing open-source models and tools under the MIT licence. The tool operates on various platforms, including Linux, macOS, and Windows WSL, with optional support for CUDA-enabled GPUs. 

Lean Co-pilot’s requirements include Git LFS, optional CUDA and cuDNN (recommended for GPU support), and CMake >= 3.7 along with a C++17 compatible compiler for building Lean Co-pilot itself.

Lean Co-pilot’s introduction aims to make LLMs more accessible to Lean users, fostering a positive feedback loop where proof automation contributes to enhanced data quality, ultimately driving improvements in LLMs for mathematical tasks.