Pith. sign in

REVIEW 2 major objections 6 minor 32 references

Mathematical reasoning and the computer

T0 review · 2 major / 6 minor · reviewed 2026-08-08 · deepseek-v4-flash

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

Pith's one-line read Machines can now find and check proofs, but cannot yet prove deep conjectures.

desk verdict A clear, honest survey of AI's current role in mathematics; the only real weakness is that it cites a contested success story without arbitrating, but the author's balance makes it a reliable overview. read the letter →

arxiv 2502.07850 v1 pith:DFZDVWZQ submitted 2025-02-11 cs.AI

Kevin Buzzard This is my paper · ORCID
classification cs.AI
keywords mathematicalreasoningneuralnetworksinteractivetheoremproversautomatedprovinglargelanguagemodelsproofformalisationdiscoverycomputersinmathematics
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

Computers have long been used to compute, but this survey argues that they are now starting to engage with the concept of proof. Neural networks have helped human mathematicians discover new theorems and counterexamples, interactive theorem provers have formalised recent research-level results, and large language models can currently do credible mathematics only at school level. The author's central claim is that machines are not yet close to independently proving deep conjectures, and that this remains science fiction. The survey matters because it maps the actual boundary of machine participation in pure mathematics and identifies near-term changes in how mathematicians work and learn.

What carries the argument

The organising device is a three-way taxonomy of computer systems for mathematics: neural networks that learn functions from data tables, automated and interactive theorem provers that manipulate formal proof objects, and large language models that generate token sequences. The taxonomy carries the argument by assigning each system a distinct role, and the paper's key structural claim is that a future 'AI mathematician' faces a single-player game with all-or-nothing scoring and an infinite, high-dimensional action space, which is what separates machine mathematics from machine chess.

What would settle it

Re-run the knot-signature prediction task from the paper's first case study using logistic regression or another standard statistical method on the same invariant table; if that method recovers the same relationship, the claim that a neural network was essential to the discovery is falsified. Separately, if a current large language model produces a formally verified proof of a genuinely new research-level lemma that is absent from its training data, the claim that such models only do school-level mathematics is falsified.

Watch

Extended reading notes

Core claim

The paper's central claim is that three kinds of computer system now participate in mathematical reasoning in distinctly different ways. Neural networks trained on tables of invariants can spot hidden relationships, and in the paper's two flagship case studies they helped mathematicians reach a new theorem about knot signatures and a new decomposition concept in representation theory that led to a checked conjecture. Interactive and automated theorem provers turn proofs into formal objects that computers can verify, and recent projects show that modern research mathematics, including advanced objects such as perfectoid spaces and condensed abelian groups, can be formalised in months rather than years. Large language models, by contrast, produce confident but often false arguments once the mathematics departs from well-trodden school examples, so their mathematical output is not yet trustworthy for research. The paper ends with the structural reason this is hard: proof is a single-player game with no useful score for partial progress and an infinite branching space of available steps, which makes the methods that mastered two-player games difficult to apply.

Load-bearing premise

The survey's case that neural networks have genuinely helped mathematicians hinges on the assumption that deep learning was essential to those discoveries; if the published rebuttal is right that ordinary statistical analysis would have sufficed, the strongest evidence for machine-assisted discovery loses its force.

Editorial extensions

If this is right

  • If neural networks keep producing checks that turn into theorems, machine learning will become a standard conjecturing tool in data-rich areas of mathematics.
  • If interactive theorem provers can formalise new papers within months, formalisation will become part of the normal publication workflow in some fields, and formalisation will occasionally simplify proofs by exposing unneeded dependencies.
  • If large language models remain at school level, their near-term research use will be as components of formal proof systems, not as autonomous mathematicians.
  • Reaching a gold-medal performance at the International Mathematical Olympiad is a plausible near-term milestone, but it would not by itself signal research-level theorem-proving ability.
  • Mathematics teaching will gradually include formal proof languages, alongside programming, for undergraduates who want to work at the new interface.

Reading between the lines

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

  • A reader should not feel obliged to accept the survey's optimism about neural networks: the paper itself cites a published critique arguing that ordinary statistical analysis could have produced the knot-theory discovery, which would reduce that success to a standard experimental-mathematics result.
  • A natural next experiment is to combine a large language model that proposes proof steps with an interactive theorem prover that rejects or accepts them; the survey's examples of 'hammer' and 'polyrith' tactics show the components for such a loop already exist.
  • The single-player-game framing implies that designing a useful partial-credit metric for incomplete proofs is a high-leverage open problem, because it would unlock reinforcement-learning methods for mathematics.
  • The paper's claim that real-time formalisation is becoming reality is concentrated in combinatorics and algebra; testing it in picture-heavy geometry would reveal whether the bottleneck is general or field-specific.
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

