PaperlayerView exact revision on arXiv

Source-linked AI summary

Learning to Repair Lean Proofs from Compiler Feedback

Evan Wang, Simon Chess, Daniel Lee, Siyuan Ge, Ajit Mallavarapu, Jarod Alper, Vasily Ilin

arXiv:2602.02990v2cs.LG

TL;DR

Existing Lean datasets provide limited supervision for interpreting compiler diagnostics and repairing failed proofs. APRIL frames proof repair as feedback-conditioned supervised learning, and finetuning on it achieves 27.4% single-shot correction accuracy, outperforming the strongest open-source baseline.

  • Problem

    Existing Lean datasets contain predominantly correct proofs, providing limited supervision for interpreting diagnostics, explaining failures, or proposing targeted repairs.

  • Method

    APRIL pairs systematically mutated Lean proof failures and compiler diagnostics with verified repairs and aligned natural-language diagnosis and fix targets.

  • Results

    27.4% correction accuracy is achieved by finetuned Qwen3-4B-Instruct versus 1.1% for the base model and 26.8% for Goedel-Prover-V2-32B.

  • Takeaways & Limitations

    Error-centric supervision is a strong, underused training signal for theorem provers that iteratively refine Lean proofs from compiler feedback.

  • Takeaways & Limitations

    The evaluation measures single-shot repair from a failing attempt rather than theorem-level success under multi-sample search or exploration.

Abstract

from arXiv · show

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.

1 Introduction

The paper frames Lean proof repair as an overlooked, feedback-driven complement to end-to-end proof generation. It introduces aligned tasks and a 260K-example dataset pairing erroneous proofs and compiler diagnostics with corrected proofs and explanations.

  • Motivation: Current theorem-proving systems mainly generate complete valid proofs, while failures and compiler feedback are not treated as supervised learning targets.Training data and evaluation therefore focus primarily on successful proofs rather than repairing failed attempts.
  • Motivation: Human proof development iteratively inspects compiler diagnostics and revises partial proofs, but public corpora generally omit these intermediate failed states.The paper contrasts error-driven proof engineering with final-proof-only resources such as mathlib and related datasets.
  • Contributions: The work defines two aligned feedback-conditioned tasks: producing a corrected proof and generating a natural-language diagnosis with a fix suggestion.Both tasks use the same error message and local proof state while emphasizing formal repair or human-interpretable debugging.
  • Method: A systematic mutation pipeline generates realistic failures by substituting semantically related theorems and swapping similar tactics.The pipeline starts from correct proofs and creates controlled erroneous variants for proof-repair supervision.
  • Contributions: 260K Lean proof-repair examples pair erroneous proofs and compiler diagnostics, including error messages and local proof states, with corresponding corrected proofs.The dataset is designed to support supervised learning from failures rather than only from verified final proofs.

2 Related Work

Prior Lean theorem-proving systems mainly use learning, search, reinforcement learning, synthetic data, and verifier feedback for proof generation and exploration. This work addresses the lack of supervised error-state data by adapting diagnostic-feedback repair ideas and systematically mutating correct Lean proofs into failures.

  • Neural Theorem Proving in Lean: Recent Lean systems primarily target end-to-end proof generation using language models, search, reinforcement learning, and synthetic data pipelines.LeanDojo supports systematic benchmarking and retrieval-augmented proving, while Lean 4 provides the formal foundation.
  • Verifier Feedback and Proof Repair: Verifier errors in Lean pipelines mainly guide exploration and policy optimization, while refinement systems use compiler diagnostics to regenerate proofs iteratively.The passage contrasts these uses with supervised correction targets.
  • Proof Datasets and Training Corpora: Large formal libraries and autoformalization datasets provide verified or aligned formal artifacts but generally omit intermediate error states encountered during proof development.The passage names mathlib, Lean Workbook, Herald, and NuminaMath as examples.
  • Program Repair from Diagnostic Feedback: Program-repair research learns from erroneous–corrected program pairs and compiler diagnostics, including scalable synthetic error–fix supervision validated by compilers or analyzers.These approaches motivate transferring diagnostic-feedback repair to formal verification.
  • Program Repair from Diagnostic Feedback: The formal-verification approach systematically mutates correct Lean proofs into plausible failures and trains models for feedback-conditioned repair.This directly applies the program-repair philosophy to Lean proofs.

