LeanCopilot: LLM Tactics Inside the Lean 4 Elaborator
LLMs as Copilots for Theorem Proving in Lean
At a glance
- What is it?
- LeanCopilot wires language models directly into Lean 4 proof automation through three tactics and a CTranslate2 inference backend. It is useful if you already have a Lean project and want tactic suggestions, aesop-driven proof search, or premise retrieval without leaving the editor.
- Who is it for?
- Adopt LeanCopilot if your project already pins a Lean version at or above v4.3.0-rc2 and you want tactic suggestions and aesop-backed proof search available as ordinary tactics rather than through an external script. Do not adopt it if you cannot accept Git LFS, a CTranslate2 shared library in your link arguments, or a premise retriever that only sees a fixed mathlib4 snapshot.
- Can I use it commercially?
- Yes. MIT is a permissive licence: you can use, modify and sell software built on it, as long as you keep its copyright and licence notices.
- Is it still maintained?
- Yes. The repository last received commits 1 day ago.
- What is it written in?
- Mainly C++, according to GitHub's language statistics.
Answers come from the project's GitHub data, last synced on September 15, 2026, and from our analysis. They are not legal advice.
DEEP OPEN-SOURCE ANALYSIS
The gap LeanCopilot fills between Lean 4 and an LLM
Lean 4 proofs are written in a language whose error messages are precise and whose search space is enormous. A user typing a proof state usually knows the shape of the goal but not which of the thousands of available lemmas will close it. LeanCopilot's premise is that this decision is exactly what a language model can help with, and that the help should arrive as a tactic inside the file rather than as a suggestion in a separate chat window. The README frames the goal plainly: it allows large language models to be used natively in Lean for proof automation, suggesting tactics and premises and searching for proofs. The audience is therefore narrow and specific. It is people who already write Lean, who have a project that builds with Lake, and who want model inference to appear in the same loop as elaboration. Someone who wants to query an LLM about mathematics in general is not the target, even though the README notes that the underlying inference machinery is not limited to theorem proving.
What is actually running: CTranslate2, three tactics, one retriever
The project is written primarily in C++ and links against CTranslate2, which is the inference engine doing the work. That choice explains the link arguments you must add to your Lake configuration, and it explains why the built-in models are distributed as CTranslate2 conversions rather than as raw PyTorch or GGUF weights. The built-in set is small and named by function: ct2-leandojo-lean4-tacgen-byt5-small generates tactics, ct2-leandojo-lean4-retriever-byt5-small and premise-embeddings-leandojo-lean4-retriever-byt5-small handle retrieval, and ct2-byt5-small appears as a base model. All four are downloaded from Hugging Face by a command rather than vendored in the repository. On top of that backend sit three tactics. suggest_tactics generates candidate tactics for the current goal and accepts a prefix such as simp to constrain generation. search_proof combines LLM-generated tactics with aesop to look for multi-tactic proofs, so the model proposes steps and aesop does the combinatorial search. select_premises retrieves potentially useful premises, and here the README is explicit about a constraint that matters: it uses the LeanDojo retriever to select premises from a fixed snapshot of Lean and mathlib4, pinned to a specific commit. The data flow is thus one-directional and stateless with respect to your project. Your goal state goes in, candidates come out, and nothing about your own definitions is indexed unless you replace the model.
Adding it to a Lake project: the four edits that matter
Integration happens through Lake, and the README gives the exact edits. First, add moreLinkArgs to your package configuration so the linker can find the CTranslate2 library: the value is a list containing -L./.lake/packages/LeanCopilot/.lake/build/lib and -lctranslate2. In lakefile.lean that goes inside the package block; in lakefile.toml the equivalent key is moreLinkArgs with the same two strings. Second, require the package from git at a pinned revision, where the README instructs you to set the version to a stable tag such as v4.33.0 for stable Lean, or to main for unstable Lean versions such as v4.34.0-rc1, and to check compatibility with other dependencies such as mathlib. Third, run lake update LeanCopilot, then lake exe LeanCopilot/download to fetch the models into ~/.cache/lean_copilot/, and finally lake build. Native Windows users have an extra step: add the project's .lake/packages/LeanCopilot/.lake/build/lib directory to the Path environment variable. Two prerequisites are easy to miss. Git LFS is listed as a requirement, and your project must use Lean at least v4.3.0-rc2. CMake 3.7 or newer and a C++17 compiler are only needed if you build LeanCopilot itself rather than consuming a prebuilt release, except on platforms with no published release, where the README says the build falls back to source automatically and therefore needs the toolchain anyway. Intel macOS is the example given.
Where the design costs you: version pinning and a frozen premise index
The most consequential limitation is stated in the README rather than hidden. select_premises retrieves from a fixed snapshot of Lean and mathlib4, pinned to one commit. If your project depends on a different mathlib revision, or on definitions that only exist in your own repository, the retriever cannot see them. It will return premises that exist in that snapshot, which may be useless or, worse, syntactically plausible but semantically mismatched with your local environment. The second cost is version coupling. The README tells you to pin LEAN_COPILOT_VERSION to a stable tag or to main, and to make sure the version is compatible with other dependencies such as mathlib. In practice this means a LeanCopilot upgrade is a project-wide dependency event, not a library bump you can absorb quietly. The release cadence visible in the repository metadata reinforces this: v4.31.0 in June 2026, then v4.32.0 and v4.33.0 two months later in August, which suggests tracking upstream Lean releases closely. If you are on a Lean version older than v4.3.0-rc2, or you cannot run Git LFS, or you are on a platform without a published prebuilt release and cannot supply CMake and a C++17 compiler, the integration will fail before any model runs. None of these are defects; they are the price of running inference inside the elaborator rather than beside it.
The alternative: LeanDojo as a retrieval corpus instead of an in-editor tactic
The obvious comparison is LeanDojo itself, which the README links as the source of the built-in models and the homepage for the project. The two solve adjacent problems with different architectures. LeanDojo is built around extracting proof states and premises from Lean repositories into a dataset, training or evaluating retrieval and generation models against that dataset, and measuring success offline. LeanCopilot inverts the direction: it takes models that LeanDojo-style pipelines produced and serves them back into a live Lean session as tactics you invoke while editing. The practical difference is where the feedback loop closes. With a dataset pipeline you learn after the fact which premises a model ranked correctly. With LeanCopilot you see candidate tactics in the goal state and can accept or reject them immediately, but you get no aggregate measurement of how well the model is doing across your file. If your goal is to evaluate a model, the dataset route gives you numbers. If your goal is to finish a proof today, the tactic route gives you candidates. They are not substitutes, and the README's own framing treats LeanCopilot as consuming the artifacts of that earlier work.
Maintenance, licensing and the upgrade path you should expect
LeanCopilot is MIT licensed, which is permissive and imposes few obligations beyond retaining the notice; the built-in models are hosted separately on Hugging Face under their own terms, so the licence of the code does not automatically describe the licence of the weights, and you should check each model card rather than assuming. The repository is not archived and was pushed as recently as August 2026, with three releases in the two months before that. That cadence is the maintenance signal that matters here: expect to revisit your pinned LEAN_COPILOT_VERSION whenever you move mathlib, and expect that moving to an unstable Lean release means pointing at main, which the README explicitly offers as an option for versions like v4.34.0-rc1. The upgrade itself is mechanical (change the revision, run lake update LeanCopilot, rebuild) but the failure mode is a link error or a version conflict rather than a compile error in your own proofs, which makes it slower to diagnose. Budget for it as a dependency you track rather than one you set once.
Bringing your own model and the API surface underneath the tactics
The default models are small by design, and the README treats replacing them as the expected advanced path. The section it labels as being for advanced users describes TacticSuggestion.lean as containing examples of how to configure suggest_tactics, including using different models and generating a different number of candidates, and it points to separate Model APIs and a Bring Your Own Model section. The README also notes that arbitrary models can run locally with or without GPUs, or remotely, and that running LLM inference inside Lean is not limited to theorem proving. That is the honest scope statement: the tactics are conveniences over a general inference binding. If your interest is in building custom proof automation, the tactic layer is a demonstration, and the model layer is the product. The trade-off is that once you leave the built-in models you also leave the tested configuration, and the README does not present a compatibility matrix for third-party models. Treat the built-ins as the supported path and anything else as your own integration work.
Editorial conclusion
Adopt LeanCopilot if your project already pins a Lean version at or above v4.3.0-rc2 and you want tactic suggestions and aesop-backed proof search available as ordinary tactics rather than through an external script. Do not adopt it if you cannot accept Git LFS, a CTranslate2 shared library in your link arguments, or a premise retriever that only sees a fixed mathlib4 snapshot. Before committing, verify three things in your own checkout: that your mathlib revision resolves against the LeanCopilot tag you chose, that lake exe LeanCopilot/download populated ~/.cache/lean_copilot/, and that the built-in tactic generator produces anything usable on your file. If the generator's output is empty or irrelevant on your domain, the rest of the integration will not compensate for it.
Community notes