Pith. sign in

REVIEW 3 major objections 2 minor 8 cited by

An AI agent using LLMs and Lean verification autonomously solved 9 open Erdős problems and 44 OEIS conjectures at a few hundred dollars each.

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.3

2026-06-30 16:53 UTC pith:W6IWLF6E

load-bearing objection The paper claims an LLM+Lean agent solved 9 open Erdős problems and 44 OEIS conjectures but supplies no verifiable Lean artifacts or formal statements, so the results stay uncheckable. the 3 major comments →

arxiv 2605.22763 v2 pith:W6IWLF6E submitted 2026-05-21 cs.AI

Advancing Mathematics Research with AI-Driven Formal Proof Search

George Tsoukalas , Anton Kovsharov , Sergey Shirobokov , Anja Surina , Moritz Firsching , Gergely B\'erczi , Francisco J. R. Ruiz , Arun Suggala
show 13 more authors
Adam Zsolt Wagner Eric Wieser Lei Yu Aja Huang Mikl\'os Z. Horv\'ath Andrew Ferraiuolo Henryk Michalewski Edward Lockhart Codrut Grosu Thomas Hubert Matej Balog Pushmeet Kohli Swarat Chaudhuri
This is my paper
classification cs.AI
keywords formal proofsLean theorem proverErdős problemsOEIS conjecturesLLM agentsautomated theorem provingmathematical reasoning
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.

The paper tests whether large language models can generate correct formal proofs in Lean for problems that remain open in mathematics. It reports that one agent design succeeded on a measurable share of Erdős problems and OEIS conjectures while keeping per-problem costs low. A sympathetic reader would care because this supplies a concrete, verifiable method for turning LLM reasoning into published mathematical results rather than informal suggestions. The work also shows that a simpler alternating generation-and-verification loop reproduces some of the same successes, though at higher cost on difficult cases, and notes ongoing use in several active research areas.

Core claim

Our most capable agent autonomously resolved 9 of 353 open Erdős problems at the per-problem cost of a few hundred dollars, proved 44/492 OEIS conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research. A basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes but proved costlier on the hardest problems.

What carries the argument

The agent that alternates LLM-based proof generation with Lean-based verification to produce formally checked solutions.

Load-bearing premise

The Lean proofs generated by the agent are correct, constitute new solutions to problems that were genuinely open, and required no post-generation human rewriting.

What would settle it

An independent check that reveals an error in one of the claimed Lean proofs or shows that any solved problem had already been resolved by prior human work.

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

If this is right

  • Formal proof search can be applied directly to open problems in number theory and combinatorics.
  • The same agent designs can be used in algebraic geometry, graph theory, optimization, and quantum optics.
  • A basic alternating generation-and-verification loop is sufficient to match some successes of more complex agents.
  • Per-problem costs remain in the low hundreds of dollars even for the hardest cases that succeed.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the success rate holds across larger sets of open problems, the method could shift the boundary of what counts as tractable without new human ideas.
  • Teams working on similar problems could run the agent on their own lists of conjectures to test reproducibility.
  • The cost scaling observed here suggests that further improvements in LLM reliability would directly lower the expense of exploring additional open questions.

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

3 major / 2 minor

Summary. The paper evaluates AI agents that use LLMs to generate candidate proofs in Lean, interleaved with verification, on two collections of open problems: 353 Erdős problems and 492 OEIS conjectures. The central empirical claim is that the strongest agent autonomously solved 9 Erdős problems at a few hundred dollars each and proved 44 OEIS conjectures; a baseline agent is shown to replicate some successes at higher cost. The work also reports ongoing deployment in several mathematical domains.

Significance. If the reported Lean proofs can be independently verified as correct, faithful to the original statements, and novel, the results would provide concrete evidence that LLM-based formal proof search can resolve open problems at modest cost and would supply a reproducible benchmark for future agent designs. The choice of established, externally curated problem lists strengthens the evaluation relative to synthetic benchmarks.

major comments (3)
  1. [Abstract and §4.2] Abstract and §4.2 (Erdős results): the claim that 9 problems were autonomously resolved rests on success counts alone; no Lean theorem declarations, proof scripts, problem identifiers, or verification logs are supplied, so it is impossible to confirm that the formalizations match the original open statements or that the proofs are both correct and previously unknown.
  2. [§5] §5 (OEIS experiments): the report of 44 proved conjectures likewise provides only aggregate counts without the corresponding Lean statements or any description of how the natural-language OEIS entries were translated into formal declarations, leaving the novelty and correctness claims unverifiable.
  3. [§3.3] §3.3 (agent autonomy): the description of the 'autonomous' workflow does not specify the protocol for human involvement in problem formalization or post-generation editing; without this information the autonomy claim cannot be assessed against the weakest assumption identified in the evaluation.
