Learning to Repair Lean Proofs from Compiler Feedback

AI summary

Overview

Research area: Machine learning for formal theorem proving, specifically supervised learning for Lean proof repair and error diagnosis.

Technical level: Intermediate (requires some familiarity with formal verification and language model fine-tuning; the core idea is accessible to general readers).

Scope: The paper introduces APRIL, a 260,125-example dataset of failed Lean proofs paired with compiler diagnostics, corrected proofs, and natural-language explanations, and shows that supervised fine-tuning on this data substantially improves single-shot proof repair.

Note on authorship: The arXiv metadata lists Evan Wang as first author, while the paper content lists Yiran Wang as first author. All authors are affiliated with the University of Washington. The paper is arXiv:2602.02990v2 [cs.LG], dated 13 Mar 2026.

What This Paper Is About

Almost all existing Lean proof datasets contain only correct proofs, so language models get very little training signal for reading compiler errors, understanding what went wrong, and making a targeted fix. The authors reframe proof repair as a supervised learning problem: given a broken proof plus the Lean compiler's error message and local goal state, predict both a repaired proof that compiles and a natural-language diagnosis of the failure. To make this trainable, they build a large dataset backward by systematically breaking correct proofs.

Key Contributions

1. The APRIL dataset: 260,125 erroneous-proof examples derived from 39,492 unique compiled theorems, each containing the broken proof, the Lean compiler error message and local proof state, a corrected proof target, and an LLM-generated natural-language explanation and fix suggestion. The dataset is publicly released on Hugging Face.

2. A systematic four-way mutation pipeline: Starting from correct proofs, the authors generate realistic failures via theorem substitution, tactic replacement, line-level redaction, and multi-line redaction, keeping only mutated proofs that actually fail to compile under Lean 4.22.0-rc4.

3. Evidence that diagnostic-conditioned supervision works: A finetuned 4B-parameter model (Qwen3-4B-Instruct-2507) reaches 27.4% correction accuracy in single-shot repair, up from 1.1% for its base version, slightly exceeding Goedel-Prover-V2-32B at 26.8% under the same protocol.

4. A measured trade-off between repair and explanation: Training exclusively for repair raises pass@1 from 27.4% to 31.2%, while joint training produces explanations that improve a separate model's success rate from 4% to 29% when supplied as context.

Main Findings

• Large headline gains from finetuning: For Qwen3-4B-Instruct-2507, finetuning on APRIL lifts repair accuracy from 1.1% to 27.4%, a 25x increase. This slightly exceeds Goedel-Prover-V2-32B (26.8%) under the identical single-shot interface with no search or iteration.

• Smaller models overtake larger baselines: Finetuned 8B models reach 31–35% repair accuracy, outperforming the 32B Goedel baseline. Finetuned Goedel-8B scores 34.6% overall and finetuned Kimina-8B scores 31.9%.

• Baseline models without finetuning: Goedel-Prover-V2-8B 15.5%, Goedel-Prover-V2-32B 26.8%, Kimina-Prover-1.7B 8.4%, Kimina-Prover-8B 11.1%, Qwen3-4B-Instruct-2507 1.1%.

• Error types differ sharply in difficulty: Tactic mutations are easiest, with top performance reaching 42.5%. Theorem mutations are intermediate. Line mutations are hardest, with maximum accuracy of 13.5%, since they often require replacing semantically inconsistent or hallucinated proof steps.

• Joint training does not cause negative interference: Models trained on all error types stay competitive with models trained separately per error type, indicating the mutation categories share structural overlap and that repair strategies generalize across them.

• Explanations cost a little accuracy but add real value: Specializing only on repair raises pass@1 from 27.4% to 31.2%. With explanations, Goedel-8B drops from 36.7% to 34.6% (−2.1%) and Kimina-8B drops from 36.9% to 31.9% (−5.0%). The paper notes that top repair-specialized models (Goedel and Kimina) have lost much of their ability to produce meaningful natural language.

• Explanations transfer to other models: DeepSeek succeeds at a rate of 4% when aided by base Qwen's explanations and 29% when aided by the trained model's explanations, performing better than either model individually.

• Theorem substitution dominates the data: Theorem substitution errors constitute 59.5% of incorrect proofs. By count, the dataset contains 154,870 theorem mutations, 62,150 tactic mutations, 24,786 multi-line mutations, and 18,319 line mutations.

• Proof source composition: Of the 39,492 compiled theorems, 40.54% come from Herald (16,010), 24.03% from Lean Workbook (9,491), 15.00% from Numina Autoformalizer (5,925), and 20.42% from Numina Human (8,066). Numina Human proofs are by far the longest, averaging 50.93 lines and 8.90 have statements.

• Splits and leakage control: The dataset is split by original theorem rather than by mutated proof (Train 249,027; Val 9,263; Test 1,835), and all theorem names are anonymized to the canonical identifier lean_problem to prevent memorization.

Methodology in Plain English

Correct Lean proofs are plentiful; human-written failed proofs are not. So the authors work backward. They start with 56,090 proofs from Herald, Lean Workbook, and NuminaMath-Lean, keep the 39,492 that compile under Lean 4.22.0-rc4, and then deliberately break them:

