Pith. sign in

REVIEW 3 major objections 5 minor 43 references

Proof2Hybrid: Automatic Mathematical Benchmark Synthesis for Proof-Centric Problems

T0 review · 3 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read Proof2Hybrid automatically converts proofs into hard, verifiable proof-centric benchmark questions.

desk verdict Real engineering contribution with a genuinely better question format, but the ground-truth labels are set by the same LLMs it evaluates, so treat the 'profound deficits' claim with caution. read the letter →

arxiv 2508.02208 v2 pith:CTXNKC4R submitted 2025-08-04 cs.CL cs.AI

Yebo Peng , Zixiang Liu , Yaoming Li , Zhizhuo Yang , Xinye Xu , Bowen Ye , Weijun Yuan , Zihan Wang
show 1 more author
Tong Yang
This is my paper
classification cs.CLcs.AI
keywords benchmarksynthesisproof-centricmathematicslargelanguagemodelsmathevaluationhybridquestionformatdistractorgenerationLLM-as-judgealgebraicgeometry
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

Proof2Hybrid is presented as the first fully automated framework for building proof-centric mathematical benchmarks from natural-language mathematical texts. The paper's central claim is that definitions and proposition-proof pairs, taken from an open algebraic-geometry reference work, can be converted into large numbers of hard, automatically verifiable exam questions without expert item writers. The demonstration is AlgGeoTest, 456 items in which each question presents six statements and exactly two are true. A sympathetic reading of the paper is that this makes benchmark construction scalable to frontier mathematics and gives a more precise measure of how well LLMs actually reason in those domains.

What carries the argument

The central object is the m-out-of-n multiple judge question: one question built from n statements, exactly m of which are true, with every statement coming from a different mathematical proposition; the model must identify the m true statements. With m=2 and n=6, random guessing earns an expected accuracy of 1/15, and the distinct-origin rule blocks reasoning by comparing options derived from the same source. The machinery around it is Proof2X, a roadmap for rewriting proofs into automatically checkable question formats, plus a two-stage LLM filter: seed items are kept only if judges vote them correct at least 8 of 12 times, while distractors are kept only if judges vote them incorrect in 7 to 10 of 12 votes. Together these components convert raw proof text into a test that is hard to guess, hard to game by pattern comparison, and less sensitive to differing standards of what counts as a correct proof.

What would settle it

Take a random sample of AlgGeoTest distractors that passed the judge threshold and determine their truth with an independent proof checker or with expert mathematicians who did not see the label; if a non-negligible fraction turn out to be true statements or mathematically undetermined, the 7-of-12 incorrect-vote threshold is not tracking falsity. A cheaper version of the same test is to deliberately modify known-true theorems in the same style the generator uses and count how many are accepted by the judge panel.

Watch

Extended reading notes

Core claim

The paper claims that high-quality proof-centric evaluation is achievable by a purely LLM-orchestrated pipeline. Seed items, meaning definitions or proposition-proof pairs, are extracted from a curated corpus; a generation team of five LLMs perturbs each seed to produce flawed variants, and a separate judge panel of four leading LLMs votes on each candidate, keeping only distractors judged incorrect in 7 to 10 of 12 votes. These distractors are combined with true seeds into m-out-of-n multiple judge questions with m=2 true items out of n=6, all from distinct propositions. The resulting benchmark, AlgGeoTest, is put forward as evidence: expert audit is reported to find more than 98.75% of distractors mathematically incorrect yet plausible, and state-of-the-art models score at best around 61, with most scores below 20. The paper takes these results to show that the framework produces a challenging, domain-specific test that existing number-centric benchmarks do not supply.

Load-bearing premise

The load-bearing premise is that the judge models' majority verdicts separate truly false distractors from true statements; if those models share a blind spot, a distractor can be labeled false when it is actually true, and the benchmark silently inherits the error.

Editorial extensions

