Copilot for theorem proving in Lean
Top 34.5% on sourcepulse
Lean Copilot integrates Large Language Models (LLMs) into the Lean theorem prover, enabling AI-assisted proof automation. It offers features like tactic suggestion, proof search, and premise selection, targeting Lean users seeking to enhance productivity and explore new proof strategies.
How It Works
Lean Copilot leverages LLMs via a Foreign Function Interface (FFI) for local execution and supports external model integration. It provides TextToText
generators for tactic suggestion/generation and TextToVec
encoders for premise retrieval. This dual approach allows for both efficient, locally-run models (via CTranslate2) and flexibility with custom or cloud-hosted LLMs.
Quick Start & Requirements
require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "LEAN_COPILOT_VERSION"
to lakefile.lean
and run lake update LeanCopilot
.lake exe LeanCopilot/download
to fetch built-in models.Highlighted Details
TextToText
and TextToVec
interfaces.Maintenance & Community
Licensing & Compatibility
Limitations & Caveats
search_proof
can sometimes generate proofs with termination errors, potentially mitigated by renaming the theorem temporarily.2 weeks ago
Inactive