3 Methodology

APRIL is constructed by mutating verified Lean proofs into compiler-checked failures paired with repairs, diagnostics, explanations, and fix suggestions. Models are trained with prompts combining errors, proof states, and failing proofs, while targets explicitly encourage diagnosis before code generation.

  • APRIL dataset construction: Each APRIL entry pairs a noncompiling Lean proof with a syntactically similar compiling repair, compiler feedback, an error explanation, and a fix suggestion.Compiler feedback includes error messages and proof state.
  • APRIL dataset construction: APRIL is built backward from correct proofs by systematically introducing errors, with compiler-generated diagnostics, offending locations, local goals, and verified repairs anchoring each example.This construction addresses the scarcity of large-scale human-generated Lean errors.
  • Mutation error types: Theorem mutations model subtle semantic mismatches by substituting semantically related declarations that differ in required premises or conclusions.Proofs are compiled before retention, so changes that remain correct are excluded; retained theorem mutations also preserve intended and substituted theorem metadata.
  • Mutation error types: Tactic mutations replace tactics only within fixed equivalence classes, such as arithmetic solvers, rewriting, structural, or proof-construction tactics.Examples include swapping nlinarith with linarith, norm_num, or ring.
  • Mutation error types: Line and multi-line mutations redact proof content and use DeepSeek-V3-0324 to generate replacements, limiting multi-line redaction to at most half the proof.Only generated mutations that fail to compile are retained, and duplicates are removed.
  • Training format and objective: Training prompts concatenate the prover error, local proof state, and failing proof, while supervised targets encourage explicit diagnostic reasoning before code generation.The same supervised finetuning pipeline with LoRA is applied across the listed base models.

4 APRIL

APRIL is built from compiled Lean proofs by injecting controlled mutations to create compiler-grounded repair examples. It pairs each failure with aligned proof, diagnostic, repair, and explanation targets while preventing theorem-level leakage across splits.

  • Correct Proof Sources: 39,492 compiled theorems from Herald, Lean Workbook, and NuminaMath-Lean form APRIL’s source pool, retaining proofs that compile under Lean 4.22.0-rc4.Herald contributes approximately 40.5%, Lean Workbook 24.0%, and NuminaMath-Lean the remainder across autoformalized and human-annotated proofs.
  • Generated Incorrect Proofs: 260,125 incorrect proofs are generated through theorem substitution, tactic replacement, line-level modification, and multi-line modification, each producing a concrete compiler error trace.The mutated Lean files remain syntactically valid but fail to compile.
  • Dataset Instances: Each instance includes the correct proof, mutated proof, compiler error and local goal state, repaired proof target, and feedback-aligned explanation with fix suggestion.These fields connect the observed failure to both a repair target and a natural-language diagnosis.
  • Generated Incorrect Proofs: 59.5% of incorrect proofs use theorem substitution, making it the largest mutation category and reflecting prevalent type- and goal-mismatch failures.Mutation categories also include line, multi-line, and tactic mutation errors.
  • Data Splits: Splitting by original theorem keeps all mutations together, while canonical theorem identifiers and stratification preserve source, proof-length, and mutation-type distributions without exposing duplicate proofs across splits.The anonymized identifier is lean_problem.

5 Results

