LeanGraph

When does verifier-guided reasoning help an LLM write proofs that Lean accepts?

LeanGraph measures how often a language model produces a Lean 4 proof that the Lean kernel accepts, and whether retrieval of Mathlib lemmas, a planning step, and repair from compiler errors actually raise that rate. Lean is the grader: a plausible-looking proof that does not compile scores zero.

Theorems in the benchmark

203

150 Mathlib held-out · 53 Authored

Best agent, verified

Full (plan + retrieval + repair)

No-LLM automation, verified

26%

fixed tactic list

Model cost per verified proof

$0.026

Full (plan + retrieval + repair)

One theorem, end to end

Every configuration is the same loop with parts switched on or off.

01
Statement
A Lean 4 theorem, rendered by the harness. The model never writes the header.
02
Retrieval
Mathlib lemmas from an index that excludes every held-out module.
03
Model draft
A tactic proof from the model, optionally after a planning call.
04
Lean check
A long-lived REPL with Mathlib loaded answers in well under a second.
05
Error
Lean's exact output, classified into a fixed taxonomy.
06
Repair
The model sees only what Lean printed, then tries again.
07
Certificate
A fresh Lean process re-checks the proof: axioms, premises, extra declarations.

Headline comparisons

Paired over the same theorems. p-values are exact McNemar tests, Holm-adjusted across every pre-registered contrast.

Question	Treatment	Control	Difference	Holm p
RQ2 compiler-feedback repair vs one draft Repair vs Direct · n = 174	6%	1%	+5.7 pts [+2.3 pts, +9.2 pts]	0.025
RQ2 repair vs independent resampling at equal LLM calls Repair vs Direct ×4 · n = 174	6%	1%	+5.2 pts [+2.3 pts, +8.6 pts]	0.047
RQ1 retrieval, single draft Hybrid retrieval vs Direct · n = 174	2%	1%	+1.1 pts [−1.1 pts, +3.4 pts]	1.000
RQ1 retrieval, with repair Hybrid retrieval + repair vs Repair · n = 174	5%	6%	−1.7 pts [−6.3 pts, +2.9 pts]	1.000
RQ3 planning on top of retrieval + repair Full (plan + retrieval + repair) vs Hybrid retrieval + repair · n = 174	7%	5%	+2.9 pts [−0.6 pts, +6.3 pts]	1.000
Primary: full agent vs direct generation Full (plan + retrieval + repair) vs Direct · n = 174	7%	1%	+6.9 pts [+3.4 pts, +10.9 pts]	0.007
Ablation: retrieval Full (plan + retrieval + repair) vs Full − retrieval · n = 174	7%	5%	+2.3 pts [−1.7 pts, +6.3 pts]	1.000
Ablation: compiler feedback Full (plan + retrieval + repair) vs Full − compiler feedback · n = 174	7%	6%	+1.7 pts [+0.0 pts, +4.0 pts]	1.000

What counts as a proof

A fresh lean process, pinned to Lean 4.33.1 and Mathlib v4.33.1, accepts the file with no errors.
The proof uses only the standard axioms (propext, Classical.choice, Quot.sound): no sorry, no new axioms.
For a Mathlib theorem, the proof uses nothing from the theorem's own module or any module built on it.
The certifier reports under a random per-run nonce, so text written by the model cannot forge its verdict.

Full methods · Browse every theorem and trace