• Theorem mutation replaces one used theorem with a semantically similar but incompatible one, found via the LeanExplore semantic search engine.
• Tactic mutation swaps one tactic for another from the same equivalence class (for example swapping nlinarith with linarith, norm_num, or ring), substituting one to three tactics per proof.
• Line mutation redacts a single proof line after by, asks DeepSeek-V3-0324 to fill it in, reinserts the completion, and keeps it only if compilation fails.
• Multi-line mutation does the same but redacts the rest of the proof after a random line, capping redaction at half the proof.

Every retained example is compiled using Lean-Interact against the Lean REPL, which supplies the error message, the offending location, and the local goal state. DeepSeek-V3-0324 then generates a natural-language explanation of the failure and a fix suggestion from the original proof, the mutated proof, the error message, and any mutation metadata.

For training, the authors fine-tune Qwen3-4B-Instruct-2507, Kimina-Prover-Distill-8B, and Goedel-Prover-V2-8B with an identical LoRA pipeline (rank 32, scaling factor 64, dropout 0.1, applied to attention and MLP projections). Prompts concatenate the error, proof state, and failing proof; the target is a completion with an explicit diagnostic reasoning step before the corrected code. Training uses AdamW at a learning rate of 1×10⁻⁴ with cosine decay and linear warmup, up to 15,000 steps at effective batch size 8 and maximum sequence length 2048, with early stopping at patience 5 (1,250 steps). Everything runs in bfloat16 on NVIDIA L40S and H200 GPUs.

Evaluation is strictly single-shot: a repair counts as successful only if the model's output compiles under Lean 4.22.0-rc4, with no search or iteration. The test set is 1,835 erroneous proofs spanning all four mutation types.

The appendix also documents approaches that failed, including prompting a model to introduce an "interesting" error, translating proofs to natural language and back, round-tripping through Rocq or Lean 3, targeting known Lean pitfalls, random multi-line redactions (which failed even with Gemini 3), and a two-stage prover pipeline that used Kimina-Prover-Distill-1.7B followed by Goedel-Prover-V2-8B (which tended to rewrite proofs from scratch rather than repair them).

Why This Matters

Research impact. The paper argues that error-centric supervision is a strong and underutilized training signal for agentic theorem provers that refine proofs iteratively from feedback. It also cites prior work showing that iterative proof refinement using compiler feedback is 32–128x more efficient than pass@k sampling, which makes targeted repair capability directly relevant to how provers are deployed. By releasing both the data and the finetuned models, the authors provide a concrete resource where none previously existed at this scale.

Real-world applications:

• Interactive proof assistants: Models that explain a Lean error in natural language and propose a localized fix could function as proof-engineering assistants inside editors.
• Education: Natural-language diagnoses of formal verification failures can help students and newcomers understand why a proof step is wrong.
• Tool-using agents: Explanation outputs improved DeepSeek's success rate from 4% to 29% when supplied as context, suggesting a role as an auxiliary module for other provers.
• Software engineering for formal methods: The same error-mutation-plus-repair philosophy transfers to other compiler-feedback-driven repair settings.

Industry relevance. Companies and labs building formal-methods tooling, verified software, and agentic coding assistants need models that can read diagnostics and make minimal edits rather than regenerate everything from scratch. This paper shows that a small, cheap 4B model can be competitive with much larger specialized provers on that specific skill, and that data-generation pipelines can manufacture the supervision that is missing from public corpora.

Future Directions

• Combining repair supervision with search and reinforcement learning. The authors explicitly frame their evaluation as an ablation of feedback-conditioned repair rather than end-to-end proving performance, since Goedel is typically deployed with search and iteration. Testing the finetuned models inside those loops is the obvious next step.
• Raising accuracy on line mutations. These remain the hardest category, with maximum accuracy of 13.5%, because they require fixing hallucinated or semantically inconsistent proof steps.
• Managing the repair-versus-explanation trade-off. Joint training costs accuracy relative to repair-only training (27.4% versus 31.2% for Qwen3-4B). Whether that gap can be closed without losing interpretable diagnoses is unresolved.
• Generating more realistic failures. The authors' mutation-based approach produces errors anchored in real compiler behavior, but their appendix lists several more ambitious generation strategies that failed. Improved methods for synthesizing genuinely human-like mistakes remain an open problem.

Target Audience

Researchers and engineers working on neural theorem proving, formal verification, or language-model-based program repair will get the most from this paper. It is also useful for practitioners who need models that interpret compiler feedback and for anyone building training datasets where paired failure-and-fix supervision is scarce. Readers without background in Lean or formal methods can follow the framing and results, though the mutation taxonomy and evaluation protocol will be easier to appreciate with some exposure to proof assistants or automated program repair.

Authors’ abstract

As neural theorem provers become increasingly agentic, the ability to interpret and act on compiler feedback is critical. However, existing Lean datasets consist almost exclusively of correct proofs, offering little supervision for understanding and repairing failures. We study Lean proof repair as a supervised learning problem: given an erroneous proof and compiler feedback, predict both a corrected proof and a natural-language diagnosis grounded in the same feedback. We introduce APRIL (Automated Proof Repair in Lean), a dataset of 260,000 supervised tuples pairing systematically generated proof failures with compiler diagnostics and aligned repair and explanation targets. Training language models on APRIL substantially improves repair accuracy and feedback-conditioned reasoning; in our single-shot repair evaluation setting, a finetuned 4B-parameter model outperforms the strongest open-source baseline. We view diagnostic-conditioned supervision as a complementary training signal for feedback-using provers. Our dataset is available at https://huggingface.co/datasets/uw-math-ai/APRIL.