LeanPolish: Verified Supervision for Lean Proof Compression
Pauline Bourigault
cs.LG
Sep 29, 2026 · v1
TL;DR
Builds a symbolic Lean 4 pipeline using InfoTree proof states to generate verified local proof-compression edits, then trains and evaluates LLM editors on them.
Abstract
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 admits a goal-independent rule with perfect ranking accuracy; teacher-selected evaluation sites also reward trivial deletions. 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 helps on other proof sources, but matched frozen-model controls show that its gains need not come from training. The supervision does improve whole-proof rewriting: fine-tuning raises verified token reduction from 2.8% to 5.5% on 19 PutnamBench proofs. 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.
Problem
LLM-generated Lean proofs are often verbose, and recent systems learn to shorten them from verified search outputs. A kernel check shows an edit is correct but does not show that the training signal is free of search artifacts such as first-success ordering or teacher-selected evaluation sites.
Approach
LeanPolish is a symbolic Lean 4 pipeline that uses the InfoTree to test candidate tactics at saved proof states. It runs four phases (goal-closing tactic replacement under a specificity filter, local-fact anti-unification, unused-fact removal, and unreachable-code cleanup), re-checks each edited file, and iterates to a fixed point. It releases accepted local edits together with same-state failed attempts and complete candidate pools. These are used to train rankers and 7B editors, which are compared against frozen-model, iterated-symbolic, and few-shot controls.
Results
The released data contain 33,402 accepted edits and 65,596 failed siblings. With complete-menu evaluation, a trained ranker picks the best candidate on 70.1% of held-out states, versus 36.9% for the strongest frozen baseline. Iterating the symbolic pass raises miniF2F token savings from 19.7% to about 27.5%, and fine-tuning raises verified whole-proof token reduction on 19 PutnamBench proofs from 2.8% to 5.5%.
| Method | Top-1 (%) |
|---|
| First in menu order | 11.6 |
| Frozen DeepSeek-7B log-prob | 36.9 |
| Trained ranker, no goal | 51.0 |
| Trained ranker | 70.1 |
| Ref.: verifier, first success | 76.9 |
Top-1 best-candidate selection on held-out complete-menu states
