ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
This addresses a critical bottleneck in neural theorem proving by making proofs more comprehensible and efficient for mathematicians and AI systems, though it is incremental as it builds on existing RL-trained provers.
The paper tackles the problem of excessively long and hard-to-understand proofs generated by neural theorem provers by introducing ProofOptimizer, a language model trained to simplify Lean proofs without human supervision, resulting in reductions of proof length by up to 87% on benchmarks like miniF2F.
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.