lean-dojo/LeanCopilot

Lean Copilot – LLM‑powered proof assistance for Lean 4

What it is

• A library that lets you call large language models (LLMs) directly from Lean 4 code to automate theorem‑proving tasks.
• Provides three main tactics:
  1. suggest_tactics – generates a list of possible Lean tactics for the current goal.
  2. search_proof – combines LLM‑generated tactics with the aesop prover to search for a complete proof.
  3. select_premises – retrieves likely useful lemmas from a frozen snapshot of Lean 4 and Mathlib 4.
• Supports built‑in models hosted on Hugging Face (via CTranslate2) and any user‑provided model (local binary or remote server).

Why it matters

• Bridges symbolic theorem proving with modern neural language models, enabling faster proof development and experimentation.
• Works natively inside the Lean ecosystem, so you can keep the whole workflow in one place – no external scripts needed.
• Open‑source and accompanied by a peer‑reviewed paper (accepted to NeuS 2025).

Key components

Component	Role
NativeGenerator / NativeEncoder	Runs small transformer models locally via CTranslate2 (C++ library linked through Lean’s FFI).
ExternalGenerator / ExternalEncoder	Calls a model served elsewhere (e.g., a Python HTTP server) using a simple JSON API defined in external_model_api.yaml.
GenericGenerator / GenericEncoder	Lets you plug any Lean type that implements the generate / encode type‑class methods.
Lake integration	Provides a moreLinkArgs snippet and a require LeanCopilot entry so downstream packages can depend on it just like any other Lean library.
Dockerfile / build scripts	Ready‑made environment for Linux/macOS/WSL users who run into native‑dependency issues.

Getting started (quick steps)

1. Add the dependency to your lakefile.lean or lakefile.toml as shown in the README.
2. Run lake update LeanCopilot and then lake exe LeanCopilot/download to fetch the pre‑trained models (≈ 200 MiB each).
3. Build the native code with lake build (or lake build LeanCopilot if you haven’t imported it yet).
4. In a Lean file, import LeanCopilot and try:

   example (n m : Nat) : n + m = m + n := by
     suggest_tactics
   

   Click a suggested tactic to insert it, or run search_proof to let the system try a multi‑step proof automatically.

Advanced usage

• Adjust generation hyper‑parameters (temperature, beam size, number of returned tactics) via the suggest_tactics options documented in LeanCopilotTests/TacticSuggestion.lean.
• Swap the default model for a larger one by editing the ModelAPIs.lean examples and pointing ExternalGenerator at your own server.
• Skip building CTranslate2/OpenBLAS from source by supplying system library paths with Lake’s -KsystemOpenblas and -KsystemCtranslate2Lib flags.

Caveats to be aware of

• select_premises returns the original theorem name from the snapshot; some derived lemmas may appear under a different name.
• search_proof can occasionally produce a proof that fails termination checks; renaming the theorem temporarily works around this.
• On Linux, executables (lean_exe) that depend on Lean Copilot need an extra linker flag to pull in the system libstdc++ because Lean’s own binary links against libc++.

Community & support

• Discussions: https://github.com/lean-dojo/LeanCopilot/discussions
• Issues: open a GitHub issue with OS details, steps to reproduce, and debug logs.
• Contributions: pull requests are welcome; the project follows the usual Lean community conventions.

Citation If you use Lean Copilot in research, cite the accompanying paper:

@article{song2024leancopilot,
  title={Lean copilot: Large language models as copilots for theorem proving in lean},
  author={Song, Peiyang and Yang, Kaiyu and Anandkumar, Anima},
  journal={arXiv preprint arXiv:2404.12534},
  year={2024}
}

---

Lean Copilot makes LLMs first‑class citizens in the Lean theorem‑proving world, offering a practical bridge between neural language models and formal mathematics.