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

• Install: Add require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "LEAN_COPILOT_VERSION" to lakefile.lean and run lake update LeanCopilot.
• Prerequisites: Lean 4 v4.3.0-rc2 or later, Git LFS. Optional: CUDA/cuDNN for GPU acceleration. CMake >= 3.7 and C++17 compiler required for building Lean Copilot itself.
• Models: Run lake exe LeanCopilot/download to fetch built-in models.
• Docs: Getting Started

Highlighted Details

• Tactic suggestion with prefix filtering.
• Proof search combining LLM tactics with Aesop.
• Premise selection using LeanDojo's retriever.
• Supports custom LLM integration via TextToText and TextToVec interfaces.

Maintenance & Community

• Active development with contributions from Lean FRO members.
• Discussions hosted on GitHub Discussions. Bug reports via GitHub Issues.

Licensing & Compatibility

• MIT License. Compatible with commercial and closed-source projects.

Limitations & Caveats

• Native Windows support is not provided; WSL is recommended.
• Occasional Lean crashes may occur upon file edits/restarts, requiring a restart.
• Premise selection may retrieve semantically similar but not identical premises.
• search_proof can sometimes generate proofs with termination errors, potentially mitigated by renaming the theorem temporarily.