If this is right

  • If Proof2Hybrid works as claimed, proof-centric benchmarks can be produced at scale for any mathematical field that has definitions and proofs in natural language, not only algebraic geometry.
  • AlgGeoTest results would imply that top LLMs still have large, measurable gaps in algebraic-geometry reasoning, gaps that MATH-500 and AIME24 rankings do not reveal.
  • The 2-of-6 format would make low scores meaningful: with a random-guess baseline near 1/15, observed scores reflect actual discrimination rather than lucky guessing.
  • The weak correlations with MATH-500 and AIME24 (R-squared around 0.42 and 0.51) would support treating AlgGeoTest as measuring a distinct mathematical subfield or skill.
  • The perplexity-based evaluation protocol would extend the benchmark to base models and show that performance scales with model size within a family.

Reading between the lines

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

  • Editorial inference: the same pipeline should transfer to non-mathematical corpora in which definitions plus proof-like derivations appear, such as formal verification or theoretical computer science, so the method's value is not limited to algebraic geometry.
  • Editorial inference: the paper has not shown that judge consensus equals mathematical truth; a decisive follow-up would compare AlgGeoTest labels against an independent formal proof checker on a sample of items.
  • Editorial inference: benchmark difficulty is likely to drift as judge models improve; distractors tuned to be deceptively plausible to current models may become easy for future models, so the thresholds and distractor pool may need periodic regeneration.
  • Editorial inference: because the pipeline is parameterized by m, n, and judge thresholds, it could generate curricula of graduated difficulty by varying these parameters, a use the authors do not explore.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper introduces Proof2Hybrid, an automated pipeline that converts natural-language mathematical statements (definitions and proposition-proof pairs from The Stacks Project) into a hybrid "m-out-of-n multiple judge question" format in which each question contains a mix of true seed items and machine-generated distractors. The pipeline has four stages—seed filtering, distractor generation, distractor filtering, and question aggregation—with enumerated hyperparameters (for example, m1=4, n1=3, k1=8 for seeds; m3=4, n3=3, k3=7, k4=10 for distractors). The authors instantiate the framework as AlgGeoTest, a 456-item algebraic geometry benchmark with exactly two true and four false options per question, evaluate a large panel of LLMs, report score gaps and ranking changes relative to MATH-500 and AIME24, and describe an expert audit. They also propose a perplexity-based evaluation protocol for base models.

Significance. If the ground-truth labels of AlgGeoTest are correct, this is a significant contribution: it offers a scalable, domain-agnostic route to proof-centric benchmark construction, with explicitly listed pipeline parameters and publicly released code and benchmark data. The m-out-of-n design is a sensible response to the guessing problem and to inter-model variance in what counts as a correct proof, and the use of a human-curated reference corpus (The Stacks Project) provides a genuine external anchor for the true options. The central weakness is that the false-option labels are produced by an LLM judge panel that overlaps the set of evaluated models, and the reported human audit is not documented at item level; until this is addressed, the benchmark may be measuring agreement with a model consensus rather than mathematical truth, and the "profound deficits" conclusion is conditional on that consensus being correct.

