Pith. sign in

REVIEW 2 major objections 7 minor 299 references

AI formal math systems must stop acting as competition solvers and become research agents that can tackle open, under-specified frontier problems with machine-checked reasoning.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · grok-4.5

2026-07-10 18:15 UTC pith:2WNC2JY2

load-bearing objection Solid, high-signal position paper: clean taxonomy plus the first structured six-category snapshot of AI work on Erdős problems; the five-pillar roadmap is useful advocacy, not a new theorem. the 2 major comments →

arxiv 2607.07779 v1 pith:2WNC2JY2 submitted 2026-07-08 cs.CL cs.AI

From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

Eric Jiang , Xiao Liang , Yikai Zhang , Yingjia Wan , Mengting Li , Haikang Deng , Alexander K. Taylor , Justin Baker
show 11 more authors
Rushil Raghavan Junyi Zhang Ying Nian Wu Andrea L. Bertozzi Kai-Wei Chang Raghu Meka Matthew Sottile Nanyun Peng Amit Sahai Terence Tao Wei Wang
This is my paper
classification cs.CL cs.AI MSC 68T0103B3568T27
keywords AI for mathematicsformal theorem provinglarge language modelsresearch agentsautoformalizationinteractive theorem provingmathematical discoveryhuman-AI collaboration
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

Today's large language model theorem provers can generate machine-checked proofs for well-posed competition problems, but they still behave like solvers of fixed tasks rather than researchers who invent theorems, formalize open conjectures, and explore under-specified frontiers. This position paper reviews the data, autoformalization methods, training recipes, search strategies, and agentic workflows that produced recent gains, and documents where those systems stand on research-level targets such as Erdős problems. It then argues that genuine progress requires five shifts: better formal data and evaluation of statement fidelity, modeling of deep relationships among theorems rather than isolated proofs, tools for open-ended discovery and conjecturing, a unified ecosystem of external mathematical tools with certificates, and tight human-AI collaboration with explainable interaction. If those barriers are closed, the field can move from saturating Olympiad benchmarks to contributing new formal mathematics at the research frontier.

Core claim

The central claim is that the next leap in AI for formal mathematics is not another incremental solver for predefined problems, but a decisive shift to research agents that can address open-ended, under-specified frontier challenges under rigorous interactive theorem proving. Current systems excel at isolated, well-defined proof generation and have largely saturated MiniF2F and reached medal-level IMO performance, yet their contributions to open Erdős problems are mostly literature review, formalization, or rediscovery of known results rather than genuine discovery. Closing five structural gaps—data and evaluation, relational structure, mathematical exploration, tool integration, and human-A

What carries the argument

The five strategic pillars that separate competition solvers from research agents: (1) limitations of formal math data and fidelity-aware evaluation, (2) shifting from isolated proofs to deep relational structure and knowledge graphs, (3) evolving from verification to discovery and conjecturing, (4) external tool integration with certificate reconstruction, and (5) human-AI collaboration with explainable interaction.

Load-bearing premise

The paper assumes that these five barriers are the main obstacles, and that closing them will be enough to turn today's solvers into genuine research-level agents rather than merely stronger competition provers.

What would settle it

A sustained series of AI-primary full solutions to long-standing open problems (for example several Erdős problems with no prior known work, or a non-trivial Millennium-adjacent result) that introduce new concepts or constructions, pass independent statement-fidelity checks against the original informal claims, and are accepted by working mathematicians as novel—without the solutions later collapsing into rediscovery or weakened formalizations.

Watch this falsifier — get emailed when new claim-graph text bears on it.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 7 minor

Summary. This position paper argues that LLM-driven formal mathematics has largely produced competition-style solvers and must shift toward research agents capable of open-ended discovery under machine-checked reasoning. It surveys foundations (ITPs, foundation models, autoformalization, standard neuro-symbolic workflows), offers a taxonomy of training, test-time, and agentic methods, and documents the empirical landscape via MiniF2F saturation, IMO-level results, a categorized compilation of AI contributions to Erdős problems (Table 6, Figure 6), and canonical open-problem lists (Table 7). It then identifies five barriers—formal data/evaluation fidelity, relational structure, exploration/discovery, tool ecosystems, and human–AI collaboration—and sketches a roadmap including synthetic curricula, knowledge graphs, evolutionary conjecturing, certificate-producing tools, and collaborative interfaces.