2 major / 6 minor

Summary. This survey by Kevin Buzzard gives an overview of recent uses of computers in mathematics, organized around three topics: neural networks as discovery tools, interactive and automated theorem provers, and large language models. It argues that while computation has long supported mathematics, computers are now beginning to engage with the concept of proof: neural networks have helped discover theorems and counterexamples, interactive theorem provers can formalize modern research-level mathematics, and large language models currently produce correct mathematics only at school level. The paper is explicitly aimed at mathematicians and assumes no background in machine learning or formal verification. It is framed as an update to Hales's 2014 survey and includes historical context, concrete examples, and citations to primary sources.

Significance. This is a readable, well-organized survey that fills a real niche: it explains current AI-related developments in mathematics to a mathematical audience without assuming computer science background. Its strengths include concrete and checkable examples, explicit citation of primary sources, inclusion of a dissenting viewpoint (Davis's rebuttal), and a appropriately cautious statement that machines independently proving deep conjectures is, as of now, science fiction. The paper makes no novel technical claims and does not ship code or machine-checked proofs, so its value lies in synthesis and accessibility. The two major concerns below do not undermine the survey's overall usefulness, but they do affect the accuracy of its central summary claims and need to be addressed.

major comments (2)
  1. [Section 2.2 / Section 5] The survey's flagship evidence for the claim that neural networks have helped human mathematicians discover new theorems is the Davies-Juhasz-Lackenby-Tomasev knot theorem. The text cites Ernest Davis's rebuttal [Dav21] but does not summarize or engage with its technical argument, and the summary in Section 5 repeats the example as an unqualified success. Since Davis argues that a conventional statistical analysis of the same invariant table could plausibly have surfaced the same relationship, the reader cannot determine whether the deep-learning component was essential to the discovery. The theorem itself is not in question, but the attribution is. Please either present Davis's objection and explain why the example still supports the survey's claim, or qualify the summary language (for example, 'neural networks have been used in the discovery process') to match the evidence.
  2. [Section 4 / Section 5] The assessment that current AI systems are 'at the level of a strong schoolchild or average 1st year undergraduate' and that an IMO gold medal is 'surely still at least a few years away' is difficult to reconcile with the paper's own mention of olympiad-level theorem proving, and it is already dated relative to the paper's February 2025 submission. The paper does not mention AlphaGeometry or AlphaProof, which in 2024 achieved silver-medal-level performance at the IMO and solved olympiad geometry problems. Even if one treats these systems as outside the narrow category of 'large language models,' they fall within the paper's stated scope of recent developments in neural networks, computer theorem provers, and large language models. Please update Section 4 and the summary to include or explicitly exclude these systems, and state the 'as of' date for the capabilities being surveyed.
minor comments (6)
  1. [Section 2.1] The claim that Yang's team achieved a success rate of well over 90% at rank prediction when taking modular form coefficients as input should be accompanied by a specific citation; the surrounding text cites [ABH19] and [He21], but not the particular claim.
  2. [Section 2.4] The section title says 'Searching for counterexamples in graph theory with neural networks,' but the opening sentence says the method is reinforcement learning 'moving away from deep learning'; please clarify whether Wagner's system used a neural network function approximator or whether reinforcement learning alone is meant.
  3. [Section 3.2] The phrase 'the computer-assisted part of the calculation is verified as bug-free, according to the prover' is stronger than what is actually shown; it would be more precise to say that the proof term is accepted by the kernel's type checker.
  4. [Section 4] There is a typo in the name 'A bby Goldberg'; it should be 'Abby Goldberg.'
  5. [References] Some references are incomplete or lack access dates: [BM] does not list the authors in the entry, [Gad] has a truncated URL, and [Lac], [Mas], and [Wag] are unversioned web links.
  6. [Section 4] The statement that progress in large language models is 'exponentially fast' is attributed only to 'Computer scientists' without a citation; either provide a source or soften the claim.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the paper is a survey of external, machine-checked and published results; the contested DJLT example is an attribution dispute, not a circular derivation.

full rationale

This paper does not present a derivation chain in which a conclusion is built into its premises. It surveys three external literatures—neural-network-assisted discovery, theorem proving, and large language models—and attributes claims to cited work. The DJLT knot example is described as a collaboration where a neural network predicted signature, parameter analysis pointed to continuous invariants, and then human mathematicians proved the theorem; the survey explicitly cites Ernest Davis's rebuttal [Dav21] that a conventional statistical analysis might have sufficed. That is a real evidentiary disagreement about whether deep learning was essential, but it is not circularity: the survey's claim does not define the theorem into existence, fit a parameter and then call the fit a prediction, or rely on the author's own prior work. The formalization claims are supported by independent, machine-checked developments in Lean, Coq and Isabelle, which are external checks rather than self-citation. The summary statement about neural networks helping discover theorems is an interpretation of published literature with the relevant caveat disclosed; whether it is overstated is a correctness question, not a circularity finding. No load-bearing step reduces to its own input.

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

The paper contributes no new mathematics; its assumptions are external facts it repeats. There are no fitted parameters or invented entities because no derivation is performed.

assumptions (2)
  • domain assumption The cited theorems, formalization projects, and neural network results are accurately summarized.
    The survey's conclusions rest on faithful reporting of external results (e.g., DJLT22, BBD+22, Liquid Tensor Experiment). We cannot independently check each source.
  • domain assumption The informal assessment of LLM capabilities based on anecdotal examples (primes ending in 7, etc.) is representative of current systems.
    The paper claims LLMs currently only do school-level math based on a few ad-hoc tests. This may not reflect all possible prompts or future models.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Mathematical reasoning and the computer." pith.science (2026). https://pith.science/paper/DFZDVWZQ

@misc{pith2026250207850,
  author       = {Pith},
  title        = {Pith review of: Mathematical reasoning and the computer},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/DFZDVWZQ}},
  note         = {Machine review of arXiv:2502.07850}
}
read the original abstract