major comments (3)
  1. [Filtration of Distractors; Audit Outcomes] The false ground-truth labels are not independent of the models later evaluated. The same four models used as judges (o3, Gemini-2.5-Pro, DeepSeek-R1, Qwen3-235B) appear in the evaluated-model list in Table 3 and Figure 2. The distractor retention rule (m3=4, n3=3, k3=7, k4=10) deliberately keeps items on which the panel is split: a distractor is retained when it is judged incorrect in 7 to 10 of 12 judgments, i.e., 2 to 5 judgments call it correct. Thus every retained false option is one on which the judge panel itself did not reach consensus. The expert audit in "Audit Outcomes" reports only aggregate percentages ("over 98.75%", "more than 95%") with no protocol, no auditor qualifications, no inter-rater statistics, and no item-level labels, so it does not resolve the circularity. The paper should provide an independent documented audit with item-level results, use a judge panel disjoint from the evaluated models, or otherwise demonstrate that the false labels are mathematical truths rather than a model-consensus artifact.
  2. [Filtration of Seed Items; Audit Outcomes] The claim that difficult seeds will not be discarded is an unsupported assumption that is in tension with the paper's own error analysis. In "Filtration of Seed Items" the authors assert that when a model cannot fully understand a proof, "it is unable to identify any flaws and consequently deems the definition or proof mathematically correct," so hard items survive the k1=8 threshold. However, "Audit Outcomes" states that model failures on AlgGeoTest include a "hallucinated belief that a valid item is inconsistent." If a judge model can falsely reject a valid proof during seed filtering, then correct seeds receiving fewer than 8 of 12 correct votes are discarded, biasing the true options toward statements that the judge panel happens to accept. The paper should report the distribution of seed-item votes and provide evidence for the claimed asymmetry, or explicitly bound the resulting selection bias.
  3. [Perplexity-Based Evaluation] The perplexity-based protocol in this section assumes that the option with the lowest perplexity is the most mathematically correct. No calibration or validation is provided. The options in AlgGeoTest differ substantially in length, notation, and style (as the appendix examples show), so perplexity may track linguistic fluency or stylistic regularity rather than mathematical validity. The base-model scaling results in Figure 4 therefore do not by themselves establish that this protocol is a robust measure of mathematical correctness. The authors should validate the protocol on a labeled held-out set or compare it against a chance baseline and a known-answer sanity check before using it to support claims about base-model mathematical ability.
minor comments (5)
  1. [Generation of Distractors] The model name "Qwen2.5-72B-Insturct" appears to be a typo for "Qwen2.5-72B-Instruct".
  2. [Aggregation of Hybrid-Formatted Questions] The statement that it is "impossible for LLMs to guess the correct answer by simply comparing between different options" is too strong: even with distinct seed origins, models can still exploit stylistic or superficial cues, such as the presence of undefined lemmas or the length of a proof. Consider softening this claim.
  3. [Analysis of Hybrid Question Format] The formula "expected accuracy of 1/C(m,n)" is correct only under the assumption of uniform random selection of exactly m items without replacement; this assumption should be stated explicitly.
  4. [Audit Outcomes] The sentence "more than 95% of the benchmark questions meet the same standard, with every distractor satisfying the same stringent criteria" is ambiguous: it is unclear whether the 95% figure refers to questions whose every distractor passed the audit, and whether any questions or distractors were replaced or removed after the audit.
  5. [Appendix, Option F] The line "Differences Between Original Proof and Adapted Proof" refers to a definition, not a proof; it should read "Original Definition" for consistency.

Circularity Check

2 steps flagged · score 5.0 of 10

AlgGeoTest's false and true labels are assigned by the same LLM judge panel that is later evaluated, so the reported 'profound deficits' measure agreement with the panel's consensus rather than an independently established ground truth.

  1. self definitional [The Proof2Hybrid Framework, 'Filtration of Distractors']
    "In contrast to the seed item stage, we now retain only those distractors deemed incorrect in k3 to k4 occasions and discard the rest. ... In our scenario of producing AlgGeoTest, we pick m3 = 4, n3 = 3, k3 = 7, and k4 = 10, and the 4 leading LLMs we employed are o3 (OpenAI 2025c), Gemini-2.5-Pro (Google 2025), DeepSeek-R1 (Guo et al. 2025) and Qwen3-235B-A22B (Qwen Team 2025)."

    The ground-truth label 'False' for every retained distractor is defined operationally as 'deemed incorrect in 7-10 of 12 judgments' by o3, Gemini-2.5-Pro, DeepSeek-R1, and Qwen3-235B. The Experiments section then evaluates AlgGeoTest on these same models (Gemini-2.5-Pro, o3, DeepSeek-R1, Qwen3-235B-A22B are all in the evaluated list). A judge model's score is therefore the rate at which its own verdicts agree with the thresholded panel label it helped produce; it is not an independent measure of mathematical competence. For non-judge models, the test measures agreement with this panel's consensus.

  2. self definitional [The Proof2Hybrid Framework, 'Filtration of Seed Items']
    "We retain all seed items that were adjudicated mathematically correct on at least k1 occasions and exclude all others. ... In our AlgGeoTest production scenario, we pick m1 = 4, n1 = 3, and k1 = 8, and the 4 leading LLMs we employed are o3 (OpenAI 2025c), Gemini-2.5-Pro (Google 2025), DeepSeek-R1 (Guo et al. 2025) and Qwen3-235B-A22B (Qwen Team 2025)."

    The 'correct' seed items in AlgGeoTest are also selected by the same four models that later appear on the evaluated model list. Although the seeds originate from The Stacks Project, the retention criterion is a model-judgment threshold, so for the judge models the benchmark's true labels are validated by the very models being scored. This compounds the distractor-label circularity and means the benchmark's overall ground truth is a model-consensus construction rather than an externally fixed answer key.

