Tool LeanDojo project
Lean Copilot
Open-source toolkit allowing language models to be used natively in Lean for proof automation, suggesting tactics/premises and searching for proofs.[11]
Workflow level n/a Source: Repository-documented Outcome: Not empirically evaluated here
Research applicability
Open-source toolkit allowing language models to be used natively in Lean for proof automation, suggesting tactics/premises and searching for proofs.[11]
Getting started
Begin from the LeanCopilot repository; add the package to a Lean project and configure local or hosted models for tactic and premise suggestions.
Maintenance
Maintenance status not independently audited.
License
MIT License listed in repository metadata; not independently audited.
Workflow & human oversight
Resource-level classification is intentionally unspecified; instantiated workflows may differ. Humans define objectives, control data access, and check outputs.
Workflow level is not an evidence score; higher is not better evidence.
Approach
Supports built-in LeanDojo models or bring-your-own models running locally (with or without GPUs) or on the cloud within Lean projects.[11]
Limitations
A proof assistant checks formal statements, not whether the formalization matches the intended mathematics; no new theorem claim here. Documentation review only - no software execution or independent performance validation.
Reproducibility
Stored primary-source extract research-wide/candidate-evidence-036.md, accessed 2026-10-15, read for this review. No software, model or claimed outcome reproduced.
Adoption requirements
Compatible Lean project, Git LFS, local or hosted model; build requirements vary by platform.
Comments
No comments yet.
Add a comment
Comments are held for moderation before appearing. Critical or corrective comments are welcome — especially evidence that an entry overstates what has been verified.