Learning to Repair Lean Proofs from Compiler Feedback

TL;DR

This paper tackles Lean proof repair by leveraging compiler feedback to train models that both fix failing proofs and generate grounded explanations. It introduces APRIL, a 260K-example dataset created by systematically mutating correct proofs to produce realistic errors, each paired with compiler diagnostics, a corrected proof, and human-readable explanations and fixes. Finetuning of multiple models on APRIL yields substantial gains in single-shot repair accuracy, with small to mid-size models approaching or matching larger baselines, illustrating the value of error-centered supervision for interactive theorem proving. The work also shows that explanations can aid human-in-the-loop use, while maintaining strong repair capability, and provides a public dataset to drive future research in feedback-conditioned proof repair for Lean 4.

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 \href{https://huggingface.co/datasets/uw-math-ai/APRIL}{this link}.

Figures (7)

• Figure 1: Overview of our dataset collection pipeline that collects paired correct and incorrect proof and their contextual information. We collected correct proofs from public datasets (Herald, Lean Workbook, NuminaMath-Lean). The paired error proofs that maintain the same proof sketch are generated by mutating tactics, lines of code, or theorems. Then, we used the Lean compiler to filter out the error proofs and extract their error messages, error lines, and goal states. Finally, we prompted an LLM to generate error explanations and fix suggestions based on the paired proofs and Lean Infoview. The resulting dataset pairs erroneous proofs and error information with structured labels containing the error interpretation from LLM and the corresponding correct proofs.
• Figure 2: Statistics based on mutation type. For each dataset, we report the total number of erroneous proofs generated and detail the distribution of specific mutation types: Line Mutation Error (LME), Multi-line Mutation Error (MLME), Tactic Mutation Error (TME), and Theorem Mutation Error (THME). The percentages denote the proportion of each mutation type within its respective dataset.
• Figure 3: An example of theorem mutation errors with an illustration of the generation model
• Figure 4: An example of tactic mutation errors with an illustration of the generation model
• Figure 5: An example of line mutation errors with an illustration of the generation model