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)

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

Selection Effects in Conditional Editing (Table 2)

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)

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)

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.