GraphCanon updated Sep 20, 2026 · GitHub synced Sep 20, 2026
40views this month
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 (0d since push)
- As of Sep 19, 2026
- Provenance
- Not a fork · Organization account
- As of Sep 19, 2026
- Security (OSV)
- No lockfile
- As of Jul 11, 2026
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 · Sep 19, 2026
- Docker
- Dockerfile present
Source: dockerfile:Dockerfile · Sep 19, 2026
- Languages
- c++
Source: github.language · Sep 19, 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 com...
For agents
This page has a .md twin and JSON over the API.