LeanPRM auto-labels 152K math proof steps via Lean itself

LeanPRM, a preprint from a group that includes Pavel Izmailov and Saadia Gabriel, builds a 152K-step training set for math-proof verifiers with zero human annotators. A model writes a natural-language proof together with a paired Lean formalization; Lean then labels every step, and a second model throws out failures that trace to formal syntax rather than real math errors. The dataset covers 10,634 proofs.

The headline result: a Qwen3-4B verifier trained on LeanPRM raises exact step-label accuracy from 48.2 to 74.7 on a 200-proof held-out set the authors call LeanPRM-Bench. The same base model trained on PRM800K, the human-labeled standard, reaches 60.3.

The authors argue the recipe scales. "LeanPRM can grow with the supply of formal statements," they write, "offering a path to step-level feedback on AI-generated proofs that are hard for humans to check." Gains hold at every size tested from 0.6B to 8B parameters, best-of-N selection improves on IMO-level problems, and the LeanPRM-trained verifier beats the PRM800K-trained one on three of four external verification benchmarks, including Hard2Verify and IMO-GradingBench.

How often the syntax filter fires, and how often it discards a step whose formal failure actually tracked a mathematical error, is not quantified. The abstract notes only that "a second model discards failures caused only by the formal syntax, so that the negative labels mark errors in the mathematics."