minor comments (2)
  1. [§4.3] The cost figures ('a few hundred dollars') are stated without a per-problem breakdown of API calls, token usage, or Lean compilation time, which would aid reproducibility.
  2. [Tables 1 and 2] Table 1 and Table 2 lack column headers that explicitly indicate whether each entry reports a verified Lean theorem or an unverified LLM output.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the thoughtful and constructive report. The comments highlight important issues of verifiability and clarity that we will address through revisions to strengthen the manuscript.

read point-by-point responses

  1. Referee: [Abstract and §4.2] Abstract and §4.2 (Erdős results): the claim that 9 problems were autonomously resolved rests on success counts alone; no Lean theorem declarations, proof scripts, problem identifiers, or verification logs are supplied, so it is impossible to confirm that the formalizations match the original open statements or that the proofs are both correct and previously unknown.

    Authors: We agree that aggregate success counts alone are insufficient for independent verification. In the revised manuscript we will add an appendix (or supplementary archive) that includes, for each of the 9 Erdős problems: the original problem identifier, the precise Lean theorem declaration used, the generated proof script, and the Lean verification log. This will allow readers to confirm that the formal statements match the open problems and that the proofs are correct and previously unknown. revision: yes

  2. Referee: [§5] §5 (OEIS experiments): the report of 44 proved conjectures likewise provides only aggregate counts without the corresponding Lean statements or any description of how the natural-language OEIS entries were translated into formal declarations, leaving the novelty and correctness claims unverifiable.

    Authors: We accept that the current text lacks both the translation methodology and the concrete Lean artifacts. The revision will include (i) a concise description of the procedure used to translate OEIS natural-language conjectures into Lean declarations and (ii) an appendix or data release containing the 44 formal statements together with their proof scripts and verification results. revision: yes

  3. Referee: [§3.3] §3.3 (agent autonomy): the description of the 'autonomous' workflow does not specify the protocol for human involvement in problem formalization or post-generation editing; without this information the autonomy claim cannot be assessed against the weakest assumption identified in the evaluation.

    Authors: We will expand §3.3 with an explicit workflow diagram and textual description. Human involvement is restricted to the one-time formalization of the natural-language problem statement into a Lean declaration; once that declaration is provided, the agent runs completely autonomously, interleaving LLM generation with Lean verification and without any human post-editing of proofs. The revised text will state this boundary clearly. revision: yes

Circularity Check

0 steps flagged

Empirical counts against external open-problem lists exhibit no circularity

full rationale

The paper reports direct experimental outcomes: an AI agent resolved 9 of 353 pre-existing Erdős problems and proved 44 of 492 OEIS conjectures. These are counts of successes measured against independent, externally defined lists. No equations, fitted parameters, self-citations, or ansatzes are invoked to derive or redefine these counts; the claims remain falsifiable by external inspection of the Lean artifacts. This matches the default expectation that most papers are non-circular when results are empirical benchmarks rather than closed-form derivations.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The central claim rests on the external correctness of the Lean theorem prover and the pre-existing openness of the selected Erdős and OEIS problems; no free parameters, new axioms, or invented entities are introduced.

pith-pipeline@v0.9.1-grok · 5793 in / 951 out tokens · 31364 ms · 2026-06-30T16:53:43.174400+00:00 · methodology

0 comments
read the original abstract

Large language models (LLMs) increasingly excel at mathematical reasoning, but their unreliability limits their utility in mathematics research. A mitigation is using LLMs to generate formal proofs in languages like Lean. We perform the first large-scale evaluation of this method's ability to solve open problems. Our most capable agent autonomously resolved 9 of 353 open Erd\H{o}s problems at the per-problem cost of a few hundred dollars, proved 44/492 OEIS conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research. A basic agent alternating LLM-based generation with Lean-based verification replicated the Erd\H{o}s successes but proved costlier on the hardest problems. These findings demonstrate the power of AI-aided formal proof search and shed light on the agent designs that enable it.

Figures

Figures reproduced from arXiv: 2605.22763 by Adam Zsolt Wagner, Aja Huang, Andrew Ferraiuolo, Anja Surina, Anton Kovsharov, Arun Suggala, Codrut Grosu, Edward Lockhart, Eric Wieser, Francisco J. R. Ruiz, George Tsoukalas, Gergely B\'erczi, Henryk Michalewski, Lei Yu, Matej Balog, Mikl\'os Z. Horv\'ath, Moritz Firsching, Pushmeet Kohli, Sergey Shirobokov, Swarat Chaudhuri, Thomas Hubert.

