Lean Copilot
In-editor Lean 4 neural theorem-proving framework combining LLM tactic generation, premise selection, and a best-first proof search tactic that uses the model confidence as score.
The loop
- Proposes
Native CTranslate2 models running inside Lean 4 propose tactics and retrieve premises for the active proof goal.
- Judged by
The Lean 4 kernel checks each tactic application and returns updated subgoal states.
- Steers
A best-first search tactic (`search_proof`) with the model confidence as score explores the proof tree until all goals close.
Headline result
Automates proof goals directly inside Lean 4 workflows with 3.8x faster tactic inference than Python RPC bridges.
What this does not prove
Designed for interactive lemma and subgoal automation rather than multi-hour distributed search.
How it generalizes the harness
- The algorithm is the solver
- Inverted control
- A domain authority judges
- Search over a population
- An infallible formal kernel
A native Lean 4 best-first search engine invokes the neural tactic generator and verifies every node in the Lean kernel.
Classification
| What it proposes | Proof tactic |
|---|---|
| Generative model | ReProver / ByT5 tactic and premise models |
| Algorithmic authority | Lean 4 kernel and best-first proof search |
| Feedback | Proof state |
| What gets updated | Search tree |
| When it runs | At inference time |
| Validity | Formal (machine-checked) |
| Evidence | Code released |
| Lineage | Derivative |