Lean 證明修復：不要只靠重新抽樣

The problem: proof search wastes its best feedback

Language models generate Lean proofs by proposing tactics or terms, compiling them, and trying again after failure. The common fallback is resampling: if a candidate does not compile, discard it and ask the model for another one. That treats a failed proof as a binary event even though Lean usually explains what went wrong.

A failed step can reveal that a theorem has the wrong argument order, a hypothesis is missing, a type does not unify, or a tactic produced the wrong shape of goal. These are actionable constraints. They can narrow the next proposal without requiring the model to rediscover everything that was already correct.

The transferable technique is to make compilation an online repair signal, while strictly bounding how many edits are allowed before abandoning the candidate. The goal is not to rescue every bad proof. It is to spend the information already produced by verification before paying for an entirely new search branch.

How it works

A Lean proof is a sequence of state transitions. The current state contains one or more goals; a tactic transforms that state, and Lean checks the resulting term before accepting the transition. If the tactic fails, Lean emits a diagnostic tied to the source location and often includes the expected type, available hypotheses, or remaining goal.

A repair loop keeps the current proof context and asks for a local correction. The model does not restart from the original theorem unless the bounded repair budget is exhausted. Conceptually, the loop is:

1. Generate the next proof step.
2. Compile the file or command containing that step.
3. If it succeeds, commit the step and continue.
4. If it fails, return the diagnostic and current goal to the model.
5. Accept only a repaired step that compiles.
6. Stop repairing after a small fixed number of attempts.

The important detail is granularity. Repairing one tactic or one proof fragment preserves all earlier verified work. Rewriting the entire proof after an error throws away useful structure and makes the search distribution much broader. A local loop also gives the model a clearer assignment: explain the reported mismatch by changing the failing fragment, rather than inventing a new proof from scratch.

A minimal compiler check can be driven with ordinary process execution:

import subprocess

result = subprocess.run(
    ["lake", "env", "lean", "Main.lean"],
    text=True,
    capture_output=True,
)

if result.returncode == 0:
    print("accepted")
else:
    print(result.stdout + result.stderr)

In a real agent, the generated fragment should be inserted into a temporary Lean file or an isolated project. The repair prompt should include the exact diagnostic, the active theorem statement, the local hypotheses, and the candidate step—not an unbounded transcript of every previous attempt. This keeps the context focused on the state Lean actually rejected and makes each repair easier to attribute.

What the evidence actually shows

The relevant evidence is mechanistic: Lean rejects incorrect proof steps with structured, precise feedback, while pure sampling discards that information. A bounded compiler-guided repair module is therefore exploiting a signal that ordinary generate-and-resample pipelines already pay to obtain. The compiler is doing more than checking the final answer; it is describing the boundary between the proposed term and the required one.

The reported work, Fix, Not Just Resample, presents this as an online, step-level repair strategy rather than a claim that every failed proof can be salvaged. Its central comparison is between using compiler errors to modify a candidate and treating each error as a reason to sample independently. The distinction is especially important when a candidate is mostly sound and only one local choice has the wrong shape.

That distinction matters when interpreting results. A repair system can improve proof completion without making the language model intrinsically better at theorem proving; it may simply use external verification more efficiently. Conversely, any gains depend on diagnostics being sufficiently informative and on the model being capable of mapping them to a valid local change. If the error is ambiguous or the needed change is global, a local repair loop may offer little advantage.

The strongest general lesson is broader than Lean: whenever a verifier returns structured failure information, feed that information back into a bounded local search. The verifier becomes part of the inference loop, not merely a final gate. This framing also clarifies what to evaluate: not only final success, but how often a diagnostic leads to a valid next step and how often the system recognizes that it should stop repairing.

Using it

Start with a narrow repair budget. Allow perhaps a few attempts for each failed step, and then fall back to a fresh candidate or terminate the theorem. The bound prevents a difficult goal from consuming the entire run and makes latency and cost predictable. It also keeps the agent from repeatedly making cosmetic edits when the underlying proof plan is wrong.

Separate accepted proof state from speculative text. Only update the canonical proof after Lean compiles the candidate; otherwise, the next repair should see the last verified state plus the failed fragment and its diagnostic. This separation prevents one unsuccessful edit from contaminating later prompts and gives backtracking a precise point to return to.

Normalize diagnostics before placing them in a prompt. Remove duplicated compiler banners, preserve line and column information, and keep the goal state intact. A useful repair instruction is explicit: change only the failing step, preserve preceding code, and return Lean code without explanation. The model should know both what it may alter and what must remain invariant.

Use deterministic checks for every proposed repair. Run Lean in the same project environment, with the same imports and options used for evaluation. If possible, compile a small temporary file containing the theorem and its dependencies so syntax and elaboration errors are caught quickly. Log each transition: candidate text, diagnostic, repair attempt, and whether the repaired step compiled. These traces are useful for debugging prompts, measuring where repairs fail, and later training a model on successful error-to-fix transformations.

Limitations and failure modes

Compiler feedback is not always a complete diagnosis. A message may point at the location where elaboration became impossible rather than the earlier mistake that caused it. Multiple fixes may be plausible, and the model can choose one that compiles locally but makes later goals harder. A diagnostic can constrain the next move without identifying the best move.

Local repair also cannot solve every global planning error. If the proof chose the wrong lemma, introduced an unusable intermediate claim, or discarded a necessary hypothesis, repeatedly editing the current tactic may be worse than restarting. The repair budget must therefore coexist with a recovery policy for backtracking or resampling. The system needs a way to recognize that the current prefix is no longer promising.

There is a verification cost as well. Invoking Lean after every token is impractical, while waiting until an entire long proof is generated reduces the value of step-level feedback. Systems need a practical unit of compilation, such as one tactic block or one theorem fragment, and should measure that choice against process startup and elaboration time. Smaller units provide sharper feedback but may require more checks; larger units amortize checking but make failures harder to localize.

Finally, successful compilation is not the same as a useful proof search trajectory. A repair policy can overfit to error messages, produce brittle tactic scripts, or exploit expensive automation. Track proof length, compilation time, and robustness—not only whether the final theorem closes. A repair that succeeds once but leaves an opaque or costly script may be less valuable than a fresh candidate that produces a simpler continuation.

What to watch

The next useful developments will be better representations of proof state and diagnostics, not merely larger generators. In particular, watch for repair policies that learn when to edit locally, when to backtrack, and when to request a new plan. Those decisions determine whether compiler feedback becomes a disciplined search strategy or just another prompt payload.

The interface between verifier and model is also important. A useful representation should distinguish the active goal from surrounding text, identify which fragment is speculative, and preserve the hypotheses that a repair is allowed to use. That structure can help the model make smaller edits and can make logged repair traces useful beyond the run that produced them.

The same pattern should transfer to SQL execution, typed program synthesis, configuration validation, and hardware design: preserve the verified prefix, expose the verifier’s structured failure, and spend a bounded number of attempts on a targeted fix. In each setting, the exact diagnostic differs, but the control problem is similar: decide how much of the current artifact remains trustworthy, apply a constrained correction, and abandon the branch when local repair no longer matches the failure.