Verified proof edits offer a natural source of supervision for improving language-model-generated Lean proofs. Yet verification establishes that an edit is correct, not that its training signal is free of search artifacts.
We introduce LeanPolish, a symbolic Lean 4 pipeline that releases 33,402 accepted local edits and 65,596 same-state failed attempts, and use it to study what models learn from this supervision.
First-success search
First-success search admits a goal-independent rule with perfect ranking accuracy; teacher-selected evaluation sites also reward trivial deletions.
Continuing menu evaluation
Continuing menu evaluation beyond the first success removes the ordering shortcut: a trained ranker selects the best candidate on 70.1% of evaluated held-out states, versus 36.9% for the strongest frozen baseline.
For compression
Iterating the symbolic pass raises miniF2F savings from 19.7% to 27.5%, exceeding the neural hybrids we test there.
Verified neural editing
Verified neural editing helps on other proof sources, but matched frozen-model controls show that its gains need not come from training.
Supervision improves whole-proof rewriting
The supervision does improve whole-proof rewriting: fine-tuning raises verified token reduction from 2.8% to 5.5% on 19 PutnamBench proofs.
Together
Together, the released edits, complete candidate pools, and controlled evaluations separate learning to imitate a search policy from improving on that search.
They provide a reproducible basis for studying proof improvement while keeping correctness, compression, and edit policy distinct.