cs.LGOct 13, 2026
SaveLeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification
Organizations: University of Texas at Austin · University of California, Los Angeles · New York University
Abstract
AI systems now write long and difficult mathematical proofs, and checking their step-by-step validity is becoming a bottleneck. A learned verifier could check proofs cheaply, but training one requires a correctness label on every step, and such labels are hard to obtain for open-ended proofs. Existing methods take them from human annotators, which is costly, or derive them from final answers, which proofs do not have, and formalizing each proof in Lean requires expert effort. We introduce LeanPRM, a framework that uses the Lean proof assistant to create step-level labels for natural-language proofs. A model writes a natural-language proof together with a paired formal proof, without feedback from Lean. Lean then labels every step, and a second model discards failures caused only by the formal syntax, so that the negative labels mark errors in the mathematics. LeanPRM contains 10,634 proofs with 152K labeled steps and no human annotation. A Qwen3-4B verifier trained on LeanPRM raises exact step-label accuracy on a held-out set of 200 proofs (LeanPRM-Bench) from 48.2 to 74.7, as opposed to 60.3 when the same base model is trained on PRM800K. It also selects better proofs in best-of-N selection on IMO-level problems, and outperforms the PRM800K-trained verifier on three of four external verification benchmarks. Training on LeanPRM improves verifiers at every size from 0.6B to 8B parameters on LeanPRM-Bench, Hard2Verify and IMO-GradingBench. Given the labels need no human annotation, LeanPRM can grow with the supply of formal statements, offering a path to step-level feedback on AI-generated proofs that are hard for humans to check.
Figures & tables
Figure 1: Overview of LeanPRM, with one example from the corpus running through it. Top row: Stage 1 writes a proof attempt from the theorem statement alone, each natural-language step paired with its formal step, and Lean checks the steps in order. Bottom row: Stage 2 decides whether the first failure lies in the mathematics or only in the formal syntax (syntax failures are patched and rechecked once), and the verifier is trained on the natural-language steps and their labels only. Here step 5 asserts without justification that conjugation by fixes , so steps 1 to 4 are labeled correct and steps 5 and 6 incorrect.
Figure 2: Composition of LeanPRM. Left: sources of the 10,634 theorems. Right: error class of the first failing step in each of the 4,264 incorrect proofs. Bars show percentages of incorrect proofs. Every incorrect proof fails first at a mathematical error, most often an unjustified assumption.
| First-error class | Judged sound | Share of errors |
| Formalization-side | ||
| Wrong rewrite direction | ||
| Theorem misapplication | ||
| Other | ||
| Automation misuse | ||
| Mathematical | ||
Table 1: Blind audit of flagged steps, 30 per class (all formalization-side classes and the two largest mathematical ones). Judged sound : correct and justified. Share of errors : fraction of incorrect proofs in the unfiltered pool. Formalization-side steps are mostly sound. Mathematical steps are mostly not sound.
| LeanPRM-Bench | Hard2Verify | ProcessBench | PRMBench | IMO-GB | |
| exact | response BA | avg. F1 | first err. | BA | |
| Qwen3-4B (initial policy) | 48.2 1.3 | 37.1 4.5 | 74.3 0.5 | 42.5 0.5 | 53.8 0.1 |
| PRM800K-Verifier-4B | 60.3 1.6 | 63.1 0.6 | 83.0 0.3 | 43.3 0.3 | 57.0 0.4 |
| NuminaMath-Solver-4B | 48.3 1.0 | 33.6 3.4 | 71.2 0.9 | 41.5 0.2 | 52.4 0.4 |
| LeanPRM-Verifier-4B (ours) | 74.7 1.8 | 72.8 0.9 | 74.9 0.4 | 47.4 0.2 | 66.4 1.1 |
| LeanPRM-Verifier-4B † | 78.7 1.3 | 79.0 0.7 | 72.6 0.3 | 48.3 0.2 | 71.8 1.0 |
Table 2: Verification accuracy. Open-weight models use temperature 1. Commercial-model settings are given in Appendix E . LeanPRM-Bench is scored by exact step-label accuracy (Section 2.2 ), and the other columns use the metrics of Section 3 . The top block compares 4B models trained for 500 updates with the same recipe, with the untrained model for reference, and bold marks the best value in that block. The bottom block holds reference rows: † a separate 4B run of 1,582 updates, only the last 300 of them on LeanPRM (Appendix D ), and commercial models prompted rather than trained for the task. At equal training, LeanPRM-Verifier-4B is best on four of the five benchmarks. Entries report mean population standard deviation over three evaluation runs (Appendix E ).
Figure 3: The top block of Table 2 per benchmark: 4B models trained for 500 updates with the same recipe, and the untrained model. Bars are means over three decoding seeds with one standard deviation as error bars. LeanPRM-Verifier-4B is best on four of the five benchmarks and PRM800K-Verifier-4B on ProcessBench.
Figure 4: Training curves and test-time selection. Left: exact step-label accuracy on the LeanPRM validation split during training, for the verifiers trained from Qwen3 base models of three sizes; the 4B point at update 300 was measured separately with the same greedy protocol. Middle: the two trained baselines on their own validation splits, PRM800K-Verifier-4B by exact accuracy and NuminaMath-Solver-4B by final-answer accuracy; both change little over the second half of training. Right: best-of- selection on IMO-GradingBench, the share of selected proofs graded correct, averaged over the 30 problems and three decoding seeds (shaded band: one standard deviation); the dotted line is random selection. LeanPRM-Verifier-4B picks better proofs as grows, while PRM800K-Verifier-4B stays near chance.
Figure 5: Accuracy before and after training on LeanPRM, by model size. Each panel is one benchmark; open circles are the untrained Qwen3 models and filled circles the trained verifiers after 500 updates. Training improves every model on LeanPRM-Bench, Hard2Verify and IMO-GradingBench; the untrained 0.6B model scores near zero on three benchmarks because it rarely produces well-formed labels. Points and error bars show the mean and population standard deviation over three decoding seeds.
| Method | Step labels from | No human step labels | Open-ended proofs | Error classes | Trained verifier |
| PRM800K ( Lightman et al., 2023 ) | Human annotators | ✗ | ✗ | ✗ | ✓ |
| Math-Shepherd ( Wang et al., 2023 ) | Rollouts | ✓ | ✗ | ✗ | ✓ |
| OmegaPRM ( Luo et al., 2024 ) | Rollouts (tree search) | ✓ | ✗ | ✗ | ✓ |
| FoVer ( Kamoi et al., 2025 ) | Z3, Isabelle | ✓ | ✗ | ✗ | ✓ |
| Safe ( Liu et al., 2025 ) | Lean 4 | ✓ | ✗ | ✗ | ✗ |
| TP-as-a-Judge ( Leang et al., 2025 ) | Lean 4 (per solution) | ✓ | ✗ | ✗ | ✗ |
Table 3: Sources of step-level labels in prior work and in LeanPRM. For each method we give the origin of its step labels and whether they avoid human annotation, cover open-ended natural-language proofs, give each failing step a mathematical error type, and train a verifier that reads the proof text. Only LeanPRM does all four.
Appendix figures & tables9 assets
Supplementary material from the paper’s appendix.
Appendix
| Correct | Incorrect | Total | |
| NuminaMath | 1,334 | 3,978 | 5,312 |
| Lean-Workbook | 4,787 | 284 | 5,071 |
| Pythagoras | 230 | 1 | 231 |
| Herald | 13 | 1 | 14 |
| ProofNet | 6 | 0 | 6 |
| Training | 6,170 | 4,094 | 10,264 |
Table 4: Size of LeanPRM by source (top) and by split (bottom); each theorem contributes one proof. NuminaMath supplies most of the incorrect proofs and Lean-Workbook most of the correct ones.
Figure 6: A proof the trained verifier labels exactly and no commercial system does. Step 5 asserts, by an unelaborated strong induction, that any smooth set of numbers yields at least disjoint pairs with equal parity vectors; the argument as written does not justify the count, the checker fails at this step, and the class is unjustified assumption. Sonnet 5, Fable 5.1 and PRM800K-Verifier-4B accept every step, Opus 5 and GPT-5.6 Sol first object at step 6, and LeanPRM-Verifier-4B † flags step 5.
Figure 7: An incomplete proof. The argument establishes the summed inequality and defines at step 19, then stops without producing the two distinct zeros. Under the convention of Section 2 the final step of an argument that stops short is incorrect; every other system accepts all nineteen steps, and LeanPRM-Verifier-4B † flags the last.
Figure 8: The reverse case. Step 8 claims a Lagrange-type identity with the wrong coefficient on the first square, so the checker’s ring normalization fails and the class is algebraic identity error. All four commercial systems and PRM800K-Verifier-4B flag step 8; LeanPRM-Verifier-4B † accepts the proof.
| LeanPRM-Bench | Hard2Verify | ProcessBench | PRMBench | IMO-GB | |
| exact | response BA | avg. F1 | first err. | BA | |
| Qwen3-0.6B base | 22.7 0.2 | 3.6 1.7 | 3.2 0.2 | 3.5 0.5 | 48.4 0.2 |
| Qwen3-4B (initial policy) | 48.2 1.3 | 37.1 4.5 | 74.3 0.5 | 42.5 0.5 | 53.8 0.1 |
| Qwen3-8B base | 45.7 1.9 | 52.4 1.2 | 79.5 0.3 | 47.6 0.2 | 58.4 0.6 |
| LeanPRM-Verifier-0.6B | 54.0 2.5 | 61.8 1.8 | 34.9 1.0 | 27.7 0.2 | 58.4 1.8 |
| LeanPRM-Verifier-4B | 74.7 1.8 | 72.8 0.9 | 74.9 0.4 | 47.4 0.2 | 66.4 1.1 |
Table 5: Model scale at a fixed budget: LeanPRM verifiers trained from Qwen3 base models of three sizes for 500 updates each with the same recipe, with the untrained models for comparison; mean population standard deviation over three decoding seeds. The 4B and 8B models are close on LeanPRM-Bench, PRMBench and IMO-GradingBench, and the 0.6B model is far behind.
Figure 9: A correct attempt: for real , . Every step elaborates, so every step is labeled correct. The argument is the standard completion of the square, written as four claims each realized by one tactic. Attempts of this kind account for 6,370 of the 10,634 theorems in LeanPRM.
Figure 10: A reasoning error whose text shows the slip. The statement asks, for and every bound , for some dividing the sum of the -th powers of its divisors. The attempt proposes , which cannot exceed an arbitrary , and step 4 concedes as much while trying to discharge the bound anyway. Elaboration fails at that step; Stage 2 assigns the class invalid inequality bound, and steps 4 and 5 are labeled incorrect.
Figure 11: An attempt from the labeled pool that is not part of LeanPRM. The statement is that implies . Step 3 invokes the true fact that divides ; the mathematics is sound, but the Lean line names the library lemma in a form the pinned Mathlib does not accept, so elaboration fails there and Stage 2 assigns theorem misapplication. The audit judged steps of this class sound in 26 of 30 cases, which is why the formalization-side classes are excluded from the corpus.
| Base models | Qwen3-0.6B, Qwen3-4B, Qwen3-8B, thinking mode enabled |
| Optimizer | GRPO as implemented in VERL, learning rate |
| Batch | 64 prompts per update, 8 responses per prompt |
| Clipping | ratio clipped at 0.20 below and 0.26 above, dual-clip constant 10 |
| Regularization | KL coefficient , low-variance estimator, no entropy bonus |
| Loss aggregation | sequence mean of token means |
| Sequence lengths | 8,192 prompt tokens, 6,656 response tokens |
Table 6: Training configuration shared by every trained model.