Pith. sign in

REVIEW 4 major objections 5 minor 3 cited by

IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation

T0 review · 4 major / 5 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A new benchmark measures AI's ability to write research-level mathematical proofs, finding that the strongest current model produces a complete, expert-accepted solution for 22% of tasks, while no model solves any of the open problems.

desk verdict A genuinely new community-built benchmark for research-level proof generation; the headline 22% figure is plausible but rests on single-author grading with no reliability data, so treat the exact rates as provisional. read the letter →

arxiv 2509.26076 v2 pith:6YFZ65ZA submitted 2025-09-30 cs.CL

Johannes Schmitt , Gergely Bérczi , Jasper Dekoninck , Jeremy Feusi , Tim Gehrunger , Raphael Appenzeller , Pieter Belmans , Alessio Bottini
show 52 more authors
Jim Bryan João Camarneiro Ana Cannas da Silva Niklas Canova Ana-Maria Castravet Timo de Wolff Claudio Fontanari Filippo Gaia Baran Hashemi Daniel Holmes David Holmes Aitor Iribar Lopez Victor Jaeck Martina J{o}rgensen Steven Kelk Martijn Kool Stefan Kuhlmann Adam Kurpisz Johannes Lengler Chiara Meroni Ingmar Metzler Martin Möller Samuel Muñoz-Echániz David Muñoz-Lahoz Robert Nowak Georg Oberdieck Daniel Platt Dylan Possamaï Gabriel Ribeiro Aluna Rizzoli Daria Sakhanda Raúl Sánchez Galán Zheming Sun Diaaeldin Taha Josef Teichmann Richard P. Thomas Henk van der Pol Michel van Garrel Charles Vial Ignacio Barros Benjamin Doerr Peter Grünwald Henry Liu David Martins Aleksandar Mijatović Sergej Monavari Marc Roth Patrick Schnider Yannik Schuler Pim Spelier Yuuji Tanaka Ronald van Luijk
This is my paper · ORCID
classification cs.CL
keywords benchmarklargelanguagemodelsmathematicalproofgenerationresearch-levelmathematicsagenticevaluationhumangradingverificationAI
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper introduces IMProofBench, a private benchmark of research-level mathematics problems where the expected answer is a written proof rather than a single number. The central claim is that current large language models can already solve a meaningful fraction of these problems when given tools: the best model, GPT-5, produces a fully correct proof for 22% of tasks, and the strongest final-answer model, GROK-4, answers 52% of the short-answer subproblems correctly. The authors argue that this shows proof-generation ability at the research frontier is non-trivial but far from solving open problems, and that benchmarks must measure proof quality, not just final answers, to track real progress.

What carries the argument

The central machinery is IMProofBench itself: a private, dynamically growing set of 39 research-level problems, each authored and peer-reviewed by a professional mathematician, with a proof-based main question plus auto-gradable subquestions. Evaluation runs in an agentic framework giving models access to web search, numerical and symbolic computation, and shell tools; human authors grade complete solutions on a 0-3 scale, while subquestions are checked automatically. This structure separates final-answer performance from proof-generation quality and provides a realistic research-like setting.

What would settle it

Take a random sample of solutions that received a full (3/3) grade and have them independently re-graded by two or more mathematicians blinded to the original grade and to each other; if the full-solution rate drops well below 22% or the inter-rater agreement is poor, the central claim is not supported. Similarly, if formal proof verification tools reject a substantial fraction of the 'full' solutions, the claim weakens.

Watch

Extended reading notes

Core claim

The paper claims that state-of-the-art LLMs, operating in an agentic environment with web search and mathematical software, can write complete, expert-accepted proofs for roughly one in five research-level problems, while solving about half of the short-answer subproblems. None of the seven open research problems in the set were solved. The benchmark's design—peer-reviewed problems authored by research mathematicians, with human grading of proofs and automated grading of subquestions—enables this assessment and reveals a consistent gap between final-answer accuracy and genuine proof-writing ability.