APRIL substantially improves single-shot Lean proof repair across models and heterogeneous error types, with finetuned models outperforming strong baselines. Joint repair-and-explanation training preserves broad repair performance while trading some pass@1 for interpretable diagnoses.

  • Evaluation protocol: Evaluation covers 1,835 erroneous proofs across four mutation types, counting repairs that compile under Lean 4.22.0-rc4 in a single-shot interface.Comparisons use base Qwen3-4B-Instruct and Goedel-Prover models without search or iteration.
  • Overall repair accuracy: 27.4% repair accuracy is achieved by finetuned Qwen3-4B-Instruct, up from 1.1% (25×), slightly exceeding Goedel-Prover-V2-32B at 26.8%.Finetuned 8B models reach 31–35% and outperform the 32B Goedel baseline.
  • Error-type breakdown: 42.5% is the highest repair rate for tactic mutations, whereas line mutations are most difficult, reaching a maximum accuracy of 13.5%.The passage attributes tactic performance to the relatively local nature of those errors; theorem mutations have intermediate difficulty.
  • Joint training: Joint training on all mutation types maintains competitive category-level accuracy, with only modest differences from separately specialized models.This limited degradation suggests shared structure among mutation types and repair strategies that generalize across heterogeneous errors.
  • Explanation ablation: 31.2% pass@1 is reached by repair-only specialization versus 27.4% with joint explanation supervision, exposing a trade-off between autonomous repair and interpretable diagnoses.The explanations can support human-in-the-loop debugging or downstream tool-using agents.

6 Conclusion

The paper frames Lean proof repair as supervised prediction from failing proofs and compiler feedback, and introduces APRIL to support this task. Supervised finetuning on APRIL improves repair accuracy, with a finetuned 4B model outperforming larger open-source provers in the reported evaluation setup.

  • Lean proof repair is formulated as predicting a corrected, compiling proof from a failing proof and compiler feedback.
  • APRIL pairs erroneous and verified proofs with compiler diagnostics and additional natural-language annotations.
  • Supervised finetuning on APRIL substantially improves repair accuracy.
  • A finetuned 4B model outperforms larger open-source provers under the reported evaluation setup.

A Dataset Description · B Finetuning Setting · C Prompts for Explanation and Fix Suggestion Generation

This section describes APRIL’s split-level dataset reporting, finetuning data format, and prompt protocols for generating explanations and fix suggestions from Lean failures. The prompts constrain outputs to concise JSON responses grounded in proof text, infoview state, errors, and, for tactic mutations, intended-versus-current-line metadata.

  • A Dataset Description: The dataset description reports the number of erroneous proofs for each split.The supplied passage identifies this as Table 4’s purpose but provides no split values.
  • A Dataset Description: Basic dataset statistics are reported separately for each split.The supplied passage identifies this as Table 5’s purpose but provides no statistics.
  • A Dataset Description: Statement source distributions are reported separately by split.The supplied passage identifies this as Table 6’s purpose but provides no distribution values.
  • B Finetuning Setting: The finetuning data format is illustrated with a template.The supplied passage identifies this as Figure 4’s purpose but provides no additional template details.
  • C Prompts for Explanation and Fix Suggestion Generation: DeepSeek generates explanations and fix suggestions for theorem and tactic mutations, while also generating line and multiline mutation errors.The prompts for these protocols are provided in the section that follows.
  • C Prompts for Explanation and Fix Suggestion Generation: The explanation prompt limits diagnosis to the incorrect proof, nearby infoview state, and Lean’s error message.It asks the model to explain failure and correction using only those inputs, then return a JSON object with explanation and fix_suggestion fields.
  • C Prompts for Explanation and Fix Suggestion Generation: For tactic mutations, the prompt supplies intended-versus-current-line metadata and asks explanations to consider multiple tactic failures, even when the compiler reports only the first.The requested output contrasts the incorrect and intended lines and includes fixes for all errors when multiple errors exist.

C.1 Line Mutation Errors

Line mutation errors are generated by redacting one line from a Lean 4 proof and asking a model to reconstruct exactly that line.

  • Error generation: A single proof line is redacted, and the task is to provide its correct contents.The input contains the broken Lean 4 proof with one line removed.
  • Error generation: Responses must begin with “MY ANSWER,” contain exactly one line, and use no semicolons.The generated response is automatically searched for the answer.

C.2 Theorem Mutation Errors · C.3 Tactic Mutation Errors

