IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation
Not on the map. Why?
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.
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
22 of 47 references.
References · 22
- 2021Training Verifiers to Solve Math Word Problemscited by 10,109
- 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 9,379
- 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,371
- 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
- 2025MathArena: Evaluating LLMs on Uncontaminated Math Competitionscited by 297
- 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 287
- 2024Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Modelscited by 284
- 2023Mathematical Capabilities of ChatGPTcited by 268
- 2024FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AIcited by 243
- 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 165
- 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 154
- 2025Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiadcited by 74
10 more
- 2024The SCIP Optimization Suite 9.0cited by 37
- 2025RealMath: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematicscited by 31
- 2025The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofscited by 30
- 2025Brains vs. Bytes: Evaluating LLM Proficiency in Olympiad Mathematicscited by 24
- 2025Solving Inequality Proofs with Large Language Modelscited by 21
- 2025UGMathBench: A Diverse and Dynamic Benchmark for Undergraduate-Level Mathematical Reasoning with Large Language Modelscited by 13
- 2025Right Is Not Enough: The Pitfalls of Outcome Supervision in Training LLMs for Math Reasoningcited by 10
- 2025UQ: Assessing Language Models on Unsolved Questionscited by 9
- 2022Learning Program Synthesis for Integer Sequences from Scratchcited by 8
- 2022FACT: Learning Governing Abstractions Behind Integer Sequencescited by 6
Built on by
Citing papers per year: 2025: 1; 2026: 12.
13 papers.
Sort:
By area:
- 2026Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMscited by 137
- 2026First Proofcited by 32
- 2026Measuring Progress in Reasoning Toward Mathematical Discovery with Automatic Verificationcited by 9
- 2026Soohak: A Mathematician-Curated Benchmark for Evaluating Research-level Math Capabilities of LLMscited by 4
- 2026Flow-based Extremal Mathematical Structure Discoverycited by 3
- 2026Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctnesscited by 3
- 2026Judging What We Cannot Solve: A Consequence-Based Approach for Oracle-Free Evaluation of Research-Level Mathcited by 1
- 2025The ORCA Benchmark: Evaluating Real-World Calculation Accuracy in Large Language Modelscited by 0
- 2026Benchmarks in Leipzigcited by 0
- 2026Failure Modes of Large Language Models on Research-Level Mathematics: A Taxonomy and an Empirical Characterisationcited by 0
- 2026Evaluating SageMath-Augmented LLM Agents for Computational and Experimental Mathematicscited by 0
- 2026Mathematical Discovery in the Wild: AI-Guided Proofs in Banach Space Theorycited by 0
- 2026TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science28 Sep 2026
- 2026Mathematical Discovery in the Wild: AI-Guided Proofs in Banach Space Theory19 Jul 2026
- 2026Evaluating SageMath-Augmented LLM Agents for Computational and Experimental Mathematics7 Jul 2026
- 2026Failure Modes of Large Language Models on Research-Level Mathematics: A Taxonomy and an Empirical Characterisation12 Jun 2026
- 2026Benchmarks in Leipzig4 Jun 2026
- 2026Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness11 May 2026
- 2026Soohak: A Mathematician-Curated Benchmark for Evaluating Research-level Math Capabilities of LLMs9 May 2026
- 2026Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs1 May 2026
- 2026Measuring Progress in Reasoning Toward Mathematical Discovery with Automatic Verification16 Mar 2026
- 2026Judging What We Cannot Solve: A Consequence-Based Approach for Oracle-Free Evaluation of Research-Level Math6 Feb 2026
- 2026First Proof5 Feb 2026
- 2026Flow-based Extremal Mathematical Structure Discovery25 Jan 2026
- 2026Measuring Progress in Reasoning Toward Mathematical Discovery with Automatic Verificationcited by 9
- 2026Soohak: A Mathematician-Curated Benchmark for Evaluating Research-level Math Capabilities of LLMscited by 4
- 2026Judging What We Cannot Solve: A Consequence-Based Approach for Oracle-Free Evaluation of Research-Level Mathcited by 1
- 2025The ORCA Benchmark: Evaluating Real-World Calculation Accuracy in Large Language Modelscited by 0
- 2026Soohak: A Mathematician-Curated Benchmark for Evaluating Research-level Math Capabilities of LLMs9 May 2026
- 2026Measuring Progress in Reasoning Toward Mathematical Discovery with Automatic Verification16 Mar 2026
- 2026Judging What We Cannot Solve: A Consequence-Based Approach for Oracle-Free Evaluation of Research-Level Math6 Feb 2026
- 2025The ORCA Benchmark: Evaluating Real-World Calculation Accuracy in Large Language Models4 Nov 2025
- 2026Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMscited by 137
- 2026First Proofcited by 32
- 2026Flow-based Extremal Mathematical Structure Discoverycited by 3
- 2026Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctnesscited by 3
- 2026Benchmarks in Leipzigcited by 0
- 2026Failure Modes of Large Language Models on Research-Level Mathematics: A Taxonomy and an Empirical Characterisationcited by 0
- 2026Mathematical Discovery in the Wild: AI-Guided Proofs in Banach Space Theorycited by 0
- 2026TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Sciencecited by 0
- 2026TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science28 Sep 2026
- 2026Mathematical Discovery in the Wild: AI-Guided Proofs in Banach Space Theory19 Jul 2026
- 2026Failure Modes of Large Language Models on Research-Level Mathematics: A Taxonomy and an Empirical Characterisation12 Jun 2026
- 2026Benchmarks in Leipzig4 Jun 2026
- 2026Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness11 May 2026
- 2026Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs1 May 2026
- 2026First Proof5 Feb 2026
- 2026Flow-based Extremal Mathematical Structure Discovery25 Jan 2026
Similar, not cited
Close in wording, no citation either way
- 2026AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification
- 2026LiveMathematicianBench: A Live Benchmark for Research-Level Mathematical Reasoning with Proof Sketches
- 2026Riemann-Bench: A Benchmark for Moonshot Mathematics
- 2025FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models
- 2026EternalMath: A Living Benchmark of Frontier Mathematics that Evolves with Human Discovery
- 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
- 2026CrowdMath: A Dataset of Crowdsourced Mathematical Research Discussions
- 2025Evaluating Frontier LLMs on PhD-Level Mathematical Reasoning: A Benchmark on a Textbook in Theoretical Computer Science about Randomized Algorithms