full rationale

The core issue is that AlgGeoTest's answer key is produced by an LLM judge panel that overlaps the evaluated model set. In 'Filtration of Distractors', a distractor is kept only if the panel marks it incorrect on 7-10 of 12 judgments; in 'Filtration of Seed Items', seeds are kept only if the same panel marks them correct on at least 8 of 12 judgments. The Experiments section then scores those same models on the resulting benchmark, so for the four judge models the headline 'profound deficits' is partly a self-agreement score rather than an independent measure of algebraic-geometry ability. The paper does cite an external anchor: seeds come from The Stacks Project, and an expert audit is claimed ('over 98.75% of model-generated distractors are mathematically incorrect yet deceptively plausible'). If the audit were item-level and reproducible, it would break the circularity. As reported, it is aggregate-only, with no protocol or per-item labels, so the released benchmark's ground truth remains the judge panel's consensus. This is partial circularity, not a definitional collapse: the source corpus is human-authored and the audit, if substantiated, would be independent. Score 5 reflects that the central evaluation claim partially reduces to the panel's own judgments.

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

The framework does not introduce mathematical entities, but it depends on several external reliability assumptions and hand-tuned thresholds that determine what counts as a valid question.

free parameters (4)
  • Seed item filter (m1, n1, k1) = 4, 3, 8
    A seed is retained only if at least 8 of 12 LLM verdicts call it correct; chosen by authors and not independently optimized.
  • Distractor generation (m2, n2, k2) = 5, 6, 2
    Five models each generate 6 distractors, with 2 randomly chosen per model; controls diversity and pool size.
  • Distractor filter (m3, n3, k3, k4) = 4, 3, 7, 10
    A distractor is kept only if judged incorrect in 7 to 10 of 12 verdicts; this directly sets the benchmark's ground truth and is hand-selected.
  • Question format (m, n) = 2, 6
    Exactly 2 true items out of 6; chosen for difficulty, pool usage, and context length, and sets the guessing baseline to 1/15.
assumptions (4)
  • domain assumption The Stacks Project statements and proofs are mathematically correct.
    Seed items are extracted from 'The Stacks project' in Collection of Seed Items; no independent verification of each selected tag is provided.
  • domain assumption LLM judge threshold votes are a reliable proxy for mathematical truth of distractors.
    Distractor filtration keeps only items with 7 to 10 incorrect verdicts out of 12; this assumes the panel's majority errors are correct judgments.
  • ad hoc to paper Models that cannot fully understand a hard proof tend to call it correct, so hard items survive the seed filter.
    Stated explicitly in 'Filtration of Seed Items': 'Empirically, when the model encounters such questions... it is unable to identify any flaws and consequently deems the definition or proof mathematically correct.'
  • domain assumption For a proposition-proof pair, modifying only the proof while keeping the proposition yields an item whose truth value is determined by the modified proof.
    The Proof2X roadmap asserts that such adapted proofs are valid distractors; if the proposition itself is true and the proof is invalid, the item is false only under the convention that the item includes the proof.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Proof2Hybrid: Automatic Mathematical Benchmark Synthesis for Proof-Centric Problems." pith.science (2026). https://pith.science/paper/CTXNKC4R

