TLDR: ProofOptimizer is a new language model designed to simplify lengthy and complex formal mathematical proofs generated by AI provers in Lean. It uses expert iteration and reinforcement learning, verified by Lean itself, to progressively shorten proofs without needing human demonstrations. The system significantly reduces proof length (e.g., 87% on miniF2F) and offers benefits like faster proof checking and improved training data for other provers, outperforming other leading LLMs.
Neural theorem proving has made remarkable strides, with AI systems now capable of generating formal proofs thousands of lines long. While these proofs are mechanically verified by systems like Lean, their sheer length often makes them difficult for humans to understand, limiting their practical value for mathematical insight. This challenge highlights a critical bottleneck: proof simplification.
Addressing this, researchers have introduced ProofOptimizer, a novel language model specifically trained to simplify Lean proofs without requiring additional human supervision. This system represents a significant step forward, especially given that existing methods often struggle with the extremely long proofs produced by state-of-the-art AI provers.
ProofOptimizer is built on three core components: a symbolic Lean linter that identifies and removes obvious redundancies, a 7-billion parameter language model fine-tuned for proof simplification, and an iterative inference-time algorithm that progressively shortens proofs. The training process involves expert iteration and reinforcement learning, where Lean itself verifies the simplifications and provides the necessary feedback for the model to learn and improve continuously.
At inference time, the process begins with the Lean linter cleaning up the initial proof. The language model then generates multiple potential simplifications. The iterative algorithm repeatedly applies the model to the shortest correct proof found so far, gradually reducing its length. This iterative approach is crucial for achieving substantial reductions.
Also Read:
- Optimizing AI Reasoning for Shorter, Smarter Responses
- Peer Review for Large Language Models: A Game Theory Approach
Significant Simplification Results
Experiments demonstrate that ProofOptimizer substantially compresses proofs generated by advanced AI provers on standard benchmarks. For instance, it reduced proof length by an impressive 87% on miniF2F, 57% on PutnamBench, and 49% on Seed-Prover’s IMO 2025 proofs. Beyond just conciseness, these simplified proofs offer several additional benefits. They check faster in Lean, improving computational efficiency. Furthermore, when these shorter, clearer proofs are reused as training data for supervised fine-tuning, they lead to improved performance in downstream proof generation tasks.
The research also highlights that ProofOptimizer significantly outperforms other powerful language models like Gemini-2.5-Pro in proof simplification, showcasing the effectiveness of its specialized training approach. While the model primarily optimizes for proof length, the researchers also explored optimizing for ‘heartbeats’ (a proxy for execution time), finding that this can lead to even faster proofs, albeit sometimes slightly longer in token count.
ProofOptimizer marks a pivotal development in the field of automated theorem proving. By making AI-generated proofs not only correct but also concise and human-readable, it bridges the gap between rigorous formal verification and intuitive mathematical understanding. For more details, you can refer to the full research paper: ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations.