The theorem-mutation task asks Lean programmers to diagnose a failing proof by contrasting an incorrect theorem with the intended one, then return a constrained explanation and repair suggestion. The supplied passages do not describe tactic-mutation errors.

  • C.2 Theorem Mutation Errors: The task presents one failing Lean 4 proof for diagnosis.The input includes the incorrect proof, its state or error, and metadata about the theorem substitution.
  • C.2 Theorem Mutation Errors: The metadata identifies the intended correct theorem and the substituted incorrect theorem.This information is provided through a cheatsheet accompanying the proof failure.
  • C.2 Theorem Mutation Errors: The explanation must ground the failure in a contrast between the incorrect and intended theorems.The requested diagnosis is specifically comparative rather than an unconstrained account of the error.
  • C.2 Theorem Mutation Errors: The output must be exactly one JSON object with two fields.The required fields are explanation and fix_suggestion, with no additional fields or code blocks.
  • C.2 Theorem Mutation Errors: The explanation contains 1--3 sentences describing the concrete reason for failure.Both required fields must be non-empty.
  • C.2 Theorem Mutation Errors: The fix suggestion begins by replacing the incorrect name with the correct name and briefly explains why this resolves the mismatch.Its prescribed opening is: Replace (incorrect_name) with (correct_name).

D Unsuccessful Attempts for Data Synthesis

The authors tested alternative error-generation and repair strategies to obtain diverse, realistic Lean failures, but found limitations in diversity, contextual fidelity, controllability, scalability, or repair validity. These failures motivated the final dataset construction pipeline.

  • Error generation: Directly prompting models to introduce “interesting” errors produced low-diversity, superficial modifications that rarely stressed semantic proof-state reasoning.Increasing sampling temperature did not resolve the tendency to repeat a small set of modifications.
  • Error generation: Single-line natural-language translation generated unrealistic errors because removing formal logic and theorem context impaired reconstruction.Translating the entire proof restored context but produced outputs considered too dissimilar from the original proof.
  • Error generation: Translation through Rocq or Lean 3 failed to produce realistic Lean errors, either altering proofs substantially or yielding simplistic errors unlike typical theorem-proving mistakes.The passage reports unsuccessful attempts with both alternative assistants.
  • Error generation: Prompting models to introduce controlled errors from common Lean pitfalls yielded largely unusable outputs, often ignoring the specified pitfall despite explicit categories and structural constraints.Examples included misuse of have for data extraction, rewriting under binders, and confusing b > a with a < b.
  • Error generation: Random multi-line redaction failed because models ignored following Lean code, causing “no goals to solve” errors, indentation problems, and other syntax issues.These problems persisted even with more powerful models.
  • Proof repair: A prover-based repair pipeline rarely produced valid repairs because Goedel-Prover-V2-8B typically rewrote proofs from scratch and substantially changed their structure and reasoning.The pipeline first used Kimina-Prover-Distill-1.7B to generate proofs, then passed unverifiable outputs to Goedel-Prover-V2-8B.

E Data Synthesis Expanded

The expanded synthesis pipeline generates realistic Lean failures through theorem, tactic, and line mutations applied to proofs known to compile. These mutations target semantic, syntactic, and proof-state mismatches while retaining metadata or controlled redactions for repair and explanation.

  • Theorem Mutation Errors: Theorem mutations replace one used theorem with a semantically related but type-incompatible declaration, targeting subtle mismatches in types, hypotheses, or goals.Proofs known to compile are decomposed into separate (proof, theorem) candidates, and replacements can cause errors to surface far from the mutation site.
  • Theorem Mutation Errors: LeanExplore retrieves up to 5 nearest semantic neighbors, after filtering trivial replacements, and one alternative is randomly sampled for substitution.LeanExplore combines symbolic features and learned embeddings to find conceptually related Lean 4 declarations despite differing names or namespaces.
  • Tactic Mutation Errors: Tactic mutations substitute tactics only within fixed role-based equivalence classes, such as arithmetic solvers, rewriting, structural, and proof-construction tactics.For example, nlinarith may be replaced by linarith, norm_num, or ring to create syntactically valid but potentially failing proof states.
  • Tactic Mutation Errors: For each compilable proof, between 1 and 3 swappable tactic occurrences are randomly selected and substituted, while original and substituted lines plus line numbers provide explanation context.Only unique proofs that fail to compile are retained.
  • Line Mutation Errors: Line mutations redact one proof line after the main by and prompt DeepSeek-V3-0324 to generate code that restores compilation.The original indentation is preserved during redaction.
Loading 2602.02990v2…