Computers have already changed the way that humans do mathematics: they enable us to compute efficiently. But will they soon be helping us to reason? And will they one day start reasoning themselves? We give an overview of recent developments in neural networks, computer theorem provers and large language models.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

32 extracted references · 30 canonical work pages

  1. [1]

    Laura Alessandretti, Andrea Baronchelli, and Yang-Hui He, Machine learning meets number theory: The data science of birch-swinnerton-dyer, 2019

    work page 2019

  2. [2]

    Theory 26 (2022), 1145--1191

    Charles Blundell, Lars Buesing, Alex Davies, Petar Veli c kovi\' c , and Geordie Williamson, Towards combinatorial invariance for K azhdan- L usztig polynomials , Represent. Theory 26 (2022), 1145--1191. 4510816

    work page 2022

  3. [3]

    Bloom, On a density conjecture about unit fractions, 2021

    Thomas F. Bloom, On a density conjecture about unit fractions, 2021

    work page 2021

  4. [4]

    Bloom and Bhavik Mehta, Unit fractions, https://b-mehta.github.io/unit-fractions/, Accessed: 24-04-2023

    Thomas F. Bloom and Bhavik Mehta, Unit fractions, https://b-mehta.github.io/unit-fractions/, Accessed: 24-04-2023

    work page 2023

  5. [5]

    Johan Commelin, Completion of the liquid tensor experiment, https://leanprover-community.github.io/blog/posts/lte-final/, Accessed: 24-04-2023

    work page 2023

  6. [6]

    Johan Commelin and Adam Topaz, Abstraction boundaries and spec driven development in pure mathematics, 2023

    work page 2023

  7. [7]

    Dahn, Robbins algebras are B oolean: a revision of M c C une's computer-generated solution of R obbins problem , J

    Bernd I. Dahn, Robbins algebras are B oolean: a revision of M c C une's computer-generated solution of R obbins problem , J. Algebra 208 (1998), no. 2, 526--532. 1655464

    work page 1998

  8. [8]

    2021) , https://arxiv.org/abs/2112.04324, 2021

    Ernest Davis, Deep learning and mathematical intuition: A review of ( D avies et al. 2021) , https://arxiv.org/abs/2112.04324, 2021

    arXiv 2021