@misc{pith2026250802208,
  author       = {Pith},
  title        = {Pith review of: Proof2Hybrid: Automatic Mathematical Benchmark Synthesis for Proof-Centric Problems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CTXNKC4R}},
  note         = {Machine review of arXiv:2508.02208}
}
abstract

Evaluating the mathematical capability of Large Language Models (LLMs) is a critical yet challenging frontier. Existing benchmarks fall short, particularly for proof-centric problems, as manual creation is unscalable and costly, leaving the true mathematical abilities of LLMs largely unassessed. To overcome these barriers, we propose Proof2Hybrid, the first fully automated framework that synthesizes high-quality, proof-centric benchmarks from natural language mathematical corpora. The key novelty of our solution is Proof2X, a roadmap of converting mathematical proofs into various kinds of questions that are easy to verify. Instructed by this roadmap, we propose a new type of hybrid-formatted questions, named ``$m$-out-of-$n$ multiple judge questions'', specifically designed to enable robust, automatic evaluation while being resilient to guessing and superficial pattern matching inherent in traditional formats. As a demonstration of our framework, we introduce AlgGeoTest, a benchmark for algebraic geometry--a frontier domain of modern mathematics--comprising 456 challenging items. Our extensive evaluations on state-of-the-art LLMs using AlgGeoTest reveal profound deficits in their comprehension of algebraic geometry, providing a more precise measure of their true mathematical capabilities. Our framework and benchmark pave the way for a new wave of in-depth research into the mathematical intelligence of AI systems.

Figures

Figures reproduced from arXiv: 2508.02208 by the authors.

