LeanPolish releases verified Lean edits and tests proof compression

A paper introduces LeanPolish, a symbolic pipeline for Lean 4 that uses verified proof edits as supervision for improving language-model-generated proofs. Its release includes 33,402 accepted local edits and 65,596 failed attempts from the same proof states, giving researchers both successful and unsuccessful candidates to study. The authors use the collection to examine what models learn from this supervision, rather than treating verification alone as evidence that the training signal is reliable.

The paper identifies a potential evaluation trap: a search procedure that stops at its first successful edit can make a goal-independent rule appear to rank candidates perfectly. It also finds that evaluation sites selected by a teacher can reward deletions that are trivial. To address the ranking shortcut, the researchers continue evaluating candidates beyond the first success. On held-out states, a trained ranker then chooses the best candidate 70.1% of the time, compared with 36.9% for the strongest frozen baseline.

For proof compression, repeatedly applying the symbolic pass increases savings on miniF2F from 19.7% to 27.5%, exceeding the neural hybrid methods tested on that benchmark. The paper also reports results from verified neural editing on other proof sources, but says comparisons with matched frozen models indicate that gains there do not necessarily result from training. That distinction cautions against attributing every improvement from a verified edit process to learned behavior.

In a whole-proof rewriting test, fine-tuning raises verified token reduction from 2.8% to 5.5% across 19 PutnamBench proofs. The authors present the released edits, complete candidate pools and controlled evaluations as a reproducible way to examine proof improvement while keeping correctness, compression and edit policy distinct. For AI builders, the reported results show why evaluations should account for how candidate edits are generated and selected, not just whether the final proof verifies.