Automated theorem provers often rely on sampling language models, but proof assistants like Lean reject each failed step with a precise error message --- information that pure sampling discards. To overcome this, we introduce a bounded, online step-level repair module. Our search samples K candidate tactics at each step and repairs a failed tactic at most R times. Instead of discarding failed tactics, we feed the compiler's error message to a pretrained repair model to fix individual rejected steps in place. This approach improves the solve rate over a sampling-only baseline across all tested candidate budgets (K∈{1,3,5,8}), achieving up to a 32% relative gain and solving 82 additional theorems on a 1,990-theorem subset of the LeanDojo benchmark. Repair is not free: it trades extra runtime for reachable proofs. But the trade is predictable: repair pays most when sampling is constrained; its return is front-loaded, with the first repair attempt capturing 84–96% of the total gain; and the gain comes almost entirely from shallow tactic-execution failures rather than structural errors such as type mismatches. This targeted repair successfully replicates on a second benchmark (Lean Workbook), nearly doubling the solve rate with zero regressions.
Figures & tables
Figure 1: Architecture of the bounded iterative repair system. Solid arrows show the main proof-search pipeline; the dashed baseline path shows tactics dropped without repair; bold orange arrows highlight the novel repair module. K tactics are sampled per state; each failed tactic triggers at most R repair attempts before being abandoned.
K
R
Atmp.
T(s)
P@1
Fix
Brk
Net
1
0
1990
29.7
7.1
0
0
+ 0
1
30.3
9.0
38
0
+ 38
2
31.8
9.4
45
0
+ 45
3
33.0
9.4
45
0
+ 45
3
0
1990
54.9
20.9
0
0
+ 0
1
83.9
23.8
57
0
+ 57
Table 1: LeanDojo results across all K×R configurations. The R=0 row of each K block is the pure-sampling (LeanDojo/ReProver-style) baseline; repair ( R>0 ) is measured against it. Atmp. = theorems attempted; T(s) = measured mean wall-clock per theorem (seconds); P@1 = Pass@1 (%); Fix / Brk = theorems newly solved / regressed vs. the baseline; Net = signed change in theorems solved. At every K , the R=0→1 step accounts for 84–96% of the total Net gain reached by R=3 (see below); Fix / Net are the most precise readout of this saturation where the rounded P@1 column loses resolution (e.g. K=3 , R=2 vs. R=3 ).
Figure 3: Net Delta versus repair depth R for each candidate budget K . Every panel shows the same shape: a large gain from R=0 to R=1 , followed by a flat or near-flat plateau.
Figure 4: Iso-runtime coverage: theorems solved within a per-theorem wall-clock budget T (log scale), for K∈{1,3,5,8} with (solid) and without (dashed) one repair. Repair lifts coverage at matched wall-clock across the range at every K shown, the gap widening as the budget grows (flat at K=1 , whose short runtime saturates coverage early).
Split
R
Proved
P@1
Fix
Brk
val (98)
0
21
21.4%
–
–
1
39
39.8%
18
0
2
42
42.9%
21
0
test (89)
0
17
19.1%
–
–
1
27
30.3%
10
0
2
28
31.5%
11
0
Table 2: Lean Workbook, K=5 , retrieval-free generator, best-first search. Fix / Brk are theorems newly solved/regressed vs. the R=0 baseline on that split; both splits show Brk = 0 at every R .
Figure 5: Visualization of search-tree traces for Set.not_subsingleton_iff at K=3 , from the raw run logs. Nodes are proof states, encoded by shape and color: blue circles are open states, red diamonds are failed states, and the green star is the solved state. Solid black edges are generator tactics; dashed blue edges are repair attempts. Without repair (a) every path dead-ends in a failed state; a single repair attempt (b) recovers a failed tactic and reaches the solved state.
K
Step
ΔT (s)
Δ Net
Eff.
1
R=0→1
0.6
38
63.33
R=1→2
1.5
7
4.67
R=2→3
1.2
0
0.00
3
R=0→1
29.0
57
1.97
R=1→2
14.1
10
0.71
R=2→3
− 0.9
1
† –
Table 3: Marginal cost and gain of each additional repair attempt, by K (successive differences of Table 1 ’s T(s) and Net columns; not cumulative). Eff. =Δ Net /ΔT , theorems gained per added second of mean cost. † At K=3 , R=2→3 , ΔT is within measurement noise (Table 1 ’s T(s) is nearly flat there), so efficiency is not meaningfully defined.
Failure category
Fail
Fix
Rate
No progress / simp
10,110
1,476
14.6%
Apply/exact failed
1,600
212
13.2%
Rfl failed
8,847
976
11.0%
Unknown identifier
7,164
386
5.4%
Rewrite failed
16,141
760
4.7%
Typeclass / synthesis
4,712
95
2.0%
Table 4: Repair fix rate by failure category, for the K=8 , R=1 run. Fail counts rejected generator tactics of each type; Fix counts those a single repair turned into a valid successor proof state; Rate = Fix/Fail. Ordered by rate; computed from the run logs.
LLM-based Lean proving systems increasingly organize a proof as a blueprint: a dependency graph of formal statements. We introduce BlueprintRepair, a repair interface that lets a model change this graph through ten schema-checked local operations. An operation names the node it edits, so the target theorem cannot be changed. Lean checks every applied change, and an accepted repair must declare every blueprint lemma its proof uses. We also construct BlueprintTrace, a benchmark of 142 controlled failures with complete accepted and rejected repair trajectories. We compare typed edits, exact source patches, and complete module rewrites under matched source, feedback, model, and budget, one episode per state and interface. With DeepSeek-V4-Flash, the three interfaces solve almost the same number of the benchmark's localized failures. Typed repair is the cheapest per solved state (patching is 1.30x as expensive, rewriting 2.06x), and within 10,000 completion tokens per task it reaches almost all of its final coverage, while both free-form interfaces are well behind. A second model, Qwen3.6-Flash, solves fewer states but keeps typed repair cheapest, puts it ahead on the proof-authoring states, and repeats the localized pattern.
Verifier-guided self-repair conditions a model on feedback from failed attempts before it tries again, without weight updates. Yet two findings in prior work are in tension: verifier feedback can improve repair of failures, but self-repair itself can provide little-to-no advantage over independent resampling. We reconcile these findings in Lean theorem proving through controlled one-step experiments that hold the preceding failure fixed while varying whether the failed proof is shown, whether the compiler error corresponds to that failure, and the retry instruction. We test frozen Qwen3.6-27B, a general-purpose model, and DeepSeek-Prover-V2-7B, a specialized prover, on difficult MiniF2F problems. We find two opposing effects. Showing the model its failed predecessor reduces success and sharply increases copying of it, while on Qwen adding that attempt's compiler error recovers the loss, to the level of the diagnostic alone. Replacing the predecessor with another theorem's failed proof largely removes the degradation on both models; on Qwen, replacing the diagnostic with another problem's error substantially reduces the recovery. Without the failed proof, correct diagnostics show no resolved advantage over wrong-diagnostic controls on either model. The failed-proof penalty persists with and without the retry instruction, whereas Qwen's diagnostic recovery is weaker without it. In 11-problem sequential experiments through 64 attempts, Qwen retains a correct-diagnostic benefit within failed-proof histories, while DeepSeek-Prover shows no resolved recovery. However, no tested one-step feedback condition establishes an advantage over instruction-only resampling, nor does 64-attempt sequential repair with failed proofs and correct diagnostics at equal token budgets. Verifier feedback can thus improve repair without overcoming the performance loss from conditioning on a failed attempt.
Jack Li, Sophia Li
Department of Computer Science, Stanford University
MerLean-Prover is an end-to-end Lean4 theorem prover that replaces sorry declarations with kernel-checkable proofs. It is built from three agent types (Planning, Check, and Lean) composed by a recursive outer loop whose unit of revision is the proof plan itself, and uses no fine-tuning, no custom RL objective, and no theorem-specific scaffolding. On FormalQualBench, a benchmark of 23 PhD-qualifying-exam theorems, MerLean-Prover solves 10/23, surpassing the strongest published open-source baseline (OpenGauss, 8/23). On Putnam2025, the same harness closes 12/12 with substantially lower total wall-clock than the next-best system that closes the full set. The harness also transfers to smaller models: Sonnet closes all four tested FormalQualBench problems, and Haiku closes the two short ones. These results suggest that harness design is a central factor in end-to-end Lean4 theorem proving, alongside raw model capability, and that a relatively simple harness can already be effective.
Jinzheng Li, Zeru Zhu, Yuanjie Ren
1Northeastern University · 2Stony Brook University · 3Massachusetts Institute of Technology