Significance. As a position paper the contribution is synthetic and agenda-setting rather than a new theorem or system. Its value lies in a coherent taxonomy that connects datasets, autoformalization, training, search, and agent workflows; a structured, caveat-aware snapshot of AI activity on genuine open Erdős problems (including selection bias, rediscovery, and the Aristotle #124 specification-fidelity failure); and a concrete five-pillar roadmap that is actionable for the community. Strengths include explicit caveats on selection bias and statement fidelity, extensive comparative tables (Tables 1–7), and concrete failure case studies in the appendix. If the field adopts the framing, the paper can usefully reorient evaluation and system design away from saturated competition benchmarks toward research-grade formal agents.

major comments (2)
  1. §5 opening and the five pillars: the central advocacy claim treats the five barriers as the primary load-bearing obstacles separating solvers from research agents. The manuscript does not provide a comparative argument that these five dominate alternatives (e.g., compute scale, pure informal LRMs, or domain-specific formalization campaigns). A short subsection that either (i) justifies primacy relative to plausible alternatives or (ii) explicitly frames the five as a working agenda rather than a complete causal account would make the roadmap more defensible without changing the paper’s position-paper character.
  2. §4.3, Table 6 and Figure 6: the Erdős compilation is a major empirical pillar, yet counts are approximate, multi-category, and drawn from a community wiki with ongoing updates. The text already notes selection bias and rediscovery, but the table/figure presentation still risks being read as a success-rate claim. Adding an explicit denominator (attempted vs. reported), a snapshot date, and a short protocol for inclusion/exclusion would make this evidence load-bearing rather than anecdotal while preserving the qualitative shift the authors correctly emphasize.
minor comments (7)
  1. Abstract and §1: ‘has achieved’ / subject–verb agreement and a few other small grammar issues (e.g., ‘decisiveshift’) should be cleaned for journal style.
  2. Table 1: ‘samlpes’ typo; also clarify whether pretraining token counts are comparable across formal vs. informal corpora given different tokenization.
  3. Table 5 / IMO notes: ‘sovled’ typos and inconsistent date/source footnotes; align with the MathArena and system-card citations already used.
  4. §2.5 vs. §2.6: autoformalization is introduced twice with overlapping content; a single consolidated subsection would improve flow.
  5. Figure 6 caption cites ‘as of April 14, 2026’ while Table 6 says ‘as of January 2026’; reconcile snapshot dates.
  6. §5.4 invents ‘Proof Agent Interface Protocol (PAIP)’ without a minimal interface sketch or comparison to existing MCP/LeanDojo-style APIs; a short box or appendix outline would make the proposal less free-floating.
  7. Appendix C case studies are strong; cross-reference them more explicitly from §5.1 so the specification-fidelity argument is not only in the main text’s Aristotle example.

Circularity Check

0 steps flagged

No circularity: position paper with no derivation that reduces to its inputs by construction.

full rationale

This is a position paper advocating a shift from competition-style solvers to research agents and surveying datasets, autoformalization, proof synthesis, and five open challenges. It advances no theorem, fitted parameter, uniqueness claim, or first-principles prediction whose validity is forced by its own definitions or by a self-citation chain. Empirical material (MiniF2F saturation, IMO scores, Erdős contribution tallies) is drawn from external systems, public community trackers, and independent reports; the authors themselves flag selection bias and specification-fidelity failures (e.g., Aristotle on a weakened #124). Self-citations appear only as ordinary literature pointers within a broad survey and are not load-bearing for any claimed derivation. There is therefore no circular step to report.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 2 invented entities

Position paper; load-bearing premises are domain assumptions about the necessity of formal verification and the sufficiency of the five identified barriers. No free parameters are fitted. Two proposed constructs (research agents as a system class, PAIP) are introduced as design targets rather than observed entities.

axioms (3)
  • domain assumption Machine-checkable formal proofs are a prerequisite for trustworthy autonomous mathematical research agents.
    Stated throughout §1–2 and used to motivate the entire formal-AI focus; not proved, taken as definitional for the research program.
  • ad hoc to paper The five barriers (data, relational structure, exploration, tools, human–AI collaboration) are the primary obstacles separating competition solvers from research agents.
    Organizing claim of §5; alternative taxonomies (e.g., pure compute scaling or pure informal reasoning) are possible but not refuted.
  • domain assumption Current AI ‘solutions’ to many Erdős problems largely rediscover literature results rather than produce genuinely novel mathematics.
    Supported by the authors’ own classification in Table 6 and the community wiki; treated as empirical background.
invented entities (2)
  • Proof Agent Interface Protocol (PAIP) no independent evidence
    purpose: Proposed unified interface so agents can call heterogeneous ITPs, SMT solvers, and CAS without system-specific glue.
    Introduced in §5.4 as a design recommendation; no implementation or independent evidence yet.
  • Mathematical research agents (as a system class) no independent evidence
    purpose: End-to-end agents that conjecture, formalize, explore, and collaborate rather than solve fixed statements.
    Central framing of the paper; aspirational rather than an already-existing, independently measured object.

pith-pipeline@v1.1.0-grok45 · 51816 in / 2306 out tokens · 37198 ms · 2026-07-10T18:15:46.694031+00:00 · methodology

0 comments
read the original abstract

Recent developments in AI for Mathematics (AI4Math), especially Large Language Model (LLM)-driven theorem provers, has achieved remarkable success in formal proof generation for well-defined mathematical problems through Interactive Theorem Proving (ITP) languages. However, current systems remain fundamentally limited in tackling frontier research mathematics, such as discovering new theorems or resolving open conjectures, which are often open-ended, under-specified, and involve multiple layers of abstraction. We argue that the next leap in AI4Math systems requires a decisive shift from predefined problem-solvers to research agents that can address frontier mathematical challenges with rigorous formal mathematical reasoning. In this position paper, we provide a systematic review of the field, covering datasets, auto-formalization, and proof synthesis. More importantly, we identify core limitations of existing systems in serving as mathematical research agents, examining issues across datasets, relational structure, mathematical exploration, tool ecosystem, and human-AI collaboration, outlining a strategic road-map for the future of AI4Math.

Figures

Figures reproduced from arXiv: 2607.07779 by Alexander K. Taylor, Amit Sahai, Andrea L. Bertozzi, Eric Jiang, Haikang Deng, Junyi Zhang, Justin Baker, Kai-Wei Chang, Matthew Sottile, Mengting Li, Nanyun Peng, Raghu Meka, Rushil Raghavan, Terence Tao, Wei Wang, Xiao Liang, Yikai Zhang, Yingjia Wan, Ying Nian Wu.

Figure 1
Figure 1. Figure 1: The Neuro-Symbolic Interaction Loop. This diagram illustrates the iterative workflow where the Symbolic Environment (ITP) maintains the logical state and provides verifiable feedback (progress, errors, or completion), while the Neural Component (LLM) acts as a generative policy to construct prompts and predict tactic candidates based on the serialized context. Level Dataset Scale (token/sample) Description… view at source ↗
Figure 2
Figure 2. Figure 2: Outline-style taxonomy of LLM-based neural theorem proving methods, organized by training [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Overview of the DeepSeek-Prover Framework. It proceeds in three phases: (1) Autoformalization (& Filtering) to convert informal problems into high-quality formal statements; (2) Proof Search & Verification where the model generates proof candidates that are rigorously checked by a formal verifier (e.g., Lean); and (3) Training, where successful proofs are used to fine-tune the policy model for the next ite… view at source ↗
Figure 4
Figure 4. Figure 4: Test-time Adaptation Strategies for LLM-based Provers. An overview of various test-time scaling and adaptation methods, including search algorithms, planning strategies, and retrieval-augmented approaches that enhance proof generation at inference time. favor hybrid settings where informal reasoning is used to guide formal proof generation. Such informal reasoning is shown to be effective for problem decom… view at source ↗
Figure 5
Figure 5. Figure 5: Agentic formal theorem proving with subgoal caching and parallel verification An illustrative workflow in which a natural-language mathematical statement is autoformalized into a formal theorem, decomposed by a planner into intermediate subgoals, and solved via multiple parallel prover agents. To overcome reasoning bottlenecks, a key feature of agentic systems is to utilize diverse tools and engage with fo… view at source ↗
Figure 6
Figure 6. Figure 6: Cumulative progress of AI contributions to Erd˝os problems, categorized by contribution type. Data sourced from the community-maintained wiki at erdosproblems.com (as of April 14, 2026). Numbers in parentheses indicate total unique problems per category. A single problem may appear in multiple categories. capabilities on problems that require genuine domain expertise rather than retrieval of known solution… view at source ↗
Figure 7
Figure 7. Figure 7: A structured mathematical knowledge graph for relationship-aware reasoning. A conceptual illustration of a layered mathematical knowledge graph connecting informal mathematical concepts, formal lemmas, and tactic-level proof fragments. Such structure enables inexact subgraph matching and abstraction￾based retrieval, allowing provers to exploit recurring proof patterns and deep relationships beyond isolated… view at source ↗
Figure 8
Figure 8. Figure 8: Overview of the AlphaEvolve Framework in LEAN. AlphaEvolve showcases mathematical exploration as an evolutionary process in which LLMs propose mutations to formal programs or conjectures, guided by task-specific scoring functions and verified within a formal environment. 5.4 External Tool Integration and Refinement To act as effective research assistants, AI4Math systems must orchestrate a diverse ecosyste… view at source ↗
Figure 9
Figure 9. Figure 9: Human-AI Collaboration in Mathematical Research. An illustration of the collaborative workflow between human mathematicians and AI systems, highlighting the complementary strengths of human insight and AI-powered automation in formal theorem proving. We argue that the ultimate goal of AI4Math should not be autonomous theorem proving, but rather col￾laborative systems that amplify human mathematical ability… view at source ↗
Figure 10
Figure 10. Figure 10: Common failure cases in LLM-driven formal mathematics. Illustrative examples of how errors introduced during translation and proof construction (e.g., missing implicit constraints, ambiguous notation/indexing, specification drift, or mismatched library choices) propagate into different downstream failure types (syntactic, semantic, search, and strategic) across autoformalization, prover search, and the Le… view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

299 extracted references · 299 canonical work pages · 84 internal anchors

  1. [1]

    Learning to guide a saturation-based theorem prover.IEEE Transactions on Pattern Analysis and Machine Intelligence, 45(1): 738–751, 2022

    Ibrahim Abdelaziz, Maxwell Crouse, Bassem Makni, Vernon Austel, Cristina Cornelio, Shajith Ikbal, Pavan Kapanipathi, Ndivhuwo Makondo, Kavitha Srinivas, Michael Witbrock, et al. Learning to guide a saturation-based theorem prover.IEEE Transactions on Pattern Analysis and Machine Intelligence, 45(1): 738–751, 2022

    work page 2022

  2. [2]

    Blumberg, Martin Hairer, Joe Kileel, Tamara G

    Mohammed Abouzaid, Andrew J. Blumberg, Martin Hairer, Joe Kileel, Tamara G. Kolda, Paul D. Nelson, Daniel Spielman, Nikhil Srivastava, Rachel Ward, Shmuel Weinberger, and Lauren Williams. First proof.arXiv preprint arXiv:2602.05192, 2026

    work page arXiv 2026

  3. [3]

    GPT-4 Technical Report

    Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. Gpt-4 technical report. arXiv preprint arXiv:2303.08774, 2023

    work page internal anchor Pith review Pith/arXiv arXiv 2023

  4. [4]

    Aristotle: IMO-level Automated Theorem Proving

    Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Mathïs Fédérico, Sergei Gukov, Daniel Halpern- Leistner, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, et al. Aristotle: Imo-level automated theorem proving.arXiv preprint arXiv:2510.01346, 2025

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  5. [5]

    Improver: Agent-based automated proof optimization

    Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, and Sean Welleck. Improver: Agent-based automated proof optimization. InThe Thirteenth International Conference on Learning Representations, ICLR 2025, Singapore, April 24-28, 2025. OpenReview.net, 2025. URLhttps://openreview.net/forum?id=dWsdJAXjQD

    work page 2025

  6. [6]

    Proofnet++: A neuro-symbolic system for formal proof verification with self-correction, 2025

    Murari Ambati. Proofnet++: A neuro-symbolic system for formal proof verification with self-correction, 2025

    work page 2025

  7. [7]

    Claude 3.5 sonnet model card addendum

    Anthropic. Claude 3.5 sonnet model card addendum. https://www.anthropic.com, 2024. Accessed: November 28, 2024

    work page 2024

  8. [8]

    Claude opus 4 & claude sonnet 4 system card

    Anthropic. Claude opus 4 & claude sonnet 4 system card. Anthropic Technical Report, 2025

    work page 2025

  9. [9]

    Springer Nature, 2005

    Vladimir I Arnold.Arnold’s Problems. Springer Nature, 2005

    work page 2005

  10. [10]

    A formally verified proof of the central limit theorem

    Jeremy Avigad, Johannes Hölzl, and Luke Serafin. A formally verified proof of the central limit theorem. Journal of Automated Reasoning, 59(4):389–423, 2017

    work page 2017

  11. [11]

    An answer to hellman: Category theory is a framework for mathematical structuralism

    Steve Awodey. An answer to hellman: Category theory is a framework for mathematical structuralism. Philosophia Mathematica, 2004

    work page 2004

  12. [12]

    Ayers, Dragomir Radev, and Jeremy Avigad

    Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics, 2023

    work page 2023

  13. [13]

    Llemma: An Open Language Model For Mathematics

    Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. arXiv preprint arXiv:2310.10631, 2024

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  14. [14]

    Neural operators for accelerating scientific simulations and design.Nature Reviews Physics, 2024

    Kamyar Azizzadenesheli, Nikola Kovachki, Zongyi Li, Miguel Liu-Schiaffini, Jean Kossaifi, and Anima Anandkumar. Neural operators for accelerating scientific simulations and design.Nature Reviews Physics, 2024

    work page 2024

  15. [15]

    Prover agent: An agent-based framework for formal mathematical proofs.arXiv preprint arXiv:2506.19923, 2025

    Kaito Baba, Chaoran Liu, Shuhei Kurita, and Akiyoshi Sannai. Prover agent: An agent-based framework for formal mathematical proofs.arXiv preprint arXiv:2506.19923, 2025

    work page arXiv 2025

  16. [16]

    Kimi K2: Open Agentic Intelligence

    Yifan Bai, Yiping Bao, Guanduo Chen, et al. Kimi k2: Open agentic intelligence.arXiv preprint arXiv:2507.20534, 2025

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  17. [17]

    Beyond accuracy: The role of mental models in human-ai team performance.AAAI Conference on Human Computation and Crowdsourcing, 2019

    Gagan Bansal, Besmira Nushi, Ece Kamar, Daniel S Weld, Walter S Lasecki, and Eric Horvitz. Beyond accuracy: The role of mental models in human-ai team performance.AAAI Conference on Human Computation and Crowdsourcing, 2019

    work page 2019

  18. [18]

    Holist: An environment for machine learning of higher-order theorem proving.International Conference on Machine Learning, pp

    Kshitij Bansal, Sarah M Loos, Markus N Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher-order theorem proving.International Conference on Machine Learning, pp. 454–463, 2019. 22

    work page 2019

  19. [19]

    Better smt proofs for easier reconstruction

    Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine, and Hans-Jörg Schurr. Better smt proofs for easier reconstruction. InAITP 2019-4th Conference on Artificial Intelligence and Theorem Proving, 2019

    work page 2019

  20. [20]

    cvc5: A versatile and industrial-strength smt solver

    Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdal- rhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, et al. cvc5: A versatile and industrial-strength smt solver. InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2022

    work page 2022

  21. [21]

    Irrationality of rapidly converging series: a problem of Erd\H{o}s and Graham

    Kevin Barreto, Jiwon Kang, Sang-hyun Kim, Vjekoslav Kovaˇ c, and Shengtong Zhang. Irrationality of rapidly converging series: A problem of Erd˝ os and Graham.arXiv preprint arXiv:2601.21442, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  22. [22]

    Springer Science & Business Media, 2013

    Yves Bertot and Pierre Castéran.Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer Science & Business Media, 2013

    work page 2013

  23. [23]

    Graph of thoughts: Solving elaborate problems with large language models.AAAI, 2024

    Maciej Besta, Nils Blach, Ales Kubicek, Robert Gerstenberger, Michal Podstawski, Lukas Gianinazzi, Joanna Gajda, Tomasz Lehmann, Hubert Niewiadomski, Piotr Nyczyk, et al. Graph of thoughts: Solving elaborate problems with large language models.AAAI, 2024

    work page 2024

  24. [24]

    Automathkg: The automated mathematical knowledge graph based on llm and vector database.Computational Intelligence, 41(4):e70096, 2025

    Rong Bian, Yu Geng, Zijian Yang, and Bing Cheng. Automathkg: The automated mathematical knowledge graph based on llm and vector database.Computational Intelligence, 41(4):e70096, 2025

    work page 2025

  25. [25]

    Hammering towards qed.Journal of Formalized Reasoning, 9(1):101–148, 2016

    Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C Paulson, and Josef Urban. Hammering towards qed.Journal of Formalized Reasoning, 9(1):101–148, 2016

    work page 2016

  26. [26]

    Springer, 2008

    John Adrian Bondy and Uppaluri S R Murty.Graph Theory. Springer, 2008

    work page 2008

  27. [27]

    Promising directions of machine learning for partial differential equations.Nature Computational Science, 2024

    Steven L Brunton and J Nathan Kutz. Promising directions of machine learning for partial differential equations.Nature Computational Science, 2024

    work page 2024

  28. [28]

    Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models

    Chenrui Cao, Liangcheng Song, Zenan Li, Xinyi Le, Xian Zhang, Hui Xue, and Fan Yang. Reviving dsp for advanced theorem proving in the era of reasoning models.arXiv preprint arXiv:2506.11487, 2025

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  29. [29]

    American Mathematical Society, 2006

    James Carlson, Arthur Jaffe, and Andrew Wiles.The Millennium Prize Problems. American Mathematical Society, 2006

    work page 2006

  30. [30]

    Anti-unification and Generalization: A Survey

    David M Cerna and Temur Kutsia. Anti-unification and generalization: a survey.arXiv preprint arXiv:2302.00277, 2023

    work page internal anchor Pith review Pith/arXiv arXiv 2023

  31. [31]

    Reform: Reflective autoformalization with prospective bounded sequence optimization.arXiv preprint arXiv:2510.24592, 2025

    Guoxin Chen, Jing Wu, Xinjie Chen, Wayne Xin Zhao, Ruihua Song, Chengxi Li, Kai Fan, Dayiheng Liu, and Minpeng Liao. Reform: Reflective autoformalization with prospective bounded sequence optimization.arXiv preprint arXiv:2510.24592, 2025

    work page arXiv 2025

  32. [32]

    Seed-prover 1.5: Mastering undergraduate-level theorem proving via learning from experience, 2025

    Jiangjie Chen, Wenxiang Chen, Jiacheng Du, Jinyi Hu, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Wenlei Shi, Zhihong Wang, Mingxuan Wang, Chenrui Wei, Shufa Wei, Huajian Xin, Fan Yang, Weihao Gao, Zheng Yuan, Tianyang Zhan, Zeyu Zheng, Tianxi Zhou, and Thomas Hanwen Zhu. Seed-prover 1.5: Mastering undergraduate-level theorem proving vi...

    work page 2025

  33. [33]

    Geoqa: A geometric question answering benchmark towards multimodal numerical reasoning.ACL Findings, 2021

    Jiaqi Chen, Jianheng Tang, Jinghui Qin, Xiaodan Liang, Lingbo Liu, Eric P Xing, and Liang Lin. Geoqa: A geometric question answering benchmark towards multimodal numerical reasoning.ACL Findings, 2021

    work page 2021

  34. [34]

    Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

    Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, Cheng Ren, Jiawei Shen, Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang, Zhihong Wang, Chenrui Wei, Shufa Wei, Yonghui Wu, Yuchen Wu, Yihang Xia, Huajian Xin, Fan Yang, Huaiyuan Ying, Hongyi Yuan, Zheng Yuan, Tianyang Zha...

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  35. [35]

    Evaluating Large Language Models Trained on Code

    Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, et al. Evaluating large language models trained on code.arXiv preprint arXiv:2107.03374, 2021

    work page internal anchor Pith review Pith/arXiv arXiv 2021

  36. [36]

    Program of thoughts prompting: Disentangling computation from reasoning for numerical reasoning tasks.TMLR, 2023

    Wenhu Chen, Xueguang Ma, Xinyi Wang, and William W Cohen. Program of thoughts prompting: Disentangling computation from reasoning for numerical reasoning tasks.TMLR, 2023. 23

    work page 2023

  37. [37]

    Teaching large language models to self-debug

    Xinyun Chen, Maxwell Lin, Nathanael Schärli, and Denny Zhou. Teaching large language models to self-debug. InThe Twelfth International Conference on Learning Representations, 2024

    work page 2024

  38. [38]

    Gold-medalist performance in solving olympiad geometry with alphageometry2.arXiv preprint arXiv:2502.03544, 2025

    Yuri Chervonyi, Trieu H Trinh, Miroslav Olšák, Xiaomeng Yang, Hoang Nguyen, Marcelo Menegali, Junehyuk Jung, Vikas Verma, Quoc V Le, and Thang Luong. Gold-medalist performance in solving olympiad geometry with alphageometry2.arXiv preprint arXiv:2502.03544, 2025

    work page arXiv 2025

  39. [39]

    An introduction to wu’s method for mechanical theorem proving in geometry

    Shang-Ching Chou. An introduction to wu’s method for mechanical theorem proving in geometry. Journal of Automated Reasoning, 4(3):237–267, 1988

    work page 1988

  40. [40]

    Automated production of traditional proofs for theorems in euclidean geometry

    Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang. Automated production of traditional proofs for theorems in euclidean geometry. InProceedings of Eigth IEEE Symposium on Login in Computer Science, pp. 48–56, 1993

    work page 1993

  41. [41]

    A deductive database approach to automated geometry theorem proving and discovering.Journal of Automated Reasoning, 25(3):219–246, 2000

    Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang. A deductive database approach to automated geometry theorem proving and discovering.Journal of Automated Reasoning, 25(3):219–246, 2000

    work page 2000

  42. [42]

    Think you have solved question answering? try arc, the ai2 reasoning challenge.arXiv preprint, 2018

    Peter Clark, Isaac Cowhey, Oren Etzioni, Tushar Khot, Ashish Sabharwal, Carissa Schoenick, and Oyvind Tafjord. Think you have solved question answering? try arc, the ai2 reasoning challenge.arXiv preprint, 2018

    work page 2018

  43. [43]

    Training verifiers to solve math word problems.arXiv preprint, 2021

    Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. Training verifiers to solve math word problems.arXiv preprint, 2021

    work page 2021

  44. [44]

    The smt-libv2 language and tools: A tutorial.Language c, pp

    David R Cok et al. The smt-libv2 language and tools: A tutorial.Language c, pp. 2010–2011, 2011

    work page 2010

  45. [45]

    Building machines that learn and think with people.Nature Human Behaviour, 2024

    Katherine Collins, Ilia Sucholutsky, Bhatt Umang, et al. Building machines that learn and think with people.Nature Human Behaviour, 2024

    work page 2024

  46. [46]

    Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilities

    Gheorghe Comanici, Eric Bieber, Mike Schaekermann, Ice Pasupat, Noveen Sachdeva, Inderjit Dhillon, Marcel Blistein, Ori Ram, Dan Zhang, Evan Rosen, et al. Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities.arXiv preprint arXiv:2507.06261, 2025

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  47. [47]

    Hammer for coq: Automation for dependent type theory.Journal of automated reasoning, 61(1):423–453, 2018

    Łukasz Czajka and Cezary Kaliszyk. Hammer for coq: Automation for dependent type theory.Journal of automated reasoning, 61(1):423–453, 2018

    work page 2018

  48. [48]

    Mathematics, word problems, common sense, and artificial intelligence

    Ernest Davis. Mathematics, word problems, common sense, and artificial intelligence.Arxiv preprint 2301.09723, 2023

    work page internal anchor Pith review Pith/arXiv arXiv 2023

  49. [49]

    Z3: An efficient smt solver

    Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008

    work page 2008

  50. [50]

    The lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction–CADE 28, pp. 625–635. Springer, 2021

    work page 2021

  51. [51]

    The lean theorem prover (system description)

    Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). InInternational Conference on Automated Deduction, pp. 378–388. Springer, 2015

    work page 2015

  52. [52]

    Ai achieves silver-medal standard solving international mathematical olympiad problems

    DeepMind. Ai achieves silver-medal standard solving international mathematical olympiad problems. https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/, 2024

    work page 2024

  53. [53]

    Gemini 3 system card

    Deepmind. Gemini 3 system card. Deepmind Technical Report, 2025

    work page 2025

  54. [54]

    Formal Conjectures: A collection of formalized statements of conjectures in Lean

    Deepmind. Formal Conjectures: A collection of formalized statements of conjectures in Lean. https: //github.com/google-deepmind/formal-conjectures, 2026. Accessed: 2026-01-22

    work page 2026

  55. [56]

    DeepSeek-V3 Technical Report

    DeepSeek-AI. Deepseek-v3 technical report.arXiv preprint arXiv:2412.19437, 2024. 24

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  56. [57]

    DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning

    DeepSeek-AI. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning.arXiv preprint arXiv:2501.12948, 2025

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  57. [58]

    Metacognitive Capabilities of LLMs: An Exploration in Mathematical Problem Solving

    Aniket Didolkar, Anirudh Goyal, Nan Rosemary Ke, Siyuan Guo, Michal Valko, Timothy Lillicrap, Danilo Rezende, Yoshua Bengio, Michael C Mozer, and Sanjeev Arora. Metacognitive capabilities of llms: An exploration in mathematical problem solving.arXiv preprint arXiv:2405.12205, 2024

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  58. [59]

    Everything of thoughts: Defying the law of penrose triangle for thought generation.arXiv preprint, 2024

    Ruomeng Ding, Chaoyun Zhang, Lu Wang, Yong Xu, Minghua Ma, Wei Zhang, Si Qin, Saravan Rajmohan, Qingwei Lin, and Dongmei Zhang. Everything of thoughts: Defying the law of penrose triangle for thought generation.arXiv preprint, 2024

    work page 2024

  59. [60]

    Darpa mathematical challenges, 2007

    DoD. Darpa mathematical challenges, 2007

    work page 2007

  60. [61]

    STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving

    Kefan Dong and Tengyu Ma. Stp: Self-play llm theorem provers with iterative conjecturing and proving.arXiv preprint arXiv:2502.00212, 2025

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  61. [62]

    Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically

    Kefan Dong, Adarsh Mahankali, and Tengyu Ma. Formal theorem proving by rewarding llms to decompose proofs hierarchically.arXiv preprint arXiv:2411.01829, 2024

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  62. [63]

    Gold-medal-level olympiad geometry solving with efficient heuristic auxiliary constructions.arXiv preprint arXiv:2512.00097, 2025

    Boyan Duan, Xiao Liang, Shuai Lu, Yaoxiang Wang, Yelong Shen, Kai-Wei Chang, Ying Nian Wu, Mao Yang, Weizhu Chen, and Yeyun Gong. Gold-medal-level olympiad geometry solving with efficient heuristic auxiliary constructions.arXiv preprint arXiv:2512.00097, 2025

    work page arXiv 2025

  63. [64]

    The Llama 3 Herd of Models

    Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang, Angela Fan, et al. The llama 3 herd of models.arXiv preprint arXiv:2407.21783, 2024

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  64. [65]

    Smtcoq: A plug-in for integrating smt solvers into coq

    Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark Barrett. Smtcoq: A plug-in for integrating smt solvers into coq. InInternational Conference on Computer Aided Verification, pp. 126–133. Springer, 2017

    work page 2017

  65. [66]

    Some unsolved problems.Michigan Mathematical Journal, 4(3):291–300, 1957

    Paul Erd˝ os. Some unsolved problems.Michigan Mathematical Journal, 4(3):291–300, 1957

    work page 1957

  66. [67]

    Graham.Old and New Problems and Results in Combinatorial Number Theory, volume 28 ofMonographies de L’Enseignement Mathématique

    Paul Erd˝ os and Ronald L. Graham.Old and New Problems and Results in Combinatorial Number Theory, volume 28 ofMonographies de L’Enseignement Mathématique. L’Enseignement Mathématique, 1999

    work page 1999

  67. [68]

    Semi-autonomous mathematics discovery with Gemini: A case study on the Erd˝ os problems.arXiv preprint arXiv:2601.22401, 2026

    Tony Feng, Trieu Trinh, Garrett Bingham, Jiwon Kang, Shengtong Zhang, Sang-hyun Kim, Kevin Bar- reto, Carl Schildkraut, Junehyuk Jung, Jaehyeon Seo, Carlo Pagano, Yuri Chervonyi, Dawsen Hwang, Kaiying Hou, Sergei Gukov, Cheng-Chiang Tsai, Hyunwoo Choi, Youngbeom Jin, Wei-Yuan Li, Hao-An Wu, Ruey-An Shiu, Yu-Sheng Shih, Quoc V Le, and Thang Luong. Semi-aut...

    work page arXiv 2026

  68. [69]

    Towards autonomous mathematics research.arXiv preprint arXiv:2602.10177, 2026

    Tony Feng, Trieu H. Trinh, Garrett Bingham, et al. Towards autonomous mathematics research.arXiv preprint, arXiv:2602.10177, 2026

    work page arXiv 2026

  69. [70]

    Baldur: Whole-Proof Generation and Repair with Large Language Models

    Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models.arXiv preprint arXiv:2303.04910, 2023

    work page internal anchor Pith review Pith/arXiv arXiv 2023

  70. [71]

    Extremal problems on set systems.Random Structures & Algorithms, 1995

    Peter Frankl and Vojtˇ ech Rödl. Extremal problems on set systems.Random Structures & Algorithms, 1995

    work page 1995

  71. [72]

    Mathematical capabilities of chatgpt

    Simon Frieder, Luca Pinchetti, Ryan-Rhys Griffiths, Tommaso Salvatori, Thomas Lukasiewicz, Philipp Christian Petersen, Alexis Chevalier, and Julius Berner. Mathematical capabilities of chatgpt. NeurIPS, 2023

    work page 2023

  72. [73]

    Complexity-based prompting for multi-step reasoning.ICLR, 2023

    Yao Fu, Hao Peng, Ashish Sabharwal, Peter Clark, and Tushar Khot. Complexity-based prompting for multi-step reasoning.ICLR, 2023

    work page 2023

  73. [74]

    Herald: A Natural Language Annotated Lean 4 Dataset

    Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated lean 4 dataset.arXiv preprint arXiv:2410.10878, 2024

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  74. [75]

    G-llava: Solving geometric problem with multi-modal large language model.ICLR, 2025

    Jiahui Gao, Renjie Pi, Jipeng Lin, Shizhe Xu, Yunsheng Zheng, and Tong Zhang. G-llava: Solving geometric problem with multi-modal large language model.ICLR, 2025. 25

    work page 2025

  75. [76]

    Pal: Program-aided language models.ICML, 2023

    Luyu Gao, Aman Madaan, Shuyan Zhou, Uri Alon, Pengfei Liu, Yiming Yang, Jamie Callan, and Graham Neubig. Pal: Program-aided language models.ICML, 2023

    work page 2023

  76. [77]

    Bertozzi

    Yurun Ge, Dominic Yang, and Andrea L. Bertozzi. Iterative active learning strategies for subgraph matching.Pattern Recognition, 158:110797, 2025. ISSN 0031-3203. doi: https://doi.org/10.1016/j.patcog. 2024.110797. URLhttps://www.sciencedirect.com/science/article/pii/S003132032400548X

    work page doi:10.1016/j.patcog 2025

  77. [78]

    Gemini: A Family of Highly Capable Multimodal Models

    Gemini Team, Rohan Anil, Sebastian Borgeaud, Yonghui Wu, Jean-Baptiste Alayrac, Jiahui Yu, Radu Soricut, Johan Schalkwyk, Andrew M Dai, Anja Hauth, et al. Gemini: A family of highly capable multimodal models.arXiv preprint arXiv:2312.11805, 2023

    work page internal anchor Pith review Pith/arXiv arXiv 2023

  78. [79]

    Mathematical exploration and discovery at scale

    Bogdan Georgiev, Javier Gómez-Serrano, Terence Tao, and Adam Zsolt Wagner. Mathematical explo- ration and discovery at scale.arXiv preprint arXiv:2511.02864, 2025

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  79. [80]

    FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI

    Elliot Glazer, Ege Erdil, Tamay Besiroglu, Diego Chicharro, Evan Chen, Alex Gunning, Caroline Falk- man Olsson, Jean-Stanislas Denain, Anson Ho, Emily de Oliveira Santos, et al. Frontiermath: A benchmark for evaluating advanced mathematical reasoning in ai.arXiv preprint arXiv:2411.04872, 2024

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  80. [81]

    Abel: Sample efficient online reinforcement learning for neural theorem proving.The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24, 2024

    Fabian Gloeckle, Jannis Limperg, Gabriel Synnaeve, and Amaury Hayat. Abel: Sample efficient online reinforcement learning for neural theorem proving.The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24, 2024

    work page 2024

Showing first 80 references.