GraphCanon updated today · GitHub synced today
Decision brief
A system that leverages large language models for theorem proving in the Lean environment.
Good fit when
- Need support with formal proof development in Lean or Lean4 specifically
- Seeking to enhance automated reasoning capabilities within a Lean project
Avoid when
- Working exclusively in theorem provers other than Lean or Lean4
- Looking for general-purpose AI programming assistant beyond Lean's domain
Observed Jul 17, 2026 · Source: enrich:decision_facts
Verify the decision
Maintenance and security
Full trust report- Maintenance
- Very active (2d since push)
- As of today
- Provenance
- Not a fork · Organization account
- As of today
- Security (OSV)
- No lockfile
- As of 1mo
Public GitHub metadata and optional OSV scans. Signals, not a guarantee. Trust methodology.
Install
git clone https://github.com/lean-dojo/LeanCopilotSimilar tools
Same-category neighbours. No typed graph edges are catalogued for this tool yet.
Evidence and technical details
Sourced facts, taxonomy, compatibility claims, README excerpt, and machine-readable endpoints.
Overview
A system that employs large language models to assist with theorem proving within the Lean formalization environment, supporting both Lean and Lean4.
Capability facts
- Deploy
- Self-host
Source: dockerfile:Dockerfile · Aug 25, 2026
- Docker
- Dockerfile present
Source: dockerfile:Dockerfile · Aug 25, 2026
- Languages
- c++
Source: github.language · Aug 25, 2026
Categories
Tags
README
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.
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).
For agents
This page has a .md twin and JSON over the API.