Lean Copilot: LLMs as Copilots for Theorem Proving in Lean
A tool that lets large language models be used natively in Lean for proof automation, suggesting tactics and premises and searching for proofs, using built-in models from LeanDojo or a model the user supplies.
Lean Copilot allows large language models to be used natively in Lean for proof automation, including tactic and premise suggestion and proof search. It works with the project's own built-in models from LeanDojo or with models a user brings themselves, running either locally, with or without a GPU, or in the cloud.
It is added to a Lean project as a dependency in lakefile.lean or lakefile.toml, requiring a Lean version of at least v4.3.0-rc2. A downstream package normally downloads a prebuilt release of Lean Copilot rather than compiling it, except on platforms without a published release, such as Intel macOS, where it falls back to building from source using CMake and a C++17 compiler, plus Git LFS and, optionally, CUDA and cuDNN for GPU use.
The project's paper was accepted at the International Conference on Neuro-symbolic Systems (NeuS) 2025.