# LeanPolish: Verified Supervision for Lean Proof Compression

arXiv: https://arxiv.org/abs/2609.38384 · HTML: https://mlsanity.com/paper/2609.38384/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 22 of its 41 references that are in the map.
- First posted on arXiv 29 Sep 2026.

## Builds on (most cited first, 22 of 22)

- [Direct Preference Optimization: Your Language Model is Secretly a Reward Model](https://mlsanity.com/paper/2305.18290/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Learning Performance-Improving Code Edits](https://mlsanity.com/paper/2302.07867/) (2023)
- [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://mlsanity.com/paper/2502.03438/) (2025)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning](https://mlsanity.com/paper/2505.05758/) (2025)
- [Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving](https://mlsanity.com/paper/2404.07382/) (2024)
- [ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations](https://mlsanity.com/paper/2510.15700/) (2025)
- [ImProver: Agent-Based Automated Proof Optimization](https://mlsanity.com/paper/2410.04753/) (2024)
- [Anti-unification and Generalization: A Survey](https://mlsanity.com/paper/2302.00277/) (2023)
- [Learning to Repair Lean Proofs from Compiler Feedback](https://mlsanity.com/paper/2602.02990/) (2026)
- [Process-Verified Reinforcement Learning for Theorem Proving via Lean](https://mlsanity.com/paper/2606.20068/) (2026)
- [AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities](https://mlsanity.com/paper/2606.26442/) (2026)
- [Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts](https://mlsanity.com/paper/2606.03743/) (2026)
- [BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints](https://mlsanity.com/paper/2607.28110/) (2026)

## Abstract (arXiv)

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.