# IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation

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

## Key facts

- Cited by 13 papers in the map (data through 14 Oct 2026).
- Builds on 22 of its 47 references that are in the map.
- First posted on arXiv 30 Sep 2025.

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

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [MathArena: Evaluating LLMs on Uncontaminated Math Competitions](https://mlsanity.com/paper/2505.23281/) (2025)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models](https://mlsanity.com/paper/2410.07985/) (2024)
- [Mathematical Capabilities of ChatGPT](https://mlsanity.com/paper/2301.13867/) (2023)
- [FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI](https://mlsanity.com/paper/2411.04872/) (2024)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad](https://mlsanity.com/paper/2503.21934/) (2025)
- [The SCIP Optimization Suite 9.0](https://mlsanity.com/paper/2402.17702/) (2024)
- [RealMath: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematics](https://mlsanity.com/paper/2505.12575/) (2025)
- [The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs](https://mlsanity.com/paper/2506.21621/) (2025)
- [Brains vs. Bytes: Evaluating LLM Proficiency in Olympiad Mathematics](https://mlsanity.com/paper/2504.01995/) (2025)
- [Solving Inequality Proofs with Large Language Models](https://mlsanity.com/paper/2506.07927/) (2025)
- [UGMathBench: A Diverse and Dynamic Benchmark for Undergraduate-Level Mathematical Reasoning with Large Language Models](https://mlsanity.com/paper/2501.13766/) (2025)
- [Right Is Not Enough: The Pitfalls of Outcome Supervision in Training LLMs for Math Reasoning](https://mlsanity.com/paper/2506.06877/) (2025)
- [UQ: Assessing Language Models on Unsolved Questions](https://mlsanity.com/paper/2508.17580/) (2025)
- [Learning Program Synthesis for Integer Sequences from Scratch](https://mlsanity.com/paper/2202.11908/) (2022)
- [FACT: Learning Governing Abstractions Behind Integer Sequences](https://mlsanity.com/paper/2209.09543/) (2022)

## Built on by (most cited first, 13 of 13)

- [Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs](https://mlsanity.com/paper/2605.00674/) (2026)
- [First Proof](https://mlsanity.com/paper/2602.05192/) (2026)
- [Measuring Progress in Reasoning Toward Mathematical Discovery with Automatic Verification](https://mlsanity.com/paper/2603.15617/) (2026)
- [Soohak: A Mathematician-Curated Benchmark for Evaluating Research-level Math Capabilities of LLMs](https://mlsanity.com/paper/2605.09063/) (2026)
- [Flow-based Extremal Mathematical Structure Discovery](https://mlsanity.com/paper/2601.18005/) (2026)
- [Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness](https://mlsanity.com/paper/2605.10379/) (2026)
- [Judging What We Cannot Solve: A Consequence-Based Approach for Oracle-Free Evaluation of Research-Level Math](https://mlsanity.com/paper/2602.06291/) (2026)
- [The ORCA Benchmark: Evaluating Real-World Calculation Accuracy in Large Language Models](https://mlsanity.com/paper/2511.02589/) (2025)
- [Benchmarks in Leipzig](https://mlsanity.com/paper/2606.05818/) (2026)
- [Failure Modes of Large Language Models on Research-Level Mathematics: A Taxonomy and an Empirical Characterisation](https://mlsanity.com/paper/2606.24902/) (2026)
- [Evaluating SageMath-Augmented LLM Agents for Computational and Experimental Mathematics](https://mlsanity.com/paper/2607.06820/) (2026)
- [Mathematical Discovery in the Wild: AI-Guided Proofs in Banach Space Theory](https://mlsanity.com/paper/2607.17388/) (2026)
- [TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science](https://mlsanity.com/paper/2609.35606/) (2026)

## Abstract (arXiv)

As the mathematical capabilities of large language models (LLMs) improve, it becomes increasingly important to evaluate their performance on research-level tasks at the frontier of mathematical knowledge. However, existing benchmarks are limited, as they focus solely on final-answer questions or high-school competition problems. To address this gap, we introduce IMProofBench, a private benchmark consisting of 77 peer-reviewed problems developed by expert mathematicians. Each problem requires a detailed proof and is paired with subproblems that have final answers, supporting both an evaluation by human experts and a large-scale quantitative analysis through automated grading. Furthermore, unlike prior benchmarks, the evaluation setup simulates a realistic research environment: models operate in an agentic framework with tools like web search for literature review and mathematical software such as SageMath. Our results show that current LLMs can already solve a significant percentage of research-level questions. IMProofBench will continue to evolve as a dynamic benchmark in collaboration with the mathematical community, ensuring its relevance for evaluating the next generation of LLMs.