# LeanPolish: Verified Supervision for Lean Proof Compression

> Verified proof datasets leak search-order shortcuts that models exploit without learning math, but complete-menu supervision and whole-proof fine-tuning reveal genuine compression gains.

- **Source:** [arXiv](https://arxiv.org/abs/2609.38384)
- **Published:** 2026-10-03
- **Permalink:** https://picx.dev/p/Vo0VI3
- **Whiteboard:** https://picx.dev/p/Vo0VI3/image

## Summary

## Summary (Overview)

- **LEANPOLISH** is a neurosymbolic pipeline for verified Lean 4 proof compression that releases 33,402 accepted local edits and 65,596 same-state failed attempts across multiple proof sources.
- The paper identifies and quantifies **search selection effects** in verified supervision: first-success search admits a goal-independent rule with perfect ranking accuracy, meaning models can exploit search-order shortcuts rather than learning mathematical reasoning.
- A **complete-menu mode** removes the ordering shortcut: a trained ranker selects the best candidate on 70.1% of held-out states, versus 36.9% for the strongest frozen baseline.
- Iterating the symbolic pass to a fixed point raises miniF2F token reduction from 19.7% to 27.5%, **exceeding all tested neural hybrids** on that source.
- Fine-tuning on LEANPOLISH proof pairs raises verified whole-proof token reduction from 2.8% to 5.5% on PutnamBench, demonstrating genuine transfer of learned compression skills.

## Introduction and Theoretical Foundation

### Background and Motivation

Language-model provers now produce kernel-checked Lean 4 proofs for competition problems at scale, but **correctness does not imply conciseness**: search can leave speculative tactic cascades, unused facts, and repeated derivations. Recent systems learn to shorten proofs using verified outputs of search, with the intuition that verified edits show *how to improve* a derivation in a specific context.

### The Core Problem

The paper identifies a fundamental issue: **the search determines which contexts, alternatives, and labels enter the dataset**. A kernel certificate answers "does this edit preserve the theorem?" but not "what must a model learn to predict this edit?" If search stops at its first success, logged failures reveal the winner's position in the search order, creating a shortcut that makes verified datasets appear more informative than their evaluation establishes.

### Theoretical Foundation

The paper distinguishes three separable components:
- **Proposal**: what to try
- **Policy**: which edits to prefer  
- **Verification**: whether the resulting proof still checks

This separation allows the symbolic teacher, its training signal, and its downstream utility to be independently inspectable.

## Methodology

### Symbolic Pipeline (Algorithm 1)

LEANPOLISH processes compiling proofs through four phases:

1. **Tactic replacement**: At every leaf tactic that closes a goal, a fixed menu is tried in order: $rfl$, $ring$, $abel$, $norm\_num$, $norm\_cast$, $positivity$, $decide$, $linarith$, $omega$, $field\_simp$, $contradiction$, $ext$, $gcongr$, $tauto$, $simp?$ (squeezed to $simp\ only\ [\ldots]$). A **specificity filter** prevents replacing explicit-term tactics with more general automation.

2. **Local fact generalization**: Near-duplicate $have$ blocks are anti-unified; differing subterms become parameters of one shared local fact, subject to a **dependency filter** requiring the abstracted proof to depend on strictly fewer local free variables.

3. **Unused-fact removal**: A usage graph identifies $have$ blocks never referenced later.

4. **Unreachable-code cleanup**: Re-elaboration with Lean's default linters removes never-executed tactics from `<;>` chains.

### Verification

- Candidates are tested against saved proof states
- Edited files are re-elaborated and kernel-checked in-process
- Independent `lake env lean` compilation from a fresh Mathlib import for benchmark sources
- Every model output counted as success is checked via fresh-process compilation

### Complete-Menu Search

Stops at first success, then continues through all 15 menu entries, selecting the **shortest successful candidate** allowed by the specificity filter. Records valid candidates, failures, timeouts, policy rejections, and length skips separately—removing first-success censoring.

### Fixed-Point Iteration

The pipeline runs on its own output until no file changes (4–8 rounds), exposing compression unavailable to one-pass baselines.

### Hybrid Compression (Algorithm 2)

Runs LEANPOLISH, then asks a local editor for proposals at every remaining tactic site, verifies each in a fresh Lean process, combines compatible edits, and jointly re-verifies the final file.

## Empirical Validation / Results

### Released Dataset (Table 1)

| Source (generator) | Inputs | Files | Accepted | Failed siblings | Tok. red. (%) |
|---|---|---|---|---|---|
| Mathlib v4.21.0 subset (human) | 5,789 | 2,233 | 6,695 | 26,912 | 0.27 |
| Goedel-Workbook (Goedel-Prover-V2) | 29,750 | 10,052 | 20,822 | 28,525 | 5.48 |
| PutnamBench sample (Goedel-Prover-V2) | 437 | 352 | 4,354 | 5,930 | 8.14 |
| miniF2F verified (Goedel-Prover-V2) | 351 | 308 | 1,184 | 3,753 | 19.72 |
| PutnamBench verified (Goedel-Prover-V2) | 19 | 16 | 80 | 254 | 6.14 |
| Putnam 2025 (AxiomProver) | 12 | 10 | 142/125 | 147/75 | 1.31 |
| **Total** | | **12,972** | **33,402** | **65,596** | |

Edit families: 51.6% deletions, 47.6% tactic replacements, 0.8% local fact generalizations.

### Selection Effects in Conditional Editing (Table 2)

| Method | miniF2F All/Tac. | PutnamBench All/Tac. | Putnam 2025 All/Tac. |
|---|---|---|---|
| Reference (pipeline) | 94.6/91.6 | 88.8/79.1 | 84.5/61.4 |
| Delete rule (no model) | 36.8/0.0 | 46.3/0.0 | 59.9/0.0 |
| DeepSeek, frozen | 0.1/0.1 | 0.0/0.0 | 0.0/0.0 |
| DeepSeek, 4-shot | 36.9/4.7 | 48.8/4.7 | 53.5/0.0 |
| DeepSeek, SFT | 86.7/79.0 | 86.3/74.4 | 79.6/49.1 |
| DeepSeek, DPO | 84.5/75.6 | 85.0/72.1 | 73.2/33.3 |

Key findings:
- Fine-tuned models recover 92–98% of the pipeline's savings at teacher-selected sites
- **Deletion rule alone** (no model) yields 8,122 tokens on miniF2F—deletions are trivially identifiable by a no-goal marker
- Tactic replacement success: 42–79% after fine-tuning vs. 0–18% with four-shot prompting
- Greedy exact match with reference: 82.7–91.5%; **imitation, not improvement**

### Ordering Leakage and Complete Pools (Table 3)

| Method | Top-1 accuracy (%) |
|---|---|
| Last in menu order (biased groups) | 100* |
| Last in menu order (complete pools) | 0.0 |
| Random | 8.2 |
| Frozen DeepSeek-7B log-prob | 36.9 |
| Trained ranker, no goal | 51.0 |
| **Trained ranker** | **70.1** |
| Reference: verifier, first success | 76.9 |

The ordering rule perfect on biased groups selects the best candidate **0%** of the time on complete pools. Goal ablation costs 19.1 points, showing genuine state-dependent information.

### Whole-Proof Improvement (Table 4)

| Method | AxiomProver (12) | PutnamBench (19) | miniF2F-99 |
|---|---|---|---|
| LEANPOLISH, release run | 1.31 | 6.14 | 20.02 |
| LEANPOLISH, clean rerun | 1.41 | 11.91 | 20.52 |
| LEANPOLISH iterated to fixed point | 1.76 | 16.07 | **29.76** |
| LLM rewrite, frozen | 1.04 | 2.76 | 12.52 |
| LLM rewrite, trained | — | 5.53 | 16.36 |
| Hybrid, frozen few-shot | 3.66 | 9.31 | 23.14 |
| Hybrid, trained DeepSeek | 3.65 | 9.02 | 22.41 |
| Hybrid, trained Qwen | 4.00 | 11.38 | — |

Critical controls:
- **Frozen editor achieves as much as trained editor** in hybrid settings
- Iterated symbolic baseline exceeds all neural hybrids on miniF2F
- Training benefit appears only in **whole-proof rewriting**: 2.8% → 5.5% on PutnamBench
- 62% of trained model's samples yield verified shorter files vs. 16% for frozen

## Theoretical and Practical Implications

### Theoretical Contributions

1. **Separation of search and learning**: The paper demonstrates that verified supervision encodes search policy, not just mathematical correctness. First-success search creates datasets where "latest in menu order" is a perfect predictor.

2. **Evaluation protocol**: The complete-menu mode and matched controls (frozen editors, symbolic fixed points, policy compliance checks) provide a template for evaluating proof-compression supervision without conflating gains from training with gains from search or verification.

3. **Policy compliance matters**: 40% of self-training edits violate the specificity filter; restricting to filter-compliant edits changes hybrid results, showing that edit policy is a distinct axis from correctness.

### Practical Implications

- **Symbolic methods remain competitive**: Iterated symbolic compression (27.5% on miniF2F) exceeds neural hybrids, suggesting symbolic passes should be a baseline for future work
- **Training signal quality**: Verified edits are useful for whole-proof rewriting but not necessarily for local editing beyond the teacher's search space
- **Dataset release**: The 33,402 accepted edits, 65,596 failures, and complete pools for ~60,000 states provide a reproducible basis for studying proof improvement

## Conclusion

LEANPOLISH makes proof-improvement supervision inspectable at the level where an edit is proposed and verified. The key takeaways:

1. **A model can reproduce a search procedure's choices without learning to improve on that search**—aggregate accuracy obscures this distinction.

2. **Complete-menu outcomes remove one concrete shortcut**, and goal ablation shows useful state-dependent information in the remaining task.

3. **Whole-proof fine-tuning provides a complementary positive result**: symbolic edits can train models to produce more effective verified rewrites (2.8% → 5.5% on PutnamBench).

4. **Future work should target improving complete proofs beyond strong symbolic and prompted baselines** at a declared computational budget.

The evidence has limits: whole-file comparisons use 12–351 files per source, one trained checkpoint per configuration, and measure length and policy compliance—not human readability or maintenance cost. Within this scope, LEANPOLISH contributes a verified neurosymbolic compression method, its supervision, and a protocol for testing what that supervision teaches: *verification certifies correctness; controlled comparisons show when learning helps*.

---

_Markdown view of https://picx.dev/p/Vo0VI3, served by PicX — AI-generated visual whiteboard summaries of research papers._