LeanPRM
Lean-Grounded Process Supervision
for Natural Language Proof Verification

Rodney Lafuente-Mercado^*1 Salman Rahman^*2,3 Jingyan Shen³ James Shiffer² Saadia Gabriel² Pavel Izmailov³

* Equal contribution

¹ UT Austin² UCLA³ NYU

Summary

AI systems now write long proofs. Checking them means checking every step, and the step labels needed to train a checker are expensive to get from people. LeanPRM gets them from Lean. A model writes each proof twice, as prose and as Lean tactics, Lean checks the tactics, and the natural-language steps inherit the result.

The corpus has 10,634 proofs with 152,005 labeled steps and no human annotation. A Qwen3-4B verifier trained on it scores 74.7% on our held-out benchmark, against 60.3% for the same model trained on PRM800K, and it beats the PRM800K verifier on four of five benchmarks. The verifier reads plain proofs. Lean is only used to build the data.

10,634Proofs

152,005Labeled steps

200Benchmark proofs

How it works

1WriteA model is given a theorem and asked to prove it. Each step is a sentence of prose paired with the Lean tactic that carries it out. It never sees the compiler, so its mistakes are real mistakes.

2CheckLean checks the tactics in order. If one fails, that step and everything after it is wrong. If all of them pass, the proof is correct.

3SortSome failures are just bad Lean, not bad math. A second model reads the compiler output, repairs pure syntax once, and keeps only failures where the mathematics is at fault.

The LeanPRM pipeline: a paired proof attempt, Lean checking, a review of the first failure, and a verifier trained on the natural-language steps. — The pipeline on one proof. Lean finds the first failing step, the reviewer confirms it is a mathematical error, and the verifier trains on the prose with those labels.

A labeled proof

The proof from the figure above, as the verifier sees it. Click a step to see the Lean behind it and what the checker decided.

Theorem (NuminaMath). In a finite group where every automorphism is a power map x ↦ x^m, any two elements commute.

theorem number_theory_65878 {G : Type*} [Group G] [Finite G]
    (h : ∀ f : G ≃* G, ∃ m : ℕ, 0 < m ∧ ∀ x : G, f x = x ^ m) :
    ∀ x y : G, x * y = y * x

1Fix two arbitrary elements x and y of G; our goal is to prove that x·y = y·x.✓
Lean tactic
```
intro x y
```
Lean
Compiles. The sentence and the tactic say the same thing, so the step is labeled correct.
2Conjugation by y is an automorphism of G, so by hypothesis there is a positive integer m for which conjugation by y sends every element z to z^m.✓
Lean tactic
```
obtain ⟨m, hm_pos, hm⟩ := h (MulAut.conj y)
```
Lean
Compiles. The sentence and the tactic say the same thing, so the step is labeled correct.
3Applying this power description to the element x and writing out conjugation explicitly, we obtain y·x·y⁻¹ = x^m.✓
Lean tactic
```
have hyx : y * x * y⁻¹ = x ^ m := by
    have hx := hm x
    rwa [MulAut.conj_apply] at hx
```
Lean
Compiles. The sentence and the tactic say the same thing, so the step is labeled correct.
4Multiplying both sides of y·x·y⁻¹ = x^m on the right by y and cancelling y⁻¹·y to the identity gives y·x = x^m·y.✓
Lean tactic
```
have hyx2 : y * x = x ^ m * y := by
    rw [← hyx]; group
```
Lean
Compiles. The sentence and the tactic say the same thing, so the step is labeled correct.
5We now claim that x^m = x by asserting that conjugating x by y returns x itself, that is y·x·y⁻¹ = x, and therefore the power x^m must coincide with x.✗
Lean tactic
```
have keyx : x ^ m = x := by
    have hxx := hm x
    rw [MulAut.conj_apply] at hxx
    rw [← hxx]; group
```
Lean and reviewer
Nothing earlier shows that conjugating x by y gives back x. That is the claim being proved, so this step assumes its own conclusion. Lean rejects it, and the reviewer confirms the problem is the mathematics, not the encoding.
6Therefore x·y = x^m·y by the claim x^m = x, and x^m·y = y·x because y·x = x^m·y; chaining these equalities shows x·y = y·x, so x and y commute.✗
Lean tactic
```
calc x * y = x ^ m * y := by rw [keyx]
    _ = y * x := by rw [hyx2]
```
Lean and reviewer
Correct on its own terms, but it rests on step 5, so it is labeled incorrect too. Every step after the first error gets this label.

Steps 1 to 4 are correct, steps 5 and 6 are not. The verifier is trained to reproduce exactly this labeling from the prose alone.

Results

We train Qwen3-4B with GRPO for 500 updates on LeanPRM and compare it with the same recipe on two other datasets. One is PRM800K, 800K human step labels. The other trains the model to solve NuminaMath problems with a final-answer reward, to test whether getting better at math makes a better checker. Scores are means over three seeds. Commercial models were prompted with the same instructions.

ModelQwen3-4B, 500 updates	LeanPRM-Benchexact	Hard2Verifybalanced acc.	ProcessBenchavg. F1	PRMBenchfirst error	IMO-GradingBenchbalanced acc.
Qwen3-4B (initial policy)	48.2	37.1	74.3	42.5	53.8
NuminaMath-Solver-4B	48.3	33.6	71.2	41.5	52.4
PRM800K-Verifier-4B	60.3	63.1	83.0	43.3	57.0
LeanPRM-Verifier-4B (ours)	74.7	72.8	74.9	47.4	66.4
Claude Sonnet 5	71.7	83.1	84.9	48.6	80.7
Claude Opus 5	80.3	81.0	84.5	47.6	81.8
Claude Fable 5.1	78.3	86.0	84.7	48.6	85.4
GPT-5.6 Sol	75.3	85.5	79.8	47.1	83.2

LeanPRM-Bench is exact step-label accuracy on 200 held-out proofs. Underlined values are the best of the four trained or untrained 4B models. Hard2Verify, ProcessBench, PRMBench and IMO-GradingBench are external benchmarks the verifier never trained on.

What we found

+14.4 Lean labels beat human labels. Against the PRM800K verifier, LeanPRM wins by 14.4 points on LeanPRM-Bench, 9.7 on Hard2Verify and 9.4 on IMO-GradingBench. PRM800K keeps ProcessBench, whose short solutions come from its own training distribution.
no gain Solving is not verifying. The model trained to solve problems gets much better at solving them, from 30% to 47.5% on its own validation set, and no better at checking proofs.
35.9% The verifier picks better proofs. Choosing among 16 candidate IMO proofs with LeanPRM lands on a correct one 35.9% of the time, against 32.4% at random. The PRM800K verifier accepts almost everything and stays at chance.
0.6B to 8B It works at every size we tried. Training on LeanPRM helps 0.6B, 4B and 8B models on LeanPRM-Bench, Hard2Verify and IMO-GradingBench. The 4B and 8B verifiers end up close, at 74.7 and 75.0 on LeanPRM-Bench.

Limits

The labels still pass through a model. It decides whether a failure is mathematical and whether the prose matches the Lean, and our audits of those decisions use a model too. All the wrong proofs are mistakes Claude made while trying to be right, which is a narrower set of errors than a checker will meet in the wild.

Code, data and the benchmark are linked at the top. The paper has the full details.