LeanPRM: Lean Labels 152,000 Proof Steps Without Humans and Lifts Accuracy to 74.7%

Verifying the long math proofs that language models write is becoming a bottleneck. The authors of LeanPRM propose getting step-by-step labels from the Lean proof assistant, with no annotators. The result is a dataset of 10,634 proofs and 152,000 labeled steps. A Qwen3-4B verifier trained on it raised its exact step-label match on the held-out LeanPRM-Bench set (200 proofs) from 48.2 to 74.7. The same base model trained on PRM800K scored 60.3.

Where the labels come from

A process reward model (PRM) can only be trained on data where every step carries a "correct" or "incorrect" label. For open-ended proofs, such labels are hard to get. Human annotators are expensive. Labels derived from a final answer don't help, because a proof has no number to check the result against. Formalizing every proof in Lean requires expert work.

LeanPRM gets around these limits as follows. A model writes a proof in natural language and, in parallel, a formal proof, without any feedback from Lean. Lean then checks the formal version and labels each step. A second model filters out cases where the failure comes only from the syntax of the formal text. After that, the negative labels reflect genuine mathematical errors, not transcription slips.

What the numbers show

Main results from the paper:

• dataset: 10,634 proofs, 152,000 labeled steps, no manual labeling;
• LeanPRM-Bench (200 held-out proofs): Qwen3-4B rose from 48.2 to 74.7 exact step-level match;
• PRM800K baseline on the same model: 60.3;
• on three of four external benchmarks, the LeanPRM-trained verifier beats the PRM800K-trained one;
• in best-of-N selection on IMO-level problems, it picks higher-quality proofs;
• the gain is confirmed on models from 0.6B to 8B parameters across LeanPRM-Bench, Hard2Verify and IMO-GradingBench.

The consistency of the effect across model sizes matters as much as the headline number. The improvement shows up in a very small model and in an eight-billion-parameter one. That suggests the gain comes from the quality of the signal, not from a lucky choice of a single configuration.

Where to look more closely

The main gap, 48.2 versus 74.7, was measured on a benchmark the authors built themselves, using the same generation and labeling procedures. LeanPRM training has a natural advantage on such a set. That makes the external tests more valuable, and there the gain appears on three of four benchmarks, so not everywhere. The paper, as summarized here, does not explain the result on the fourth, and it is worth checking in the full text.

There is also a structural limitation. The labels are only as correct as the match between the formal proof and the natural-language one. If the model wrote a formal version that diverges from the text, Lean will grade something other than what a human reads. The second-model filter reduces the risk of syntax noise but does not guarantee that the two versions fully correspond. Coverage is limited too: only what could be formalized can be labeled.

The practical value lies in scaling. The volume of data grows with the number of available formal statements, not with the budget for experts. For teams training math models with best-of-N or RL on process rewards, this offers a way to get a dense signal on reasoning steps without buying annotation. To assess the approach, run your own verifier on Hard2Verify and IMO-GradingBench. It is also worth checking how well the gain holds on proofs from areas far from those formalized in Lean.