Lean Proofs for AI-Generated Code Break After Refactoring 13-27% of the Time

When a language model writes code and immediately attaches a formal mathematical proof of its correctness in Lean, it looks bulletproof: the program is guaranteed to do what it's supposed to. But every existing test checks the proof against only one fixed version of the code. In real-world development, code gets rewritten constantly — duplicate logic gets pulled into a separate function, operations get reordered, conditions get inverted — while the program's behavior stays the same. The question is whether the old proof survives that kind of restructuring, even when the code's meaning hasn't changed.

The authors propose a methodology called RefactorProof to measure exactly this. They took 185 problems from the well-known VERINA benchmark (which checks both code and Lean proofs) and applied five kinds of mechanical, fully automated rewrites to each problem: extracting a piece of logic into a separate function, swapping operands in commutative operations, inverting conditions, and so on. For every such rewrite, Lean was used to separately prove that the program's behavior hadn't changed. This produced 458 verified code variants. Each variant was then paired with the original proof (byte-for-byte identical) to see whether Lean still accepted it.

What turned out to be fragile — and what didn't

The reference proofs that the VERINA authors wrote by hand for 46 problems survived refactoring almost unscathed — a breakage rate of just 4.3%. But that doesn't mean hand-written proofs are inherently more robust: all 46 of those problems are the simplest in the benchmark, with a median code length of one line, and only 6.5% of them are recursive.

Proofs generated by specialized theorem-proving models — DeepSeek-Prover-V2-7B and two versions of Goedel-Prover-V2 (8B and 32B) — broke much more often: failure rates ranged from 13.3% to 26.8%. But when comparing the models to the reference baseline on an identical, matched set of problems, the picture flips: model-generated proofs survive refactoring more often than reference proofs — by 15.6 points for DeepSeek-7B, 18.8 points for Goedel-32B, and 20.3 points for Goedel-8B. The difference is statistically significant in all three cases.

Why some proofs collapse and others hold

The researchers identified a specific mechanism behind this resilience. Reference proofs typically begin with the `unfold` command, which expands the function's definition directly in the text. Model-generated proofs more often start by explicitly asserting that a function call and its body are equal, using the `rfl` tactic (a so-called "definitional bridge"), and then prove the rest automatically.

When code gets moved into a separate function (logic extraction), that "bridge" turns out to be far more durable: at the task level, bridge-based proofs survive in 6 out of 6 cases, while other strategies only manage 6 out of 31. But this trick has a downside: if the rewrite substantively changes the function's body (rather than just its location), a bridge tied to the specific text of that body stops type-checking — such proofs survive only 0 out of 3 times, compared to 17 out of 19 for more general proofs not tied to a specific wording.

A break isn't a catastrophe

The main practical takeaway: a proof failing to check after refactoring doesn't necessarily mean an expensive rewrite. The researchers tested this directly: they took the broken proofs and tried to fix them with one simple, targeted edit — renaming a single identifier. Out of 54 eligible breakages in reference proofs, 51 were fixed this way; out of 85 breakages in model-generated proofs, 58 were fixed.

For teams relying on verifiable AI code generation, the conclusion is straightforward: the mere fact that a proof stops checking after refactoring is no reason to panic, nor is it evidence that a model is fundamentally worse at producing proofs. It's better read as a signal to build automatic checking and lightweight proof repair into the verification pipeline after any code change, rather than treating a single breakage as a final verdict on a model's quality.