Show all 32 references
  1. [9]

    Dahmen, Johannes H\" o lzl, and Robert Y

    Sander R. Dahmen, Johannes H\" o lzl, and Robert Y. Lewis, Formalizing the solution to the cap set problem, 10th I nternational C onference on I nteractive T heorem P roving, LIPIcs. Leibniz Int. Proc. Inform., vol. 141, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2019, p...

    2019

  2. [10]

    Alex Davies, András Juhász, Marc Lackenby, and Nenad Tomasev, The signature and cusp geometry of hyperbolic knots, 2022

    2022

  3. [11]

    Ellenberg and Dion Gijswijt, On large subsets of F^n_q with no three-term arithmetic progression , Ann

    Jordan S. Ellenberg and Dion Gijswijt, On large subsets of F^n_q with no three-term arithmetic progression , Ann. of Math. (2) 185 (2017), no. 1, 339--343. 3583358

    2017

  4. [12]

    Siddhartha Gadgil, Formalizing gardam's disproof of kaplansky's unit conjecture, https://siddhartha-gadgil.github.io/automating-mathematics/posts/formalizing-gardam-disproof-kaplansky-conjecture/, Accessed: 24-04-2023

    2023

  5. [13]

    Giles Gardam, A counterexample to the unit conjecture for group rings, Ann. of Math. (2) 194 (2021), no. 3, 967--979. 4334981

    2021

  6. [14]

    Hales, A proof of the K epler conjecture , Ann

    Thomas C. Hales, A proof of the K epler conjecture , Ann. of Math. (2) 162 (2005), no. 3, 1065--1185. 2179728

    2005

  7. [15]

    Notes Log., vol

    , Mathematics in the age of the T uring machine , Turing's legacy: developments from T uring's ideas in logic, Lect. Notes Log., vol. 42, Assoc. Symbol. Logic, La Jolla, CA, 2014, pp. 253--298. 3497663

    2014

  8. [16]

    2293, Springer, Cham, [2021] 2021

    Yang-Hui He, The C alabi- Y au landscape---from geometry, to physics, to machine learning , Lecture Notes in Mathematics, vol. 2293, Springer, Cham, [2021] 2021. 4301304

    2021

  9. [17]

    Marc Lackenby, Using machine learning to formulate mathematical conjectures, https://www.youtube.com/watch?v=0ekP5M7w3dQ, Accessed: 24-04-2023

    2023

  10. [18]

    Adrien Marie Legendre, Essai sur la theorie des nombres; par am legendre, membre de l'institut et de la legion d'honneur.., chez Courcier, imprimeur-libraire pour les mathematiques, quai des Augustins, 1808

  11. [19]

    Koyejo, S

    Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet, Hypertree proof search for neural theorem proving, Advances in Neural Information Processing Systems (S. Koyejo, S. Mohamed, A. Agarwal...

    2022

  12. [20]

    The LMFDB Collaboration , The L -functions and modular forms database , https://www.lmfdb.org, 2023, [Online; accessed 24 April 2023]

    2023

  13. [21]

    Allen Mann, A complete proof of the R obbins conjecture , http://math.colgate.edu/ amann/MA/robbins_complete.pdf, Accessed: 24-04-2023

    2023

  14. [22]

    Patrick Massot, Formal mathematics for mathematicians and mathematics students, https://www.youtube.com/watch?v=tp_h3vzkObo, Accessed: 24-04-2023

    2023

  15. [23]

    Patrick Massot, Floris van Doorn, and Oliver Nash, Formalising the h -principle and sphere eversion, 2022

    2022

  16. [24]

    Blackwood and sons, 1889

    John Napier, The construction of the wonderful canon of logarithms, W. Blackwood and sons, 1889

  17. [25]

    OpenAI, Chatgpt, https://chat.openai.com, Accessed: 24-04-2023

    2023

  18. [26]

    , Gpt-4 technical report, 2023

    2023

  19. [27]

    Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever, Formal mathematics statement curriculum learning, 2022

    2022

  20. [28]

    J. D. Phillips and David Stanovsk\' y , Bruck loops with abelian inner mapping groups, Comm. Algebra 40 (2012), no. 7, 2449--2454. 2948838

    2012

  21. [29]

    Peter Scholze, Liquid tensor experiment, Exp. Math. 31 (2022), no. 2, 349--354. 4458116

    2022

  22. [30]

    The Stacks Project Authors , Stacks Project , https://stacks.math.columbia.edu, 2018

    2018

  23. [31]

    Adam Wagner, Finding counterexamples to conjectures via reinforcement learning, https://www.youtube.com/watch?v=vMLVH6IEwlM, Accessed: 24-04-2023

    2023

  24. [32]

    Adam Zsolt Wagner, Constructions in combinatorics via neural networks, 2021

    2021

Pith tools

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