Figure 1
Figure 1. Figure 1: Pseudocode for ’s main components. The main loop creates a pool of asynchronous sketchers and raters and awaits the creation of a full (sorry-free) proof. Each prover subagent samples a parent sketch from the population using the P-UCB strategy and creates a stateful conversation session with an LLM (Gemini 3.1 Pro) instance. In this conversation, it receives instructions to perform tool calls from the LLM… view at source ↗
Figure 4
Figure 4. Figure 4: Sketcher agent prompt (condensed). Elided text is represented by [...]. Text in braces denotes template variables populated at runtime. For example, {code} is replaced by the current Lean file. 5 [PITH_FULL_IMAGE:figures/full_fig_p023_4.png] view at source ↗
Figure 3
Figure 3. Figure 3: Rater agent prompt (condensed). Elided text is represented by [...]. Text in braces denotes template variables populated at runtime. For example, {player blocks} is replaced by the sketches to be compared. 4 [PITH_FULL_IMAGE:figures/full_fig_p024_3.png] view at source ↗
Figure 2
Figure 2. Figure 2: Rater agent prompt (condensed). Elided text is represented by [...]. Text in braces denotes template variables populated at runtime. For example, {player blocks} is replaced by the sketches to be compared. 3 [PITH_FULL_IMAGE:figures/full_fig_p025_2.png] view at source ↗

Review history (2 revisions) →

discussion (0)

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

Forward citations

Cited by 8 Pith papers

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

  1. LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization

    cs.AI 2026-06 unverdicted novelty 7.0

    LeanMarathon uses four contract-scoped agents on an evolving blueprint coordinated by a two-stage orchestrator to formalize seven theorems from Erdős problems in Lean, proving 258 lemmas with no sorry across three runs.

  2. LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

    cs.AI 2026-06 unverdicted novelty 7.0

    LEAP enables general-purpose LLMs to reach 100% solve rate on the 2025 Putnam and 70% on a new Lean-IMO-Bench by combining informal reasoning with iterative Lean interaction.

  3. Theoria: Rewrite-Acceptability Verification over Informal Reasoning States

    cs.AI 2026-07 unverdicted novelty 6.0

    Theoria rewrites solutions into auditable typed state transitions with justifications, certifying 105 of 185 HLE problems at 91.4% precision and outperforming holistic judges on adversarial poisoned proofs by catching...

  4. Code evolution for link prediction in complex networks

    cs.SI 2026-06 unverdicted novelty 6.0

    Code evolution produces link prediction algorithms with average AUC of 0.915 versus 0.783 for human-designed methods across 580 networks, with better scalability.

  5. Recursions for Mock Theta Functions

    math.NT 2026-06 unverdicted novelty 5.0

    Derives weighted recursions for coefficients of mock theta functions f and ω via holomorphic projection on vector-valued Rankin-Cohen brackets, exploiting vanishing cusp form spaces.

  6. Agentic Publication Protocol: An Attempt to Modernize Scientific Publication

    cs.DL 2026-06 unverdicted novelty 5.0

    Introduces the Agentic Publication Protocol (APP) as a repository-based standard for publishing papers together with reproducibility artifacts and agent instructions.

  7. Witness-split + window-cardinality refinement for $r_3(N)$: Architecture, empirical results, and a structural hard pocket

    cs.LO 2026-05 unverdicted novelty 5.0

    A witness-split and window-pruning SAT framework finds no 44-element 3-AP-free subset of [1,212] but leaves two resistant instances unsolved.

  8. Skills for the future software profession: beyond agentic AI!

    cs.SE 2026-06 unverdicted novelty 2.0

    Round-table discussions with researchers and practitioners indicate verification and validation skills will become central for software engineers in the agentic AI era.

Reference graph

Works this paper leans on

