Lean Copilot: LLMs as Copilots for Theorem Proving in Lean

🚩News: Our paper is accepted to the International Conference on Neuro-symbolic Systems (NeuS), 2025. See you in Philadelphia!

Lean Copilot allows large language models (LLMs) to be used natively in Lean for proof automation, e.g., suggesting tactics/premises and searching for proofs. You can use our built-in models from LeanDojo or bring your own models that run either locally (w/ or w/o GPUs) or on the cloud.

https://github.com/lean-dojo/LeanCopilot/assets/114432581/ee0f56f8-849e-4099-9284-d8092cbd22a3

Table of Contents

1. Requirements
2. Using Lean Copilot in Your Project
   1. Adding Lean Copilot as a Dependency
   2. Getting Started with Lean Copilot
      1. Tactic Suggestion
      2. Proof Search
      3. Premise Selection
3. Advanced Usage
   1. Tactic APIs
   2. Model APIs
   3. Bring Your Own Model
   4. Using Prebuilt System Libraries
4. Caveats
5. Getting in Touch
6. Acknowledgements
7. Citation

Requirements

• Supported platforms: Linux (priority), macOS (priority), Windows and Windows WSL.
• Git LFS.
• Optional (recommended if you have a CUDA-enabled GPU): CUDA and cuDNN.
• Required for building Lean Copilot itself (rather than a downstream package): CMake >= 3.7 and a C++17 compatible compiler. A downstream package normally downloads a prebuilt release instead of needing these, except on a platform we don't publish a release for (e.g. Intel macOS), where it automatically falls back to building from source and so needs them too.

Using Lean Copilot in Your Project

:warning: Your project must use a Lean version of at least lean4:v4.3.0-rc2.

Adding Lean Copilot as a Dependency

1. Add the package configuration option moreLinkArgs := #["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"] to lakefile.lean. For example,

package «my-package» {
  moreLinkArgs := #[
    "-L./.lake/packages/LeanCopilot/.lake/build/lib",
    "-lctranslate2"
  ]
}

Alternatively, if your project uses lakefile.toml, it should include:

moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]

2. Add the following line to lakefile.lean, including the quotation marks:

require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "LEAN_COPILOT_VERSION"

For stable Lean versions (e.g., v4.33.0), set LEAN_COPILOT_VERSION to be that version. For the latest unstable Lean versions (e.g., v4.34.0-rc1), set LEAN_COPILOT_VERSION to main. In either case, make sure the version is compatible with other dependencies such as mathlib. If your project uses lakefile.toml instead of lakefile.lean, it should include:

[[require]]
name = "LeanCopilot"
git = "https://github.com/lean-dojo/LeanCopilot.git"
rev = "LEAN_COPILOT_VERSION"

3. If you are using native Windows, add <path_to_your_project>/.lake/packages/LeanCopilot/.lake/build/lib to your Path variable in Advanced System Settings > Environment Variables... > System variables.

4. Run lake update LeanCopilot.

5. Run lake exe LeanCopilot/download to download the built-in models from Hugging Face to ~/.cache/lean_copilot/. Alternatively, you can download the models from Hugging Face manually from

• ct2-leandojo-lean4-tacgen-byt5-small
• ct2-leandojo-lean4-retriever-byt5-small
• premise-embeddings-leandojo-lean4-retriever-byt5-small
• ct2-byt5-small

6. Run lake build.

Here is an example of a Lean package depending on Lean Copilot. If you have problems building the project, our Dockerfile, build.sh or build_example.sh may be helpful.

Getting Started with Lean Copilot

Tactic Suggestion

After import LeanCopilot, you can use the tactic suggest_tactics to generate tactic suggestions. You can click on any of the suggested tactics to use it in the proof.

You can provide a prefix (e.g., simp) to constrain the generated tactics:

Proof Search

The tactic search_proof combines LLM-generated tactics with aesop to search for multi-tactic proofs. When a proof is found, you can click on it to insert it into the editor.

Premise Selection

The select_premises tactic retrieves a list of potentially useful premises. Currently, it uses the retriever in LeanDojo to select premises from a fixed snapshot of Lean and mathlib4.

Running LLMs

You can also run the inference of any LLMs in Lean, which can be used to build customized proof automation or other LLM-based applications (not limited to theorem proving). It's possible to run arbitrary models either locally or remotely (see Bring Your Own Model).

Advanced Usage

This section is only for advanced users who would like to change the default behavior of suggest_tactics, search_proof, or select_premises, e.g., to use different models or hyperparameters.

Tactic APIs

• Examples in TacticSuggestion.lean showcase how to configure suggest_tactics, e.g., to use different models or generate different numbers of tactics.
• Examples in ProofSearch.lean showcase how to configure search_proof using options provided by aesop.
• Examples in PremiseSelection.lean showcase how to set the number of retrieved premises for select_premises.

Model APIs

Examples in ModelAPIs.lean showcase how to run the inference of different models and configure their parameters (temperature, beam size, etc.).