Load-bearing premise

The paper assumes that a single expert author's 0-3 grade, given while knowing the intended solution, reliably and consistently measures whether a proof is complete and correct.

Editorial extensions

If this is right

  • Proof-writing ability at research level can be measured with human expert grading, and current top models pass on roughly one in five problems.
  • Final-answer accuracy overestimates proof ability: the best final-answer model scores 52% on subquestions but only 19% on full proofs, so final-answer-only benchmarks mislead.
  • Models rarely abstain and often present confident but incorrect proofs, meaning practitioners cannot trust unsolicited AI proofs without careful review.
  • The benchmark's dynamic, rolling design is intended to prevent saturation and contamination as models improve.
  • No model solved any of the open research problems, indicating that frontier proof-generation is still far from pushing research forward independently.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the 22% full-solution rate generalizes beyond this small, self-selected problem set, AI systems could plausibly serve as research assistants that propose proof sketches for expert vetting, but not as autonomous provers; a testable extension would be a study where experts attempt to verify a random sample of graded 'full' solutions without knowing the model, and measure agreement.
  • The absence of inter-rater reliability means the precise numbers (22%, 52%) are likely to shift under independent grading, so the paper's contribution is better read as 'non-trivial proof ability exists' than as a precise ranking.
  • The benchmark's dependence on volunteer expert authors and its small size (39 problems) may bias difficulty; a replication with problems from a broader community or stratified sampling would test robustness.
  • One could connect this to formal proof verification: submitting a graded 'full' solution to a proof assistant would provide a stronger, less subjective check of the claim.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper introduces IMProofBench, a private benchmark of research-level proof-generation problems authored and peer-reviewed by professional mathematicians, with each problem paired with automatically gradable subquestions. Ten LLMs are evaluated in an agentic, tool-augmented environment (Python, SageMath, bash, web search), and the main proof attempts are graded by the problem's author on a 0–3 scale. The headline results are that GPT-5 solves 22% of problems completely, GROK-4 achieves 52% accuracy on final-answer subquestions, and none of the 7 open problems were solved. The paper also provides a qualitative analysis of error modes, tool use, and model behavior.

Significance. If the quantitative results are reliable, the benchmark fills a genuine gap: it targets research-level proof-writing rather than final answers, uses an agentic setup that mimics real mathematical work, and is built through a community pipeline with expert review. The distinction between proof-grade and final-answer performance is valuable, and the qualitative observations (e.g., models rarely abstain, hallucinate existing results, and sometimes produce useful partial insights) are informative. However, the central quantitative claims rest on a single expert grader per problem with no inter-rater reliability measurement, and the reporting contains denominator inconsistencies. The paper's current value is therefore more indicative than definitive; the benchmark infrastructure and methodology are promising, but the headline numbers need stronger validation.

major comments (4)
  1. [§3.3, §B.4, Fig. 5] The central claim that GPT-5 produces 'complete solutions' for 22% of tasks rests entirely on the author-assigned 0–3 progress score. The grading process is described as single-grader, with no inter-rater reliability, no independent verification that a 3/3 grade corresponds to a mathematically correct proof, and the grader is the problem author who knows the intended solution. On a denominator of 39 problems, 22% is 8–9 problems, so a single grade change shifts the headline by several points. The paper explicitly defers inter-rater reliability to future work (App. F). I ask the authors to provide at least a small inter-rater study (e.g., a second independent grader on a random subset, with agreement statistics such as Cohen's kappa or weighted kappa) and to report confidence intervals around the key percentages. Without this, the 22% figure is not yet established.
  2. [Abstract vs. §3.4, §4.1, Fig. 4] There are inconsistent denominators across the paper. The abstract as submitted states the benchmark contains '77 peer-reviewed problems' while the body (§3.4, §5) consistently says 39 problems. Fig. 4 reports results 'on the 31 questions that include follow-up subquestions and human grading,' while Fig. 5 is labeled 'Results on IMProofBench' without specifying the denominator. The relationship among 39, 31, and 77, and the exact denominators behind the 22% and 52% figures, must be clarified. These inconsistencies directly affect the interpretation of every quantitative claim.
  3. [Reproducibility Statement] The paper's quantitative results cannot currently be independently checked: the dataset is private, and the code base and evaluation framework are only promised for future release (before November 30, 2025). For a benchmark paper, the evaluation code, grading scripts, and analysis pipeline are central artifacts. I request that the code and at least the sample problems be made available at submission time, or that the paper clearly state an embargo with a DOI or repository link. Without this, the 22% and 52% numbers are not verifiable by reviewers or the community.
  4. [§4.1, Fig. 4] The correlation coefficient of 0.45 between author-weighted subquestion scores and human progress scores is reported without a confidence interval or significance test, on a sample of 31 questions. Given that the subquestions are written by the same author who assigns the progress grade, the observed correlation may partly reflect shared problem-specific difficulty rather than a general relationship between final-answer performance and proof quality. Please provide error bars and discuss this interpretation.
minor comments (5)
  1. [Throughout] Model names are inconsistent (e.g., 'Grok 4' vs 'GROK-4' in figure captions and text). Please standardize.
  2. [App. C] The sample problem is useful, but the figure (Fig. 1) and surrounding text should clarify that GPT-5's 'Full Grade: 3/3' is an example, not necessarily representative; otherwise readers may overgeneralize from one showcased success.
  3. [§4.2] The 'Not Sure' category in error and achievement indicators is reported in aggregate but not defined with respect to the binary True/False options. Please state how 'Not Sure' responses were treated in the percentages (e.g., excluded, counted as False).
  4. [App. E] The tool descriptions are detailed and helpful, but the statement that 'each execution is independent—no state is preserved' is contradicted later by 'files written to disk remain accessible.' Please reconcile the wording.
  5. [References] The reference to the Inspect framework lists 'AI Security Institute' while the bibliography entry says 'UK AI Security Institute.' Please align the citation with the official institution name.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the benchmark measures models against external expert-authored problems; grading reliability is a validity risk, not a reasoning loop.

full rationale

IMProofBench is an evaluation study, not a derivation. The central quantitative claims (GPT-5 22% complete solutions; GROK-4 52% final-answer accuracy) are direct measurements: the 0–3 progress score is assigned by the problem author (§3.3) and follow-up answers are checked against ground truth. There is no equation in the paper that is fitted to these measurements and then re-predicted, no parameter identified with a target quantity, and no uniqueness theorem or ansatz inherited from the authors' prior work. The only self-citation in a mathematical context is Schmitt and van Zelm (2020), used in Appendix C as background for the definition of stable graphs; it is not load-bearing for any result. The paper's own App. F defers inter-rater reliability to future work, and the grading protocol's reliance on a single author-grader is a legitimate threat to the reliability of the 22% figure, but that is an empirical validity concern, not a circularity of the kind where a claim reduces by construction to its own input. No circular step can be quoted and exhibited, so the score is 0.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

Benchmark papers do not have derived equations, so the ledger records the evaluative assumptions that the headline numbers rest on.

assumptions (5)
  • domain assumption The 39 expert-reviewed problems are representative of research-level mathematics.
    Small scale (39 problems), skewed topic distribution (algebraic geometry-heavy; Fig. 13), and selection via organizers' networks mean general claims about 'research-level mathematics' rely on representativeness.
  • domain assumption Author-graders' 0–3 scores are reliable ground truth.
    Grading by question authors, blinded to model identity, with no inter-rater reliability (§3.3, App. B.4, App. F).
  • domain assumption Private problems are not in model training data (contamination-free).
    Privacy is the contamination defence; no systematic contamination check is described, and authors could preview questions on GPT-5 during creation (§3.2).
  • domain assumption The agentic environment approximates a research environment.
    The Inspect-based setup with tools mirrors researcher workflows; claims about 'real research conditions' depend on this approximation (§3.3, App. E).
  • domain assumption Automated subquestion parsing is accurate.
    Automated comparisons are manually verified by an administrator; parsing errors are corrected, but this manual step is not quantified.

how reviews work

0 comments
Cite this review

Pith. "Pith review of IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation." pith.science (2026). https://pith.science/paper/6YFZ65ZA

@misc{pith2026250926076,
  author       = {Pith},
  title        = {Pith review of: IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/6YFZ65ZA}},
  note         = {Machine review of arXiv:2509.26076}
}
read the original abstract

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.

Figures

Figures reproduced from arXiv: 2509.26076 by the authors.

Figure 1
Figure 1. Example IMProofBench problem. Models are tested on research-level questions in an [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Workflow for question creation with peer review. Authors iteratively refine questions based [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Evaluation workflow in a multi-turn environment with research tools. The main solution is [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (15 more)
Figure 4
Figure 4. Figure 4: Results on the 31 questions that include follow-up subquestions and human grading. GPT-5 Grok 4 Gemini 2.5 Pro o4-mini Claude Opus 4.1 0% 20% 40% 60% 80% 100% 22% 53% 17% 19% 14% 25% 42% 69% 17% 14% 50% 31% 53% 42% Complete Solution Major Progress Minor Progress No Pro…
Figure 5
Figure 5. Figure 5: Results on IMProofBench. Final-answer evaluation In [PITH_FULL_IMAGE:figures/full_fig_p007_5.png]
Figure 6
Figure 6. Figure 6: Error indicators GPT-5 Grok 4 o4-mini Gemini 2.5 Pro Claude Opus 4.1 0% 20% 40% 60% 80% 100% Understanding Correct Result Not Sure Insight Usefulness [PITH_FULL_IMAGE:figures/full_fig_p008_6.png]
Figure 8
Figure 8. Figure 8: Average tool usage per question. GPT-5 Grok 4 o4-mini Gemini 2.5 Pro Claude Opus 4.1 500 1k 5k 10k 50k 100k Reasoning Tokens Output Tokens [PITH_FULL_IMAGE:figures/full_fig_p008_8.png]
Figure 10
Figure 10. Figure 10: Average percentage of points for subquestion evaluation. Here, performance on any [PITH_FULL_IMAGE:figures/full_fig_p015_10.png]
Figure 11
Figure 11. Figure 11: Token usage distribution for problem evaluation (main question and subquestions) for all [PITH_FULL_IMAGE:figures/full_fig_p015_11.png]
Figure 12
Figure 12. Figure 12: Average tool usage for all tested models. [PITH_FULL_IMAGE:figures/full_fig_p016_12.png]
Figure 13
Figure 13. Figure 13: Word cloud of tags assigned to IMProofBench problems. [PITH_FULL_IMAGE:figures/full_fig_p016_13.png]
Figure 14
Figure 14. Figure 14: Landing and overview page of IMProofBench website. [PITH_FULL_IMAGE:figures/full_fig_p030_14.png]
Figure 15
Figure 15. Figure 15: Guidelines for authoring benchmark problems. [PITH_FULL_IMAGE:figures/full_fig_p031_15.png]
Figure 16
Figure 16. Figure 16: Window for editing questions, solutions, and their associated subquestions; via the blue [PITH_FULL_IMAGE:figures/full_fig_p032_16.png]
Figure 17
Figure 17. Figure 17: Overview page of question data (with main question, sample solution, AI answer preview, [PITH_FULL_IMAGE:figures/full_fig_p033_17.png]
Figure 18
Figure 18. Figure 18: Question review window showing text box for feedback and review instruction summary. [PITH_FULL_IMAGE:figures/full_fig_p034_18.png]
Figure 19
Figure 19. Figure 19: Detailed explainer of review instructions and process. [PITH_FULL_IMAGE:figures/full_fig_p035_19.png]
Figure 20
Figure 20. Figure 20: Grading form, displaying sample solution, model answer, and scoring form side by side. [PITH_FULL_IMAGE:figures/full_fig_p036_20.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Mathematical Discovery in the Wild: AI-Guided Proofs in Banach Space Theory

    math.FA 2026-07 conditional novelty 8.0 of 10

    AI-generated, human-verified proofs of five open Banach-space problems, including primariness of Lp(L1) and a unital Banach algebra that is not any Calkin algebra.

  2. Evaluating SageMath-Augmented LLM Agents for Computational and Experimental Mathematics

    cs.AI 2026-07 accept novelty 6.5 of 10

    SageMath-augmented ReAct agents raise solve rates by +9.7 pp on average on a curated 133-problem RealMath subset, with GPT-5.5 reaching 75.2%.

  3. QEDBENCH: Quantifying the Alignment Gap in Automated Evaluation of University-Level Mathematical Proofs

    cs.LG 2026-02 conditional novelty 6.0 of 10

    On QEDBench, frontier LLM judges over-score university math proofs by up to +0.36 on average relative to human experts, while some solver models fail badly on discrete-combinatorial problems.

Reference graph

Works this paper leans on

12 extracted references · 1 linked inside Pith · cited by 3 Pith papers

  1. [3]

    auto" max tokens=32000 reasoningtokens=31000 GPT-5gpt-5 reasoning effort=

    ”. After a few attempts, it calculates this polynomial via Lagrange interpolation on datapoints with fixed residue modulo 6, discovering that the case g= 2 needs separate treatment. This not only represents a perfect solution to the given problem, but also mirrors precisely the approach of the human question author to solving the problem. • GROK-4 obtains...

    2025

  2. [6]

    True”, “False

    Correct Result:Arrives at the correct final answer (with N/A option for open-ended problems or when the correct answer is unknown) 7.Insight:Shows creative problem-solving or novel approaches 8.Usefulness:Solution would be helpful to someone learning this topic Each binary category offers three response options: “True”, “False”, or “Not Sure”, allowing gr...

    2020

  3. [8]

    Underlying system is ArchLinux with many standard open-source computer algebra systems (like GAP) pre-installed

    This tool has a timeout of 15 minutes and maximal memory usage (RAM) of 8 GB Bash tool description Use this function to execute bash commands. Underlying system is ArchLinux with many standard open-source computer algebra systems (like GAP) pre-installed. This tool has a timeout of 15 minutes and maximal memory usage (RAM) of 8 GB. Web search tool descrip...

  4. [12]

    Each execution is independent - no state is preserved between runs

  5. [13]

    You must explicitly use print() statements to see any output

  6. [14]

    Simply writing expressions (like in notebooks) will not display results

  7. [15]

    The script cannot accept interactive input during execution

  8. [16]

    Return statements alone won’t produce visible output

Show all 12 references
  1. [17]

    All variables and imports are cleared between executions

  2. [18]

    Standard output (via print()) is the only way to see results

  3. [19]

    Automorphismsˆ2: {G.automorphism_number()ˆ2}

    This tool has a timeout of 15 minutes and maximal memory usage (RAM) of 8 GB All standard SageMath functions are pre-imported and available. The SageMath preparser is applied, so you can use natural mathematical syntax. Key Features: - Natural syntax: Use xˆ2 for powers, K.<a>...

  4. [2025]

    Is the statement true forn= 5 ?

    Accessed: 2025-09-15. Epoch AI. Clarifying the creation and use of the frontiermath benchmark. https://epoch.ai/ blog/openai-and-frontiermath, January 2025. Accessed: 2025-09-25. UK AI Security Institute. Inspect AI: Framework for Large Language Model Evaluations, 2024. URL ht...

    2025 doi arXiv

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.