{"id":"01c870f6-0c60-4178-bba6-b88a16a661a1","arxiv_id":"2509.26076","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"In an agentic, tool-equipped evaluation of 39 expert-written problems, GPT-5 produced fully correct proofs on 22% and GROK-4 answered 52% of final-answer subquestions.","lead":"IMProofBench is a private, expert-authored benchmark for research-level math proof generation; running 10 LLMs in an agentic environment with web search and computer algebra, the authors find GPT-5 fully solves 22% of proof tasks and GROK-4 answers 52% of final-answer subquestions. It matters because most math benchmarks only check final answers, so this is an early attempt to grade whether AI can actually write research-grade proofs.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The 22% full-solution rate rests on a single author-grader's 0–3 score per problem, with no inter-rater reliability or independent verification, so the headline number is not yet established.","rationale":"The reader identified exactly the same load-bearing assumption, and I agree: grading reliability is the hinge. Other issues—the problem-count inconsistency, no public code or questions, topic skew toward algebraic geometry—are real but do not directly determine whether 22% is meaningful; they affect reproducibility and generality. A benchmark whose main metric is a human judgment on a 0–3 scale must demonstrate that the judgment is not idiosyncratic. Because the grader is the problem author, the standard is the author's own solution, and no independent check exists. App. F's planned inter-rater reliability study confirms this gap. The concrete test above would settle it. If reliability is high, the conditional verdict can be upgraded; if not, the headline rates need confidence intervals or recalibration. I therefore leave the reader's CONDITIONAL verdict unchanged.","tokens_in":22540,"tokens_out":5346,"duration_ms":45949,"concrete_test":"Select a random stratified sample of ~20 problems × the five Tier-1 models (≈100 solutions). Have two independent expert mathematicians (not the problem authors) grade each solution with the same rubric, blinded to author grades and model identity; also have the original authors re-grade a blinded subset. Report exact agreement and Cohen's kappa on the binary full/non-full decision and on the 4-point scale, and recompute GPT-5/GROK-4 full-solution rates using the independent grades. If kappa < 0.6 or the independent GPT-5 full-solution rate falls outside roughly 10–35%, the paper's headline rate is not supported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central quantitative claim—GPT-5 produces complete solutions for 22% of research-level proof problems—depends entirely on the 0–3 progress score assigned by the problem's author in §3.3/App. B.4. A 3/3 ('full') grade is the only basis for 'complete solution'; there is no formal verification, no second reader, and App. F explicitly defers 'inter-rater reliability' to future work. The grading interface blinds model identity, but the author knows the intended solution and has a personal stake in the problem, which can bias leniency or harshness in either direction. Compounding this, GROK-4's short answers caused graders to be unsure ('Not Sure') on many binary categories, and the 39-problem scale means 22% is roughly 8–9 problems with a wide binomial confidence interval. Without reliability data, the 22% figure could materially shift under independent evaluation. The internal 77-vs-39 problem-count inconsistency also reduces trust in the reporting but is secondary to the grading concern.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":22804,"tokens_out":3429,"duration_ms":32255,"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":[{"comment":"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.","section":"§3.3, §B.4, Fig. 5"},{"comment":"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.","section":"Abstract vs. §3.4, §4.1, Fig. 4"},{"comment":"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.","section":"Reproducibility Statement"},{"comment":"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.","section":"§4.1, Fig. 4"}],"minor_comments":[{"comment":"Model names are inconsistent (e.g., 'Grok 4' vs 'GROK-4' in figure captions and text). Please standardize.","section":"Throughout"},{"comment":"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.","section":"App. C"},{"comment":"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).","section":"§4.2"},{"comment":"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.","section":"App. E"},{"comment":"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.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The paper is a solid community effort and the benchmark concept addresses a real gap. The main unresolved issue is scientific: the headline numbers depend on single-author grading with no reliability evidence. This is fixable within the scope of a revision by adding an inter-rater reliability experiment (even on a subset), reporting confidence intervals, and cleaning up the denominator inconsistencies. I would not reject, but the current version is not yet acceptable as a definitive benchmark claim."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Rough take: this is worth taking seriously. The gap it targets is real: FrontierMath and HLE only measure final answers, and proof benchmarks stop at olympiad level. IMProofBench is the first effort I know that combines expert-authored private research problems, proof-based main questions, human grading, auto-graded subquestions, and an agentic tool environment (Python, SageMath, web). The qualitative findings are the most valuable part: models can engage with accessible research questions, fail on open problems, rarely abstain, and hallucinate about half the time. That matches what I'd expect, and it's grounded in logs and grader comments.\n\nThe soft spots are real but not fatal. The headline numbers—22% full solutions for GPT-5, 52% for Grok-4 on subquestions—come from 39 problems, so 22% is roughly 8-9 cases, with a wide binomial confidence interval. Grading is done by the problem author alone on a 0-3 scale; the paper reports no inter-rater reliability, and App. F defers it to future work. The blinding of model identities helps, but the grader knows the intended solution, and that can bias leniency in either direction. This doesn't sink the conclusion that current models solve a meaningful minority of these problems, but the exact rates should be treated as provisional. The 77-vs-39 problem-count discrepancy between the abstract and body is sloppy and needs fixing. The lack of released code and data also blocks independent verification, though the reproducibility statement promises code by November 30 and the appendices are unusually detailed. Topic coverage skews to algebraic geometry, which reflects the organizers' network; the paper acknowledges this.\n\nWhat the paper does well: the problem-creation pipeline with peer review is sound, the evaluation environment is well specified, and the limitations section is honest about scale. The correlation of 0.45 between human proof grades and subquestion scores is a useful sanity check, and it supports the claim that final-answer benchmarks miss nuance.\n\nBottom line: this deserves a serious referee, not a desk reject. I'd condition acceptance on fixing the abstract discrepancy, adding confidence intervals and at least a small inter-rater reliability study, and making the code and sample problems available. The paper is a solid foundation for a benchmark that should become more useful as it grows.","headline":"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.","tokens_in":23532,"tokens_out":2061,"would_cite":true,"duration_ms":17999,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["benchmark","large language models","mathematical proof generation","research-level mathematics","agentic evaluation","human grading","proof verification","AI evaluation"],"falsifier":"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.","tokens_in":22469,"feed_emoji":"📐","tokens_out":3491,"duration_ms":29160,"temperature":0.7,"pith_summary":"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.","feed_headline":"Top AI model produces full proofs on 22% of research tasks","feed_subtitle":"New benchmark grades proof writing, not just answers, and shows current LLMs make real but limited progress.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["AI writes full proofs on 22% of research problems","LLMs ace proof writing on 1 in 5 research tasks","New benchmark shows AI proof limits: 22% success","AI tackles research proofs, scores 22% complete","Research-proof benchmark: LLMs hit 22% full proofs"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["AI writes full proofs on 22% of research problems","LLMs ace proof writing on 1 in 5 research tasks","New benchmark shows AI proof limits: 22% success","AI tackles research proofs, scores 22% complete","Research-proof benchmark: LLMs hit 22% full proofs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000185,"raw_usage":{"total_tokens":1122,"prompt_tokens":670,"completion_tokens":452,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":414,"completion_tokens_details":{"reasoning_tokens":369}},"tokens_in":414,"tokens_out":452,"duration_ms":3932,"temperature":1.0,"reasoning_tokens":369,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T13:34:38.182464+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}