ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations

TL;DR

ProofOptimizer tackles the problem that state-of-the-art neural provers in Lean produce correct but exceedingly long proofs, limiting human insight and practical reuse. The authors train a 7B Lean-focused model for proof simplification via two regimes—Expert Iteration and Online Reinforcement Learning—together with a symbolic Lean linter and an iterative inference-time shortening loop. They formalize proof simplification as minimizing a deterministic complexity measure $\mathcal{L}$ (taken as Lean token length $|x|$) and introduce metrics $\text{min@k}$ and $\text{red@k}$ to evaluate shortfall and relative reduction. Across MiniF2F, PutnamBench, and Seed-Prover IMO 2025 proofs, ProofOptimizer achieves substantial reductions (e.g., averages of $87\%$ on MiniF2F and $57\%$ on PutnamBench with iterative shortening), faster Lean execution for many shortened proofs, and improved downstream learning when training on simplified proofs. The work demonstrates that training-time proof simplification, augmented by inference-time strategies and execution feedback, can meaningfully narrow the gap between formally verified rigor and human-readable mathematical reasoning, with practical impact for library-building and automated proof synthesis.

Abstract

Neural theorem proving has advanced rapidly in the past year, reaching IMO gold-medalist capabilities and producing formal proofs that span thousands of lines. Although such proofs are mechanically verified by formal systems like Lean, their excessive length renders them difficult for humans to comprehend and limits their usefulness for mathematical insight. Proof simplification is therefore a critical bottleneck. Yet, training data for this task is scarce, and existing methods -- mainly agentic scaffolding with off-the-shelf LLMs -- struggle with the extremely long proofs generated by RL-trained provers. We introduce ProofOptimizer, the first language model trained to simplify Lean proofs without requiring additional human supervision. ProofOptimizer is trained via expert iteration and reinforcement learning, using Lean to verify simplifications and provide training signal. At inference time, it operates within an iterative proof-shortening workflow, progressively reducing proof length. Experiments show that ProofOptimizer substantially compresses proofs generated by state-of-the-art RL-trained provers on standard benchmarks, reducing proof length by 87% on miniF2F, 57% on PutnamBench, and 49% on Seed-Prover's IMO 2025 proofs. Beyond conciseness, the simplified proofs check faster in Lean and further improve downstream prover performance when reused as training data for supervised finetuning.

Figures (22)

• Figure 1: Overview of our pipeline. ProofOptimizer reduces the shortest generated proof of a Putnam problem from 1097 to 76 tokens.
• Figure 2: miniF2F (train)
• Figure 3: Putnam (train)
• Figure 4: miniF2F (test-time)
• Figure 5: Putnam (test-time)