Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4

Haotian Deng; Chris Farber; Sonal Narasimha; Samskrithi Sivakumar; Yexiang Xue

cs.AIOct 18, 2026

Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4

Authors: Haotian Deng, Chris Farber, Sonal Narasimha, Samskrithi Sivakumar, Yexiang Xue

Organizations: Purdue University

Abstract

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 \in \{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\text{--}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

Panel of Figure 1 — 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	Net
1	0	1990	29.7	7.1	0	$+$ 0
	1		30.3	9.0	38	$+$ 38
	2		31.8	9.4	45	$+$ 45
	3		33.0	9.4	45	$+$ 45
3	0	1990	54.9	20.9	0	$+$ 0
	1		83.9	23.8	57	$+$ 57

Table 1: LeanDojo results across all

K\times 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{\to}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

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\in\{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

Panel of Figure 5 — 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	$\Delta T$ (s)	$\Delta$ Net	Eff.
1	$R{=}0\to 1$	0.6	38	63.33
	$R{=}1\to 2$	1.5	7	4.67
	$R{=}2\to 3$	1.2	0	0.00
3	$R{=}0\to 1$	29.0	57	1.97
	$R{=}1\to 2$	14.1	10	0.71
	$R{=}2\to 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.

=\Delta

Net

/\Delta T

, theorems gained per added second of mean cost. † At

K{=}3

R{=}2\to 3

\Delta 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.

Automated Theorem Proving

Automated theorem proving develops algorithms and AI systems that construct or check formal proofs in mathematics, logic, and software.

See all 160 papers

BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints
Jul 30, 2026Ruslan KhrulevAutomated Theorem Proving Interactive Theorem Proving
Lomonosov Moscow State University
Repair, Retry, and the Cost of Hindsight: Verifier Feedback in Formal Theorem Proving
Oct 15, 2026Jack Li, Sophia LiLLM Self-Correction Large Language Model-Guided Theorem Proving
Department of Computer Science, Stanford University
MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
May 26, 2026Jinzheng Li, Zeru Zhu, Yuanjie RenLarge Language Model-Guided Theorem Proving Automated Theorem Proving
1Northeastern University · 2Stony Brook University · 3Massachusetts Institute of Technology

Jul 30, 2026J/K move · Enter open · S save

BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints

Ruslan Khrulev

Lomonosov Moscow State University

Automated Theorem Proving Interactive Theorem Proving Lean Theorem Proving

Open paper AskPDF arXiv

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.

Abstract

Automated Theorem Proving

Explore similar work

BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints

Repair, Retry, and the Cost of Hindsight: Verifier Feedback in Formal Theorem Proving

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving