mlsanityData to 14 Oct 2026

IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation

arXiv 2509.26076 ↗First posted 30 Sep 2025cs.CLcited by 13

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

  1. 2021Training Verifiers to Solve Math Word Problemscited by 10,109
  2. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 9,379
  3. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,371
  4. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  5. 2025MathArena: Evaluating LLMs on Uncontaminated Math Competitionscited by 297
  6. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 287
  7. 2024Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Modelscited by 284
  8. 2023Mathematical Capabilities of ChatGPTcited by 268
  9. 2024FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AIcited by 243
  10. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 165
  11. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 154
  12. 2025Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiadcited by 74
10 more
  1. 2024The SCIP Optimization Suite 9.0cited by 37
  2. 2025RealMath: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematicscited by 31
  3. 2025The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofscited by 30
  4. 2025Brains vs. Bytes: Evaluating LLM Proficiency in Olympiad Mathematicscited by 24
  5. 2025Solving Inequality Proofs with Large Language Modelscited by 21
  6. 2025UGMathBench: A Diverse and Dynamic Benchmark for Undergraduate-Level Mathematical Reasoning with Large Language Modelscited by 13
  7. 2025Right Is Not Enough: The Pitfalls of Outcome Supervision in Training LLMs for Math Reasoningcited by 10
  8. 2025UQ: Assessing Language Models on Unsolved Questionscited by 9
  9. 2022Learning Program Synthesis for Integer Sequences from Scratchcited by 8
  10. 2022FACT: Learning Governing Abstractions Behind Integer Sequencescited by 6

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2025: 1; 2026: 12.

13 papers.

Sort:

By area:

Similar, not cited

Close in wording, no citation either way

  1. 2026AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification
  2. 2026LiveMathematicianBench: A Live Benchmark for Research-Level Mathematical Reasoning with Proof Sketches
  3. 2026Riemann-Bench: A Benchmark for Moonshot Mathematics
  4. 2025FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models
  5. 2026EternalMath: A Living Benchmark of Frontier Mathematics that Evolves with Human Discovery
  6. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
  7. 2026CrowdMath: A Dataset of Crowdsourced Mathematical Research Discussions
  8. 2025Evaluating Frontier LLMs on PhD-Level Mathematical Reasoning: A Benchmark on a Textbook in Theoretical Computer Science about Randomized Algorithms