Lean Copilot supports two kinds of models: generators and encoders. Generators must implement the TextToText interface:

class TextToText (τ : Type) where
  generate (model : τ) (input : String) (targetPrefix : String) : IO $ Array (String × Float)

• input is the input string
• targetPrefix is used to constrain the generator's output. "" means no constraint.
• generate should return an array of String × Float. Each String is an output from the model, and Float is the corresponding score.

We provide three types of Generators:

• NativeGenerator runs locally powered by CTranslate2 and is linked to Lean using Foreign Function Interface (FFI).
• ExternalGenerator is hosted either locally or remotely. See Bring Your Own Model for details.
• GenericGenerator can be anything that implements the generate function in the TextToText typeclass.

Encoders must implement TextToVec:

class TextToVec (τ : Type) where
  encode : τ → String → IO FloatArray

• input is the input string
• encode should return a vector embedding produced by the model.

Similar to generators, we have NativeEncoder, ExternalEncoder, and GenericEncoder.

Bring Your Own Model

In principle, it is possible to run any model using Lean Copilot through ExternalGenerator or ExternalEncoder (examples in ModelAPIs.lean). To use a model, you need to wrap it properly to expose the APIs in external_model_api.yaml. As an example, we provide a Python API server and use it to run a few models.

Using Prebuilt System Libraries

By default, building Lean Copilot from source clones and compiles its native dependencies, OpenBLAS and CTranslate2, which can be slow or awkward on systems (e.g., Nix-based distros) that already package these libraries or make it difficult to compile them from source. If you already have compatible builds available, you can point Lean Copilot at them instead with lake's -K flag (add -R too if you already have a .lake/build from a previous build, so that the new options take effect):

• -KsystemOpenblas=<path to your libopenblas.so/.dylib> skips cloning and building OpenBLAS (Linux/Windows only; macOS uses Apple's Accelerate framework instead of OpenBLAS).
• -KsystemCtranslate2Lib=<path to your libctranslate2.so/.dylib> together with -KsystemCtranslate2Include=<path to a directory containing the ctranslate2/, nlohmann/, and half_float/ header trees> skips cloning and building CTranslate2.

For example, on Linux:

lake -R -KsystemOpenblas=/usr/lib/libopenblas.so \
        -KsystemCtranslate2Lib=/usr/lib/libctranslate2.so \
        -KsystemCtranslate2Include=/usr/include \
        build

Caveats

• select_premises always retrieves the original form of a premise. For example, Nat.add_left_comm is a result of the theorem below. In this case, select_premises retrieves Nat.mul_left_comm instead of Nat.add_left_comm.

@[to_additive]
theorem mul_left_comm : ∀ a b c : G, a * (b * c) = b * (a * c)

• In some cases, search_proof produces an erroneous proof with error messages like fail to show termination for .... A temporary workaround is changing the theorem's name before applying search_proof. You can change it back after search_proof completes.

• On Linux, a downstream lean_exe target (as opposed to a lean_lib) links against Lean's own bundled, statically-linked libc++, while Lean Copilot's native code (ct2.cpp) is compiled against the system's libstdc++. A lean_lib never hits this (its .so tolerates undefined symbols, resolved later at load time), but a plain executable link requires every symbol resolved up front, so without extra configuration a lean_exe that depends on Lean Copilot fails to link with undefined libstdc++ symbols. Lean Copilot cannot fully paper over this on its own: statically bundling libstdc++ itself would collide with Lean's already-statically-linked libc++ (both define the same ABI-mangled symbols for types like std::logic_error), so it can only be linked in dynamically, which downstream still has to opt into. If your project has a lean_exe target, add this to its lakefile.toml/lakefile.lean on Linux (adjust the -L path for your distro, e.g. via gcc -print-file-name=libstdc++.so):

  moreLinkArgs = [
    "-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2",
    "-Wl,-L/usr/lib/gcc/x86_64-linux-gnu/13", "-Wl,-lstdc++"
  ]
  

  (-Wl,-lstdc++, not a plain -lstdc++: Lean's bundled clang driver silently rewrites a literal -lstdc++ argument to link libc++ instead, so it must be passed through to the linker directly.)

Getting in Touch

• For general questions and discussions, please use GitHub Discussions.
• To report a potential bug, please open an issue. In the issue, please include your OS information, the exact steps to reproduce the error on the latest stable version of Lean Copilot, and complete logs preferrably in debug mode. Important: If your issue cannot be reproduced easily, it will be unlikely to receive help.
• Feature requests and contributions are warmly welcome. Please feel free to start a discussion or open a pull request.

Acknowledgements

• We thank Scott Morrison for suggestions on simplifying Lean Copilot's installation and Mac Malone for helping implement it. Both Scott and Mac work for the Lean FRO.
• We thank Jannis Limperg for supporting our LLM-generated tactics in Aesop (https://github.com/leanprover-community/aesop/pull/70).

Citation

If you find our work useful, please consider citing our paper:

@article{song2024lean,
  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}
}