86 extracted references · 28 canonical work pages · cited by 8 Pith papers · 14 internal anchors

  1. [1]

    Aristotle: IMO-level Automated Theorem Proving

    TudorAchim, AlexBest, AlbertoBietti, KevinDer, MathïsFédérico, SergeiGukov, 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

  2. [2]

    Primitive sets and von mangoldt chains: Erdős problem #1196 and beyond, 2026

    BorisAlexeev,KevinBarreto,YanyangLi,JaredDukerLichtman,LiamPrice,JibranIqbal Shah, Quanyu Tang, and Terence Tao. Primitive sets and von mangoldt chains: Erdős problem #1196 and beyond, 2026

    2026

  3. [3]

    Alexeev, M

    Boris Alexeev, Moe Putterman, Mehtaab Sawhney, Mark Sellke, and Gregory Valiant. Short proofs in combinatorics and number theory.arXiv preprint arXiv:2603.29961, 2026

    work page arXiv 2026

  4. [4]

    Short proofs in combinatorics, probability and number theory II

    Boris Alexeev, Moe Putterman, Mehtaab Sawhney, Mark Sellke, and Gregory Valiant. Short proofs in combinatorics, probability and number theory ii.arXiv preprint arXiv:2604.06609, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  5. [5]

    Pantograph: A machine-to-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in lean 4, 2025

    LeniAniva,ChuyueSun,BrandoMiranda,ClarkBarrett,andSanmiKoyejo. Pantograph: A machine-to-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in lean 4, 2025

    2025

  6. [6]

    AXLE: Axiom lean engine, 2025

    Axiom. AXLE: Axiom lean engine, 2025. Accessed: 2025

    2025

  7. [7]

    A note on p-sets

    Stephan Baier. A note on p-sets. 2004

    2004

  8. [8]

    Erdosproblems.com

    Thomas Bloom. Erdosproblems.com. https://www.erdosproblems.com, 2026

    2026

  9. [9]

    Migliore, Rosa M

    Mats Boij, Juan C. Migliore, Rosa M. Miró-Roig, Uwe Nagel, and Fabrizio Zanello.On the Shape of a Pure O-Sequence, volume 218 ofMemoirs of the American Mathematical Society. American Mathematical Society, Providence, RI, 2012

    2012

  10. [10]

    J. A. Bondy and R. L. Hemminger. Graph reconstruction–a survey.Journal of Graph Theory, 1(3):227–268, 1977

    1977

  11. [11]

    The motivic class of the space of genus0maps to the flag variety.arXiv preprint arXiv:2601.07222, 2026

    Jim Bryan, Balázs Elek, Freddie Manners, George Salafatinos, and Ravi Vakil. The motivic class of the space of genus0maps to the flag variety.arXiv preprint arXiv:2601.07222, 2026

    work page arXiv 2026

  12. [12]

    S. A. Burr, P. Erdős, R. L. Graham, and W. Wen-Ching Li. Complete sequences of sets of integer powers.Acta Arithmetica, 77(2):133–138, 1996

    1996

  13. [13]

    Last-Iterate Convergence of Anchored Gradient Descent

    Yang Cai and Weiqiang Zheng. Last-iterate convergence of anchored gradient descent. arXiv preprint arXiv:2604.12235, 2026. 11 Advancing Mathematics Research with AI-Driven Formal Proof Search

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  14. [14]

    Efficient Bayesian inference for generalized Bradley–Terry models.Journal of Computational and Graphical Statistics, 21(1):174– 196, 2012

    François Caron and Arnaud Doucet. Efficient Bayesian inference for generalized Bradley–Terry models.Journal of Computational and Graphical Statistics, 21(1):174– 196, 2012

    2012

  15. [15]

    arXiv preprint arXiv:2512.17260 , year=

    Jiangjie Chen, Wenxiang Chen, Jiacheng Du, Jinyi Hu, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Wenlei Shi, et al. Seed-prover 1.5: Mastering undergraduate-level theorem proving via learning from experience.arXiv preprint arXiv:2512.17260, 2025

    work page arXiv 2025

  16. [16]

    Deepseek-v2: A strong, economical, and efficient mixture-of-experts language model, 2024

    DeepSeek-AI. Deepseek-v2: A strong, economical, and efficient mixture-of-experts language model, 2024

    2024

  17. [17]

    On Erd\H{o}s and S\'ark\"ozy's sequences with Property P

    Christian Elsholtz and Stefan Planitzer. On erdős and sárközy’s sequences with property p.arXiv preprint arXiv:1609.07935, 2016

    work page internal anchor Pith review Pith/arXiv arXiv 2016

  18. [18]

    On the divisibility properties of sequences of integers

    Paul Erdős and Alice Sárközi. On the divisibility properties of sequences of integers. Proceedings of The London Mathematical Society, pages 97–101, 1970

    1970

  19. [19]

    On conjectures of graffiti

    Siemion Fajtlowicz. On conjectures of graffiti. In J. Akiyama, Y. Egawa, and H. Enomoto, editors,Graph Theory and Applications, volume 38 ofAnnals of Discrete Mathematics, pages 113–118. Elsevier, 1988

    1988

  20. [20]

    Aletheia tackles firstproof au- tonomously,

    Tony Feng, Junehyuk Jung, Sang-hyun Kim, Carlo Pagano, Sergei Gukov, Chiang- Chiang Tsai, David Woodruff, Adel Javanmard, Aryan Mokhtari, Dawsen Hwang, et al. Aletheia tackles firstproof autonomously.arXiv preprint arXiv:2602.21201, 2026

    work page arXiv 2026

  21. [21]

    arXiv preprint arXiv:2602.10177 , year=

    Tony Feng, Trieu H. Trinh, Garrett Bingham, Dawsen Hwang, Yuri Chervonyi, Junehyuk Jung,JoonkyungLee,CarloPagano,SanghyunKim,FedericoPasqualotto,SergeiGukov, Jonathan N. Lee, Junsu Kim, Kaiying Hou, Golnaz Ghiasi, Yi Tay, YaGuang Li, Chenkai Kuang, Yuan Liu, Hanzhao Lin, Evan Zheran Liu, Nigamaa Nayakanti, Xiaomeng Yang, Heng-Tze Cheng, Demis Hassabis, Ko...

    work page arXiv 2026

  22. [22]

    A strict separation between two notions of quadratically structured functions

    Moritz Firsching and Bogdan Georgiev. A strict separation between two notions of quadratically structured functions. In preparation, 2026

    2026

  23. [23]

    Horváth, Yaël Dillies, Calle Sönne, Eric Wieser, Fred Zhang, Thomas Hubert, Blaise Agüera y Arcas, and Pushmeet Kohli

    Moritz Firsching, Paul Lezeau, Salvatore Mercuri, Miklós Z. Horváth, Yaël Dillies, Calle Sönne, Eric Wieser, Fred Zhang, Thomas Hubert, Blaise Agüera y Arcas, and Pushmeet Kohli. Formal conjectures: An open and evolving benchmark for verified discovery in mathematics, 2026

    2026

  24. [24]

    Safeverify.https://github.com/GasStationManager/Saf eVerify, 2025

    GasStationManager. Safeverify.https://github.com/GasStationManager/Saf eVerify, 2025. [Accessed: 2026-05-12]

    2025

  25. [25]

    Mathematical exploration and discovery at scale

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

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  26. [26]

    Gemini 3.1 deep think, 2026

    Google DeepMind. Gemini 3.1 deep think, 2026. Accessed: 2026-04-30

    2026

  27. [27]

    100 open problems

    Ben Green. 100 open problems. https://people.maths.ox.ac.uk/greenbj/papers/open- problems.pdf, 2024. 12 Advancing Mathematics Research with AI-Driven Formal Proof Search

    2024

  28. [28]

    Progress in Formalizing Sphere Packing in Dimension 8

    Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, and Maryna Viazovska. A milestone in formalization: The sphere packing problem in dimension 8.arXiv preprint arXiv:2604.23468, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  29. [29]

    Olympiad-level formal mathematical reasoning with reinforcement learning.Nature, pages 1–3, 2025

    Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z Horváth, Goran Žužić, Eric Wieser, Aja Huang, Julian Schrittwieser, Yannick Schroecker, Hussain Masoom, Ottavia Bertolli, Tom Zahavy, Amol Mandhane, Jessica Yung, Iuliya Beloshapka, Borja Ibarz, Vivek Veeriah, Lei Yu, Oliver Nash, Paul Lezeau, Salvatore Mercuri, Calle Sönne, Bhavik Mehta, Alex Davies, ...

    2025

  30. [30]

    Learning and planning in complex action spaces

    Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Mohammadamin Barekatain, Simon Schmitt, and David Silver. Learning and planning in complex action spaces. In International Conference on Machine Learning, 2021

    2021

  31. [31]

    software engineer

    Geoffrey Huntley. Ralph wiggum as a "software engineer".https://ghuntley.com /ralph, 2025. Blog post

    2025

  32. [32]

    Equality in Fill's spectral gap problem

    Vishesh Jain and Clayton Mizgerd. Equality in fill’s spectral gap problem.arXiv preprint arXiv:2604.03937, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  33. [33]

    Jang and E

    Uijeong Jang and Ernest K Ryu. Point convergence of nesterov’s accelerated gradient method: An ai-assisted proof.arXiv preprint arXiv:2510.23513, 2025

    work page arXiv 2025

  34. [34]

    Jiang, A

    Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs.arXiv preprint arXiv:2210.12283, 2022

    work page arXiv 2022

  35. [35]

    Thor: Wielding hammers to integrate language models and automated theorem provers.Advances in Neural Information Processing Systems, 35:8360–8373, 2022

    Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers.Advances in Neural Information Processing Systems, 35:8360–8373, 2022

    2022

  36. [36]

    Paul J. Kelly. A congruence theorem for trees.Pacific Journal of Mathematics, 7(1):961– 968, 1957

    1957

  37. [37]

    John R. Koza. Genetic programming as a means for programming computers by natural selection.Statistics and Computing, 4(2):87–112, 1994

    1994

  38. [38]

    A Tensor-Algebraic No-Go Theorem for High-Dimensional Photonic GHZ States

    Mario Krenn, Moritz Firsching, George Tsoukalas, Rishikesh Gajjala, Xuemei Gu, and Swarat Chaudhuri. A Tensor-Algebraic No-Go Theorem for High-Dimensional Photonic GHZ States. In preparation, 2026

    2026

  39. [39]

    Quantum experiments and graphs: Multiparty states as coherent superpositions of perfect matchings.Physical Review Letters, 119(24), December 2017

    Mario Krenn, Xuemei Gu, and Anton Zeilinger. Quantum experiments and graphs: Multiparty states as coherent superpositions of perfect matchings.Physical Review Letters, 119(24), December 2017. 13 Advancing Mathematics Research with AI-Driven Formal Proof Search

    2017

  40. [40]

    Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction

    Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, et al. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction.arXiv preprint arXiv:2508.03613, 2025

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  41. [41]

    Luce.Individual Choice Behavior: A Theoretical Analysis

    R.D. Luce.Individual Choice Behavior: A Theoretical Analysis. Wiley, 1959

    1959

  42. [42]

    Gauss: An agent for autoformalization, 2026

    Math Inc. Gauss: An agent for autoformalization, 2026. Accessed: 2026

    2026

  43. [43]

    Thelean4theoremproverandprogramming language

    LeonardodeMouraandSebastianUllrich. Thelean4theoremproverandprogramming language. InInternational Conference on Automated Deduction, pages 625–635. Springer, 2021

    2021

  44. [44]

    Reinforced generation of com- binatorial structures: Hardness of approximation, 2026

    Ansh Nagda, Prabhakar Raghavan, and Abhradeep Thakurta. Reinforced generation of combinatorial structures: Hardness of approximation.arXiv preprint arXiv:2509.18057, 2025

    work page arXiv 2025

  45. [45]

    Reinforced Generation of Combinatorial Structures: Ramsey Numbers

    Ansh Nagda, Prabhakar Raghavan, and Abhradeep Thakurta. Reinforced generation of combinatorial structures: Ramsey numbers.arXiv preprint arXiv:2603.09172, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  46. [46]

    Alexander Novikov, Ngân V˜u, Marvin Eisenberger, Emilien Dupont, Po-Sen Huang, Adam Zsolt Wagner, Sergey Shirobokov, Borislav Kozlovskii, Francisco J. R. Ruiz, Abbas Mehrabian, M. Pawan Kumar, Abigail See, Swarat Chaudhuri, George Holland, Alex Davies, Sebastian Nowozin, Pushmeet Kohli, and Matej Balog. Alphaevolve: A coding agent for scientific and algor...

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  47. [47]

    R. L. Plackett. The analysis of permutations.Journal of the Royal Statistical Society. Series C (Applied Statistics), 24(2):193–202, 1975

    1975

  48. [48]

    Generative Language Modeling for Automated Theorem Proving

    StanislasPoluandIlyaSutskever. Generativelanguagemodelingforautomatedtheorem proving.arXiv preprint arXiv:2009.03393, 2020

    work page internal anchor Pith review Pith/arXiv arXiv 2009

  49. [49]

    On infinite sets with no3on a line.arXiv preprint arXiv:2602.21275, 2026

    Moe Putterman, Mehtaab Sawhney, and Gregory Valiant. On infinite sets with no3on a line.arXiv preprint arXiv:2602.21275, 2026

    work page arXiv 2026

  50. [50]

    Colouring versus density in integers and hales–jewett cubes.Journal of the London Mathematical Society, 110(5):e12987, 2024

    Christian Reiher, Vojtěch Rödl, and Marcelo Sales. Colouring versus density in integers and hales–jewett cubes.Journal of the London Mathematical Society, 110(5):e12987, 2024

    2024

  51. [51]

    Pawan Kumar, Emilien Dupont, Francisco J

    Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi. Mathematical discoveries from program search with large language models.Nature, 625(7995):468– 475, 2024

    2024

  52. [52]

    Ryu, Kun Yuan, and Wotao Yin

    Ernest K. Ryu, Kun Yuan, and Wotao Yin. Ode analysis of stochastic gradient methods with optimism and anchoring for minimax problems.arXiv preprint arXiv:1905.10899, 2019. 14 Advancing Mathematics Research with AI-Driven Formal Proof Search

    work page arXiv 1905

  53. [53]

    Extremal descendant integrals on moduli spaces of curves: An inequality dis- covered and proved in collaboration with ai, 2025

    Johannes Schmitt. Extremal descendant integrals on moduli spaces of curves: An inequality discovered and proved in collaboration with ai.arXiv preprint arXiv:2512.14575, 2025

    work page arXiv 2025

  54. [54]

    On a problem of erdős and sárközy.Journal of Combinatorial Theory, Series A, 94(1):191–195, 2001

    Tomasz Schoen. On a problem of erdős and sárközy.Journal of Combinatorial Theory, Series A, 94(1):191–195, 2001

    2001

  55. [55]

    A general reinforcement learning algorithm that masters chess, shogi, and go through self-play, 2018

    David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al. A general reinforcement learning algorithm that masters chess, shogi, and go through self-play, 2018

    2018

  56. [56]

    Neil J. Sloane. The on-line encyclopedia of integer sequences. InProceedings of the 14th Symposium on Towards Mechanized Mathematical Assistants: 6th International Conference, Calculemus ’07 / MKM ’07, page 130, Berlin, Heidelberg, 2007. Springer- Verlag

    2007

  57. [57]

    Richard P. Stanley. Hilbert functions of graded algebras.Advances in Mathematics, 28(1):57–83, 1978

    1978

  58. [58]

    An Improved Last-Iterate Convergence Rate for Anchored Gradient Descent Ascent

    Anja Surina, Arun Suggala, George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Francisco JR Ruiz, Pushmeet Kohli, and Swarat Chaudhuri. An improved last-iterate convergencerateforanchoredgradientdescentascent.arXivpreprintarXiv:2604.03782, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  59. [59]

    Ai contributions to Erdős problems.https://github .com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-p roblems, 2026

    Terence Tao and contributors. Ai contributions to Erdős problems.https://github .com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-p roblems, 2026. Accessed: 2026-04-23

    2026

  60. [60]

    The Lean Mathematical Library

    The Mathlib Community. The Lean Mathematical Library. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, 2020. ACM

    2020

  61. [61]

    Stanislaw M. Ulam. A collection of mathematical problems.New York and London: Interscience Publishers, 1960

    1960

  62. [62]

    Ulam.A Collection of Mathematical Problems, volume 8 ofInterscience Tracts in Pure and Applied Mathematics

    Stanislaw M. Ulam.A Collection of Mathematical Problems, volume 8 ofInterscience Tracts in Pure and Applied Mathematics. Interscience Publishers, New York, 1960

    1960

  63. [63]

    Hilbert : Recursively building formal proofs with informal reasoning

    Sumanth Varambally, Thomas Voice, Yanchao Sun, Zhifeng Chen, Rose Yu, and Ke Ye. Hilbert: Recursively building formal proofs with informal reasoning.arXiv preprint arXiv:2509.22819, 2025

    work page arXiv 2025

  64. [64]

    Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning

    Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning.arXiv preprint arXiv:2504.11354, 2025

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  65. [65]

    Woodruff et al

    David P Woodruff, Vincent Cohen-Addad, Lalit Jain, Jieming Mao, Song Zuo, Moham- madHossein Bateni, Simina Branzei, Michael P Brenner, Lin Chen, Ying Feng, et al. 15 Advancing Mathematics Research with AI-Driven Formal Proof Search Accelerating scientific research with gemini: Case studies and common techniques. arXiv preprint arXiv:2602.03837, 2026

    work page arXiv 2026

  66. [66]

    Formal mathematical reasoning: A new frontier in AI,

    Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in ai.arXiv preprint 2412.16075, 2024

    work page arXiv 2024

  67. [67]

    Leandojo: Theorem proving with retrieval-augmented language models.Advances in Neural Information Processing Systems, 36:21573–21612, 2023

    Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models.Advances in Neural Information Processing Systems, 36:21573–21612, 2023

    2023

  68. [68]

    Log-concavity of level Hilbert functions and pure o-sequences.Journal of Commutative Algebra, 16(2):245–256, 2024

    Fabrizio Zanello. Log-concavity of level Hilbert functions and pure o-sequences.Journal of Commutative Algebra, 16(2):245–256, 2024

    2024

  69. [69]

    Daniel Zheng, Ingrid von Glehn, Yori Zwols, Iuliya Beloshapka, Lars Buesing, Daniel M. Roy, Martin Wattenberg, Bogdan Georgiev, Tatiana Schmidt, Andrew Cowie, Fernanda Viegas, Dimitri Kanevsky, Vineet Kahlon, Hartmut Maennel, Sophia Alj, George Holland, Alex Davies, and Pushmeet Kohli. AI Co-Mathematician: Accelerating mathematicians with agentic AI.arXiv...

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  70. [70]

    Population Database and Matchmaking

    Database sampling:The controller selects a root proof sketch𝑆root by sampling from the database, along with𝑀= 2auxiliary inspiration sketches 𝑆insp. The selection strat- egy balances exploitation of high-rated sketches with exploration of diverse candidates (see “Population Database and Matchmaking”)

  71. [71]

    decompose unsolved goals,

    Prompt construction:A prompt X is assembled to guide the LLM. It integrates the formal problem specification, the Lean source code and natural language plan of𝑆root, and structured feedback derived from AlphaProof’s previous attempts on{𝑆insp}. As in AlphaEvolve, the controller encourages diversity by stochastically injecting instructions such as “decompo...

  72. [72]

    To scale to large Lean files, the subagent outputs mutations via asearch_replace tool in a compact diff format rather than rewriting the entire file

    Prover subagent:The assembled prompt X is dispatched to the LLM (Gemini 3.1 Pro), initiating a multi-turn episode. To scale to large Lean files, the subagent outputs mutations via asearch_replace tool in a compact diff format rather than rewriting the entire file. The subagent can also query AlphaProof to test specific subgoals mid- episode; the feedback ...

  73. [73]

    Global GoalCaching

    Validation:Once the candidate sketch𝑆′ passes the sandbox check, it undergoes formal validation. The system extracts all remainingsorry subgoals and cross-references them against a global goal cache using a deep hash of their exact Lean state (see “Global GoalCaching”). Ifa subgoal waspreviously resolved, theproof isretrieved immediately; otherwise, it is...

  74. [74]

    matches

    Database registration:The candidate 𝑆′, along with per-subgoal feedback from Al- phaProof, is registered in the database. Its fitness is then determined asynchronously via Elo matchmaking. AlphaProof has a Test-Time Reinforcement Learning (TTRL) mode in which it learns to solve a problem by solving its AI-generated variants at inference time; however, we ...

    2026

  75. [75]

    4𝑁1(𝑋) +𝑁 3(𝑋) ≤ 3|𝑋| + 2𝑁2(𝑋), which follows from writing𝑁𝑘(𝑥)= Í 𝑥∈ℤ 1𝑋 (𝑥) 1𝑋 (𝑥+ 𝑘) and a pointwise check of the indicator function1𝑋 across all4-point windows (𝑥, 𝑥+ 1, 𝑥+ 2, 𝑥+ 3); that is, summing the local inequality1𝑋 (𝑥) + 1𝑋 (𝑥+ 1) + 1𝑋 (𝑥+

  76. [76]

    + 1𝑋 (𝑥) 1𝑋 (𝑥+ 2) + 1𝑋 (𝑥+ 1)1𝑋 (𝑥+ 3) ≥ 1𝑋 (𝑥) 1𝑋 (𝑥+ 1) + 21𝑋 (𝑥+ 1)1𝑋 (𝑥+ 2) + 1𝑋 (𝑥+2)1 𝑋 (𝑥+3) +1 𝑋 (𝑥)1 𝑋 (𝑥+3)and then summing over all𝑥∈ℤ

  77. [77]

    Consider each pair(𝑥, 𝑥+ 2) ∈𝑋 2 and we proceed by cases on𝑥+ 1

    2𝑁2(𝑋) ≤𝑁 3(𝑋) + 2𝑉2(𝑋) + 2𝐼(𝑋) . Consider each pair(𝑥, 𝑥+ 2) ∈𝑋 2 and we proceed by cases on𝑥+ 1. Let 𝐺={𝑥∈𝑋|𝑥+ 1 ∉𝑋∧𝑥+ 2 ∈𝑋} . If 𝑥+ 1 ∈𝑋 , then the pair is counted exactly by𝑉2, so𝑁 2(𝑋)=𝑉 2(𝑋) + |𝐺|. If𝑥+1∉𝑋, then •If𝑥−1∈𝑋, then(𝑥−1, 𝑥+2)is a pair counted in𝑁 3(𝑋). •If𝑥+3∈𝑋, then(𝑥, 𝑥+3)is a pair counted in𝑁 3(𝑋). 41 Advancing Mathematics Research wit...

  78. [78]

    For any 𝛿∉{ 0,−𝑘} , the Sidon property ensures that there is at most one pair(𝑎, 𝑐) with 𝑎−𝑐=𝛿 and at most one pair(𝑑, 𝑏) with 𝑑−𝑏=𝛿+𝑘

    The cases𝛿= 0and 𝛿=−𝑘 each contribute≤ |𝐴| (one coordinate determines the rest). For any 𝛿∉{ 0,−𝑘} , the Sidon property ensures that there is at most one pair(𝑎, 𝑐) with 𝑎−𝑐=𝛿 and at most one pair(𝑑, 𝑏) with 𝑑−𝑏=𝛿+𝑘 . Consequently, each gap of size𝑘in𝐷identifies exactly one quadruple. Thus|quad 𝑘| ≤𝑁 𝑘(𝐷) +2𝑛

  79. [79]

    Combining these bounds shows that𝑁𝑘(𝐷) and 𝑁𝑘(𝑆) are related up to𝑂(𝑛) error

    Each "good" element 𝑠∈𝑆 with 𝑠+𝑘∈𝑆 (excluding ≤ 2𝑛 doubles of the form2𝑎) produces≥4quadruples, giving4𝑁 𝑘(𝑆) ≤ |quad 𝑘| +8𝑛. Combining these bounds shows that𝑁𝑘(𝐷) and 𝑁𝑘(𝑆) are related up to𝑂(𝑛) error. Apply- ing fact (2) to𝐷=𝐴−𝐴gives 4𝑁1(𝐷) +𝑁 3(𝐷) ≤3|𝐷| +2𝑁 2(𝐷) and then substitute the above two quadruple transfer bounds for𝑘= 1, 2, 3and collecting al...

    2002

  80. [80]

    Í 𝑅𝑛,𝑘 ≤2𝑛2 𝑛/2 =𝑜 2𝑛+1 𝑛6 . 44 Advancing Mathematics Research with AI-Driven Formal Proof Search Since all residual terms are bounded by𝑜 2𝑛+1 𝑛6 , we conclude that 𝑎𝑛 =𝑓 𝑛 +𝑜 2𝑛+1 𝑛6 = 2𝑛+1 𝑛 1+ 1 𝑛 + 3 𝑛2 + 13 𝑛3 + 75 𝑛4 + 541 𝑛5 +𝑜 1 𝑛5 This establishes the conjectured asymptotic expansion.□ Theorem.(A conjecture of OEIS A228143, 2018) Let𝑠𝑚 = Í𝑚 𝑘=0 ...

    2018

Showing first 80 references.