Figure 1
Figure 1. Example of the full workflow of Proof2Hybrid in our scenario of producing AlgGeoTest. At the framework’s heart is a carefully orchestrated pipeline of powerful LLMs. First, a generation team of models crafts distractors by strategically altering keywords, conditions, or formulas in the original statements. Then, a separate judging team filters and refines these candidates, discarding any that are obviously wrong whi… view at source ↗
Figure 2
Figure 2. The evaluation results of AlgGeoTest on multiple LLMs. The evaluation results reveal that even the best-performing model to date achieves only a moderate score of around 60, with scores commonly lower than 20. This result underscores the rigorous and challenging nature of our benchmark. We also observe that reasoning models commonly outperform their non-reasoning counterparts, demonstrating that our benchmark effect… view at source ↗
Figure 3
Figure 3. Pros and Cons comparison between true-or-false [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Performance evaluation across families of base [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: Two scatter plots comparing the performance of various LLMs on AlgGeoTest versus MATH-500 and AIME24. Both plots include a linear regression line with a shaded confidence interval, and the R-squared value is displayed in the top-left corner of each plot. As we can see,…

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

43 extracted references · 25 canonical work pages

  1. [1]

    Abels, A.; and Lenaerts, T. 2025. Wisdom from Diversity: Bias Mitigation Through Hybrid Human‑LLM Crowds. arXiv preprint arXiv:2505.12349. Accepted for publication in IJCAI 2025; hybrid crowd-based bias mitigation study

    arXiv 2025

  2. [2]

    AI, M. 2024. Llama 3.1: Dense Language Models up to 405B Parameters. Technical documentation / Whitepaper. Dense family up to 405 B parameters; trained on 15.6T tokens

    work page 2024

  3. [3]

    AI, M. 2025. Kimi-K2: A Trillion-Parameter Open-Source Agentic Language Model. GitHub repository and model card. Released July 2025; utilizes a mixture-of-experts architecture with 32B active parameters per forward pass; optimized for agentic tasks and tool integration

    work page 2025

  4. [4]

    Alibaba Cloud Qwen Team . 2025 a . Qwen3‑30B‑A3B: A 30B MoE Model with Hybrid Reasoning Modes and Long‑Context Support. Qwen3 Technical Report, Model Card (Apache 2.0, Hugging Face). Supports enable thinking mode (complex reasoning) or fast mode interchangeably; 30.5B total vs. 3.3B active params; context up to 131K

    work page 2025

  5. [5]

    Alibaba Cloud Qwen Team . 2025 b . QwQ‑32B: A Compact 32B‑Parameter Reasoning Model with Reinforcement Learning and 131K‑Token Context Support. Alibaba Cloud Blog, Qwen Technical Blog. Released March 5, 2025; achieves performance comparable to DeepSeek‑R1 and OpenAI's o1‑mini on reasoning benchmarks

    work page 2025

  6. [6]

    Anthropic. 2025 a . Claude 4 Opus. Accessed: 2025-06-01

    work page 2025

  7. [7]

    Anthropic. 2025 b . Claude 4 Sonnet: A Cost‑Effective Hybrid‑Reasoning Model Optimized for Coding and Agentic Workflows. Public release / Model card on Anthropic Website and Shared via API Platforms. Released May 22 2025 alongside Claude 4 Opus as a midsize hybrid‐reasoning model

    work page 2025

  8. [8]

    Cai, K.; and Singh, J. 2025. Google clinches milestone gold at global math competition, while OpenAI also claims win. Reuters. Accessed: 2025‑07‑25

    work page 2025

Show all 43 references
  1. [9]

    Cobbe, K.; Kosaraju, V.; Bavarian, M.; Chen, M.; Jun, H.; Kaiser, L.; Plappert, M.; Tworek, J.; Hilton, J.; Nakano, R.; Hesse, C.; and Schulman, J. 2021. Training Verifiers to Solve Math Word Problems. arXiv preprint arXiv:2110.14168

    2021 arXiv

  2. [10]

    de Moura, L.; and Ullrich, S. 2021. The Lean 4 Theorem Prover and Programming Language. Reimplementation of Lean in Lean itself, addressing previous shortcomings and introducing new features

    2021

  3. [11]

    DeepMind, G. 2025. Gemini 2.5 Flash: A Cost‑Efficient Hybrid Reasoning Model for Multimodal and Long‑Context Tasks. Google Developers Blog. Released June 17, 2025; optimized for low latency and efficiency with adjustable thinking budget, supports multimodal input up to 1 milli...

    2025

  4. [12]

    DeepSeek‑AI . 2025. DeepSeek‑R1‑Distill‑Qwen‑32B: A 32 B model distilled from DeepSeek‑R1 with state‑of‑the‑art reasoning performance. Model card on Hugging Face / DeepSeek Platform. Achieves 72.6

    2025

  5. [13]

    DeepSeek‑AI; Liu, A.; Feng, B.; Xue, B.; Wang, B.; Zhao, C.; et al. 2024. DeepSeek‑V3 Technical Report. arXiv preprint arXiv:2412.19437. Deep mixture‑of‑experts LLM (671B params; 37B activated); trained on 14.8T tokens, cost approximately 5.6M dollars using 2.788M H800 GPU‑hours

    2024 arXiv

  6. [14]

    Gao, B.; Song, F.; Yang, Z.; Cai, Z.; Miao, Y.; Dong, Q.; Li, L.; Ma, C.; Chen, L.; Xu, R.; Tang, Z.; Wang, B.; Zan, D.; Quan, S.; Zhang, G.; Sha, L.; Zhang, Y.; Ren, X.; Liu, T.; and Chang, B. 2024. Omni‑MATH: A Universal Olympiad Level Mathematical Benchmark for Large Langua...

    2024 arXiv

  7. [15]

    Glazer, E.; Erdil, E.; Besiroglu, T.; Chicharro, D.; Chen, E.; Gunning, A.; Olsson, C. F.; Denain, J.; Ho, A.; de Oliveira Santos, E.; Järviniemi, O.; Barnett, M.; Sandler, R.; Vrzala, M.; Sevilla, J.; Ren, Q.; Pratt, E.; Levine, L.; Barkley, G.; Stewart, N.; Grechuk, B.; Grec...

    2024 arXiv

  8. [16]

    Google. 2025. Gemini 2.5 Pro. Accessed: 2025-06-01

    2025

  9. [17]

    Guo, D.; Yang, D.; Zhang, H.; Song, J.; and et al., L. W. 2025. DeepSeek‑R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning. arXiv preprint arXiv:2501.12948. Introduces the open-source reasoning model DeepSeek‑R1, trained via RL to rival OpenAI o1 on mat...

    2025 arXiv

  10. [18]

    Hendrycks, D.; Burns, C.; Kadavath, S.; Arora, A.; Basart, S.; Tang, E.; Song, D.; and Steinhardt, J. 2021. Measuring Mathematical Problem Solving With the MATH Dataset. arXiv preprint arXiv:2103.03874. Dataset of 12,500 challenging competition mathematics problems

    2021 arXiv

  11. [19]

    Huang, Y.; and Yang, L. F. 2025. Gemini 2.5 Pro Capable of Winning Gold at IMO 2025. arXiv preprint arXiv:2507.15855. Demonstrates solving 5 out of 6 IMO 2025 problems using Gemini 2.5 Pro with a verification pipeline

    2025

  12. [20]

    IMO-Board, T. 2025. International Mathematical Olympiad. Accessed: 2025-06-01

    2025

  13. [21]

    (Maxwell‐Jia), M. J. 2024. AIME 2024 Dataset. Hugging Face Dataset. Available at https://huggingface.co/datasets/Maxwell-Jia/AIME_2024

    2024

  14. [22]

    Morris, R. L. 2020. Motivated Proofs: What They Are, Why They Matter and How to Write Them. arXiv preprint arXiv:2001.02657. Forthcoming in *The Review of Symbolic Logic*; DOI:10.1017/S1755020319000583

    2020 arXiv

  15. [23]

    C.; and Wenzel, M

    Nipkow, T.; Paulson, L. C.; and Wenzel, M. 2002. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. In Lecture Notes in Computer Science, volume 2283, 378--388. Springer

    2002

  16. [24]

    OpenAI. 2024. GPT‑4o (``Omni''): A Multimodal Transformer Capable of Text, Vision, and Audio. OpenAI Blog and System Card. Released May 13 2024; integrates text, image, and audio in a single end‑to‑end model using the same neural network

    2024

  17. [25]

    OpenAI. 2025 a . Introducing GPT‑4.1: Enhanced Coding, Instruction Following, and Long‑Context Capabilities. OpenAI Technical Blog. Released April 14, 2025; supports up to 1M‑token context window

    2025

  18. [26]

    OpenAI. 2025 b . Introducing o4‑mini: Cost‑efficient and image‑capable reasoning model. OpenAI Blog and System Card. Released April 16, 2025; supports reasoning with images, tools, and Python execution

    2025

  19. [27]

    OpenAI. 2025 c . OpenAI o3: A New Frontier in Reasoning Models. OpenAI Technical Blog. Introduced the o‑series reasoning model o3, designed for deep logical reasoning and benchmarking

    2025

  20. [28]

    Paulin-Mohring, C. 2012. Introduction to the Coq Proof‑Assistant for Practical Software Verification. In Tools for Practical Software Verification, LASER 2011, volume 7682 of Lecture Notes in Computer Science, 45--95. Springer

    2012

  21. [29]

    Phan, L.; Gatti, A.; Han, Z.; Li, N.; Hu, J.; Zhang, H.; Shi, S.; Choi, M.; Agrawal, A.; Chopra, A.; et al. 2025. Humanity’s Last Exam. arXiv preprint arXiv:2501.14249. CC BY 4.0 license; publicly released as the HLE benchmark

    2025 arXiv

  22. [30]

    Qwen Team, A. C. 2024. Qwen2.5‑72B‑Instruct: A 72‑billion‑parameter instruction‑tuned model with long‑context support and strong math and reasoning performance. Model card on Hugging Face and Alibaba Cloud Model Studio. Outperforms larger models on benchmarks including MATH, M...

    2024

  23. [31]

    thinking

    Qwen Team, A. C. 2025. Qwen3‑235B‑A22B: A Mixture‑of‑Experts LLM with Thinking Mode for Advanced Reasoning and Long‑Context Processing. Technical Model Card (Hugging Face / Official Documentation). Release date May 21 2025; features 235B total parameters (22B active modes), su...

    2025

  24. [32]

    Stacks-Project-Authors, T. 2025. The Stacks Project. https://stacks.math.columbia.edu. Accessed: 2025‑06‑01

    2025

  25. [33]

    X.; Liu, Z.; Wang, Z.; Fang, L.; and Wen, J.-R

    Sun, H.; Min, Y.; Chen, Z.; Zhao, W. X.; Liu, Z.; Wang, Z.; Fang, L.; and Wen, J.-R. 2025. Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models. arXiv:2503.21380

    2025 arXiv

  26. [34]

    Tsoukalas, G.; Lee, J.; Jennings, J.; Xin, J.; Ding, M.; Jennings, M.; Thakur, A.; and Chaudhuri, S. 2024. PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition. arXiv:2407.11214

    2024 arXiv

  27. [35]

    Vendrow, J.; Vendrow, E.; Beery, S.; and Madry, A. 2025. Do Large Language Model Benchmarks Test Reliability? arXiv preprint arXiv:2502.03461. Submitted February 5, 2025

    2025 arXiv

  28. [36]

    Wang, P.; Liu, T.; Wang, C.; Wang, Y.; Yan, S.; Jia, C.; Li, Z.; Liu, X.; Chen, X.; Xu, J.; and Yu, Y. 2025. A Survey on Large Language Models for Mathematical Reasoning. arXiv preprint arXiv:2506.08446. Https://arxiv.org/abs/2506.08446

    2025 arXiv

  29. [37]

    Wang, Y.; Ma, X.; Zhang, G.; Ni, Y.; Chandra, A.; Guo, S.; Ren, W.; Arulraj, A.; He, X.; Jiang, Z.; Li, T.; Ku, M.; Wang, K.; Zhuang, A.; Fan, R.; Yue, X.; and Chen, W. 2024. MMLU‑Pro: A More Robust and Challenging Multi‑Task Language Understanding Benchmark. arXiv preprint ar...

    2024 arXiv

  30. [38]

    xAI (Elon Musk’s AI Company). 2025. Grok 4: A Reasoning-Capable Multimodal Model with Native Tool Use and Real-Time Search Integration. Model announcement and documentation via xAI website. Released July 9, 2025; supports image/text inputs, structured outputs, tool use, and 25...

    2025

  31. [39]

    Yang, A.; Li, A.; Yang, B.; Zhang, B.; Hui, B.; Gao, C.; Huang, C.; Lv, C.; Zhou, F.; Huang, F.; Zhang, J.; Zhou, J.; Lin, J.; Deng, L.; Li, T.; et al. 2025. Qwen3 Technical Report. arXiv preprint arXiv:2505.09388. Introduces the Qwen3 model family including the 32B dense vari...

    2025 arXiv

  32. [40]

    Yang, A.; Yang, B.; Hui, B.; Zheng, B.; Yu, B.; Zhou, C.; Li, C.; Liu, D.; Huang, F.; et al. 2024. Qwen 2.5 Technical Report. arXiv preprint arXiv:2412.15115. Introduces open-weight Qwen 2.5 LLM family (0.5B–72B) and MoE variants Qwen2.5‑Turbo/Plus

    2024 arXiv

  33. [41]

    M.; and Polu, S

    Zheng, K.; Han, J. M.; and Polu, S. 2022. MiniF2F: A Cross-System Benchmark for Formal Olympiad-Level Mathematics. In Proceedings of the 10th International Conference on Learning Representations (ICLR 2022). Accessed: 2025-07-25

    2022

  34. [42]

    , " * write output.state after.block = add.period write newline

    ENTRY address archivePrefix author booktitle chapter edition editor eid eprint howpublished institution isbn journal key month note number organization pages publisher school series title type volume year label extra.label sort.label short.list INTEGERS output.state before.all...

  35. [43]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 gl...

Pith tools

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