# ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization

arXiv: https://arxiv.org/abs/2605.22885 · HTML: https://mlsanity.com/paper/2605.22885/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 12 of its 35 references that are in the map.
- First posted on arXiv 21 May 2026.

## Builds on (most cited first, 12 of 12)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [A Survey of Deep Learning for Mathematical Reasoning](https://mlsanity.com/paper/2212.10535/) (2022)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learning](https://mlsanity.com/paper/2412.15184/) (2024)
- [ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations](https://mlsanity.com/paper/2510.15700/) (2025)
- [HepLean: Digitalising high energy physics](https://mlsanity.com/paper/2405.08863/) (2024)
- [ImProver: Agent-Based Automated Proof Optimization](https://mlsanity.com/paper/2410.04753/) (2024)
- [Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure](https://mlsanity.com/paper/2509.09726/) (2025)

## Abstract (arXiv)

Formal mathematics libraries are rapidly expanding, creating a growing need to refactor verified proofs for maintainability and to improve training data quality for neural provers. However, scalable proof optimization is hindered by heterogeneous and heuristically specified objectives, scarce data, and high training and inference costs. To overcome these challenges, we introduce ImProver 2, a neurosymbolic framework for automated proof optimization in Lean 4. ImProver 2 combines a data-efficient expert-iteration pipeline with a scaffold that exposes formal structure alongside lightweight informal abstractions. We further introduce a suite of metrics capturing structural proof properties. Using ImProver 2, we train a 7B-parameter model that outperforms orders-of-magnitude larger models within the same model family, and is competitive with mid-tier frontier models across metrics. We additionally demonstrate that our neurosymbolic scaffold significantly improves performance across both small and frontier models. We show that with proper scaffolding and training, small models can effectively restructure research-level proofs over complex and varied metrics, matching substantially larger systems and establishing proof optimization as a scalable, learnable task.