LeanPRM: Lean-Grounded Supervision for Natural Language Proof Verification

AI systems now write long and difficult mathematical proofs, and checking their 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 Lean-PRM, 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, and we release a held-out benchmark, LeanPRM-Bench. A Qwen3-4B verifier trained on Lean-PRM raises exact step-label accuracy on LeanPRM-Bench from 48.2 to 72.5, as opposed to 59.5 when the same base model is trained on PRM800K. It also selects better proofs in best-of-N selection on IMO-level problems, and leads on 3 of 4 external 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 people to check.