After math
Updates on my research and expository papers, discussion of open problems, and other maths-related topics. By Terence Tao
After Math
12 September, 2026 in guest blog, math.GM, opinion | Tags: Eamon Duede, philosophy, Silvia De Toffoli | by Terence Tao
This is a guest post by [Silvia De Toffoli and Eamon Duede. This blog post was initially written in a different file format and converted using AI. — T.]
Silvia De Toffoli (University School for Advanced Studies IUSS Pavia)
Eamon Duede (Princeton University and Purdue University)
On September 8th, 2026, OpenAI announced that it had produced an AI-generated solution to the Navier–Stokes existence and smoothness problem, one of the seven Millennium Prize Problems. The announcement kicked off debate over credit allocation and the respective contributions of humans and machines to the result. Moreover, the announcement intensified already circulating comparisons with earlier AI conquests in domains believed to otherwise exemplify human intellectual prowess. In a recent statement, Tristan Buckmaster, one of the mathematicians involved in the Navier–Stokes saga, wrote: “This is a Deep Blue–Kasparov moment.”
Existential questions for mathematics follow naturally: if AI can now provide answers to questions at the very frontier of mathematics, is the discipline on the verge of being “solved” as many have said of chess and Go? Like chess and Go players, should mathematicians just “keep playing” and rearrange their practices?
There is something right about the “keep playing” response. As philosopher C. Thi Nguyen (2019) has been insisting, the purpose of playing a game is not exhausted by its aim (winning). The real point is not only the outcome but the process. This is perhaps clearer with a party game such as Twister than with chess: the aim of playing Twister is certainly not winning. But something similar also applies to deep intellectual games, like chess and Go. For instance, playing a game of Go well can be an achievement in defeat.
But in the context of mathematical practice, this feels like an unnecessary retreat. Instead, we can make a stronger move: reject the characterization of mathematics as a game that makes the retreat seem necessary in the first place.
The question, then, is not simply what comes after math, once AI can answer its hardest questions. It is also what we are after when we do mathematics in the first place.
The narrative that AI has “solved” mathematics rests on two assumptions, both seductive and plausible, but both wrong:
- AI really did solve a problem in mathematics.
- Mathematics is only about solving problems.
The first assumption is wrong because to really solve a mathematical problem, providing a mere answer (even if formally certified) is not sufficient. What is missing is an intelligible proof that human mathematicians can understand and use to advance the aims of mathematics. And, as we will argue below, even if AI were to give us just that, the story would not be over because the second assumption is wrong. Mathematics is clearly a much broader enterprise than just problem solving. Mathematicians strive to develop new concepts and theories, to ask and answer new questions, to unify disparate areas, to educate and sustain scholarly communities, and to produce work that is valued for its beauty and depth.
We can (and should) therefore reject the narrative of AI defeating humans at mathematics and start thinking hard about what mathematics really is and what we want it to be.
Not All Answers Are Solutions
OpenAI produced an answer to the question of whether Navier–Stokes can develop a singularity: yes. In The Hitchhiker’s Guide to the Galaxy, Deep Thought produced an answer to life, the universe, and everything: 42. Neither is exactly what we wanted.
Of course, OpenAI gave us much more than “yes.” Deep Thought offered only a number, whereas OpenAI produced two artifacts that many are willing to call proofs. The first is a Lean formalization certifying validity. This was accompanied by a manuscript that appears to contain the corresponding informal proof. So, why is this still dissatisfying? The reason has to do with the underlying notion of proof itself.
There are, in fact, two notions of proof: a logical notion and an intelligible notion.
Modern logic characterizes proof in terms of deductive validity such that a proof can be checked by a mechanical procedure that does not itself require understanding of the mathematical argument. A Lean formalization meets these standards exactly and a Lean formalization of the Navier–Stokes result is therefore a genuine and important contribution: by meeting the demands of the logical notion of proof, it secures certainty.
But mathematicians also want something else from proof. They want understanding (Thurston 1994). They want to know what makes a proposition true. This kind of knowledge trades in mathematical ideas that they can grasp, communicate to other experts, connect with existing knowledge, and use to make further progress. This is the intelligible notion of proof. As of now, it is not clear that OpenAI’s result has given the mathematical community the kind of value that one expects from the intelligible notion of proof.
Genuine proofs are at the same time logical and intelligible proofs. Historically, the two notions have tended to run together. This is because no mathematician could produce an enormously complicated logical proof without first grasping some of the key shareable ideas that made the theorem true. The logical notion of proof was primarily used to verify the correctness of intelligible proofs (Burgess and De Toffoli 2022).
But with AI, these two notions can now come apart dramatically. We can end up with formal proofs that float free from any intelligible proof.
This is not a criticism of formal proof. The converse problem is at least as serious. An intelligible mathematical argument can convey a grand idea while failing to establish that the result is actually true. Jaffe and Quinn (1993) famously used Thurston’s geometrization theorem for Haken three-manifolds as an example: a major insight accompanied by insufficiently complete proofs could become a “roadblock rather than an inspiration.” And one motivation for Hales’s Flyspeck formalization project was to verify that the intelligible (but hard to check) proof presented for the Kepler conjecture was, indeed, a genuine proof (Hales et al. 2009).
Therefore, falling short of either the logical or intelligible notion creates roadblocks where genuine proofs clear the way for mathematical progress. A real mathematical solution requires both logical correctness and intelligibility.
This is particularly clear in the case of the seven Millennium Prize Problems. They were not selected because mathematicians merely wanted seven answers, but rather because they wanted fruitful solutions. The Clay Mathematics Institute itself explains why proof matters in the case of Navier–Stokes: “Because a proof gives not only certitude, but also understanding.”
What OpenAI has given us is an answer. But it is not clear that they have delivered a fruitful solution. Perhaps, we will find that they have, but at the moment, the situation is far from clear. A genuine solution will provide adequate grounds for believing the result but also an intelligible mathematical argument that allows the result to become part of mathematics as understood and practiced by mathematicians.
Nevertheless, if it turns out that what OpenAI has provided is a mere answer, this is not enough to dispel the existential threat that mathematics is facing. Future AI systems are likely to produce genuine proofs that are at once formally certified and fully intelligible to mathematicians. So, current concerns that mathematics is on the verge of being “solved” by AI are not fully dispelled by simply insisting on genuine solutions rather than mere answers.
You Need More than Solutions to “Solve Math”
If future AI systems will produce genuine proofs, logically correct and intelligible, like those produced by “master” mathematicians, it would still be incorrect to think that mathematics would have been “solved” as some say that chess or Go have been solved.
In chess and Go, we accept radically uneven competition between humans and machines because both are, in the relevant sense, playing the same game.
But mathematics is not (or at least not only) a game. To begin with, there is no winner. Mathematics is not an adversarial game with determinate conditions for victory. It is certainly true that mathematicians compete with one another for fame, prizes, jobs, and credit. Chess players do those things too. But chess players also win chess. There is no corresponding condition for winning mathematics. There is no mathematical checkmate.
In mathematics, it is more natural to treat AI as an assistant rather than as a competitor. As Jeremy Avigad (2026) puts it, “We should keep in mind that AI is nothing more than technology, designed to serve our purposes. It is misguided to think of mathematicians as competing with AI; when we drive a car, we aren’t competing to see who can go faster, and when we use a phone, we aren’t competing to see who can speak louder.”
But there is a deeper, and in many ways prior, problem with the competition framing. It requires accepting the assumption that solving problems is the activity by which mathematical success should be measured.
Genuine problem solving is certainly one of the principal aims of mathematics. It is not, however, its only aim. Mathematics is a body of knowledge engaged with, interpreted, and digested by a scholarly community and not a registry of results in the abstract. This simple point has even motivated an entire movement in the philosophy of mathematics: the philosophy of mathematical practice.
Terence Tao (2026) lists many goals of mathematics beyond problem solving. These include developing new theories and techniques, understanding the world, sustaining a community, training the next generation of mathematicians, contributing to cumulative knowledge, and creating works of aesthetic value. Of course, these have been positively correlated with genuine solutions.
But AI breaks that correlation, for the same reason it separates the two notions of proof. So, even genuine solutions would not satisfy us.
This is not moving the goalposts but recognizing that any specific goalpost is inadequate. If mathematics is a game, it is an infinite one.
This attitude is not reactionary. We reject both the concession that logically establishing a theorem is sufficient for a genuine proof and the reduction of “AI for mathematics” to proving theorems. Accepting this, we may find many opportunities for AI in mathematics to support human mathematical flourishing.
Aftermath
We do not deny that, if OpenAI’s announcement is correct, this is an extraordinary achievement. But we should get clear about what type of achievement it is. At this moment, it is an answer, not a solution. And, even if in time the result reveals itself as a genuine solution, we have argued that, in the practice of mathematics, solutions are not everything.
The urgency of rethinking what we value in mathematics is already being recognized within the mathematical community. In a recent declaration initially signed by 25 Fields Medallists, mathematicians warn of a “severe misalignment” between the goals of AI companies and those of the mathematical community.
Mathematicians need to do more to examine their norms. The priority norm is not the problem here (though it is likely a separate problem). The current failure to distinguish genuine solutions from answers, and the growing focus on problem-solving alone, are. This way of thinking is inspired by the current credit economy in mathematics and, as David Bessis recently discussed in his blog, the credit economy needs rethinking.
AI presents mathematics not with an ending but with a choice about what mathematical practice should become. If mathematical success comes to be identified too closely with the production of certified answers, mathematics risks adapting itself to precisely those features that are easiest to benchmark and automate away.
If, instead, mathematicians treat AI as a technology for advancing its long-standing and centrally human purposes, the technology may come to contribute to an accelerated flourishing and enrichment of the discipline. The important question is, therefore, not whether AI will defeat mathematicians, but which mathematical ends we want AI to serve.
What remains in the aftermath is not merely leftovers for humans to scramble for once machines have devoured all of the real problems. Rather, it is an opportunity to clarify what mathematics is all about. We should ask again what we are after when we do mathematics.
(An extended version of this text will appear elsewhere.)
Share this:
- [Print (Opens in new window)
Print](https://terrytao.wordpress.com/2026/09/12/after-math/#print?share=print) - Email a link to a friend (Opens in new window) Email
- More
-
- [Share on X (Opens in new window)
X](https://terrytao.wordpress.com/2026/09/12/after-math/?share=twitter)
- [Share on Facebook (Opens in new window)
Facebook](https://terrytao.wordpress.com/2026/09/12/after-math/?share=facebook)
- [Share on Reddit (Opens in new window)
Reddit](https://terrytao.wordpress.com/2026/09/12/after-math/?share=reddit)
- [Share on Pinterest (Opens in new window)
Pinterest](https://terrytao.wordpress.com/2026/09/12/after-math/?share=pinterest) -
Like Loading...
Recent Comments
Fabien Besnard on “Deep theorems were scar…
Anonymous on After Math
Jason Zhao on Crowdsourcing a list of genera…
mattecapu on Crowdsourcing a list of genera…
R Pi on A Severe Misalignment of AI in…
Anonymous on Happy, those able to know the…
Anonymous on “Deep theorems were scar…
Thái Võ on “Deep theorems were scar…
Anonymous on “Deep theorems were scar…
Anonymous on A Severe Misalignment of AI in…
Anonymous on On the Hodge conjecture
Anonymous on “Deep theorems were scar…
Anonymous on Happy, those able to know the…
Anonymous on Happy, those able to know the…
brianbeverly1 on “Deep theorems were scar…
Top Posts
- A Severe Misalignment of AI in Mathematics
- After Math
- "Deep theorems were scarce and difficult and so became an effective mechanism to identify deep thought. AI has broken this system."
- Wimbledon, the U.S. Open, and the future of mathematics
- The status of the Hodge conjecture
- Happy, those able to know the causes of things
- On the Hodge conjecture
- Finite time blowup with smooth forcing term for the incompressible porous medium, Boussinesq, and incompressible Euler equations
- Crowdsourcing a list of general resources on the purpose, value, and nature of mathematics
- On the existence of non-sofic groups
Archives
- September 2026 (13)
- August 2026 (6)
- July 2026 (9)
- June 2026 (3)
- May 2026 (1)
- March 2026 (4)
- February 2026 (3)
- January 2026 (4)
- December 2025 (5)
- November 2025 (5)
- September 2025 (1)
- August 2025 (3)
- July 2025 (1)
- June 2025 (2)
- May 2025 (5)
- April 2025 (2)
- March 2025 (1)
- February 2025 (3)
- January 2025 (1)
- December 2024 (3)
- November 2024 (4)
- October 2024 (1)
- September 2024 (4)
- August 2024 (3)
- July 2024 (3)
- June 2024 (1)
- May 2024 (1)
- April 2024 (5)
- March 2024 (1)
- December 2023 (2)
- November 2023 (2)
- October 2023 (1)
- September 2023 (3)
- August 2023 (3)
- June 2023 (8)
- May 2023 (1)
- April 2023 (1)
- March 2023 (2)
- February 2023 (1)
- January 2023 (2)
- December 2022 (3)
- November 2022 (3)
- October 2022 (3)
- September 2022 (1)
- July 2022 (3)
- June 2022 (1)
- May 2022 (2)
- April 2022 (2)
- March 2022 (5)
- February 2022 (3)
- January 2022 (1)
- December 2021 (2)
- November 2021 (2)
- October 2021 (1)
- September 2021 (2)
- August 2021 (1)
- July 2021 (3)
- June 2021 (1)
- May 2021 (2)
- February 2021 (6)
- January 2021 (2)
- December 2020 (4)
- November 2020 (2)
- October 2020 (4)
- September 2020 (5)
- August 2020 (2)
- July 2020 (2)
- June 2020 (1)
- May 2020 (2)
- April 2020 (3)
- March 2020 (9)
- February 2020 (1)
- January 2020 (3)
- December 2019 (4)
- November 2019 (2)
- September 2019 (2)
- August 2019 (3)
- July 2019 (2)
- June 2019 (4)
- May 2019 (6)
- April 2019 (4)
- March 2019 (2)
- February 2019 (5)
- January 2019 (1)
- December 2018 (6)
- November 2018 (2)
- October 2018 (2)
- September 2018 (5)
- August 2018 (3)
- July 2018 (3)
- June 2018 (1)
- May 2018 (4)
- April 2018 (4)
- March 2018 (5)
- February 2018 (4)
- January 2018 (5)
- December 2017 (5)
- November 2017 (3)
- October 2017 (4)
- September 2017 (4)
- August 2017 (5)
- July 2017 (5)
- June 2017 (1)
- May 2017 (3)
- April 2017 (2)
- March 2017 (3)
- February 2017 (1)
- January 2017 (2)
- December 2016 (2)
- November 2016 (2)
- October 2016 (5)
- September 2016 (4)
- August 2016 (4)
- July 2016 (1)
- June 2016 (3)
- May 2016 (5)
- April 2016 (2)
- March 2016 (6)
- February 2016 (2)
- January 2016 (1)
- December 2015 (4)
- November 2015 (6)
- October 2015 (5)
- September 2015 (5)
- August 2015 (4)
- July 2015 (7)
- June 2015 (1)
- May 2015 (5)
- April 2015 (4)
- March 2015 (3)
- February 2015 (4)
- January 2015 (4)
- December 2014 (6)
- November 2014 (5)
- October 2014 (4)
- September 2014 (3)
- August 2014 (4)
- July 2014 (5)
- June 2014 (5)
- May 2014 (5)
- April 2014 (2)
- March 2014 (4)
- February 2014 (5)
- January 2014 (4)
- December 2013 (4)
- November 2013 (5)
- October 2013 (4)
- September 2013 (5)
- August 2013 (1)
- July 2013 (7)
- June 2013 (12)
- May 2013 (4)
- April 2013 (2)
- March 2013 (2)
- February 2013 (6)
- January 2013 (1)
- December 2012 (4)
- November 2012 (7)
- October 2012 (6)
- September 2012 (4)
- August 2012 (3)
- July 2012 (4)
- June 2012 (3)
- May 2012 (3)
- April 2012 (4)
- March 2012 (5)
- February 2012 (5)
- January 2012 (4)
- December 2011 (8)
- November 2011 (8)
- October 2011 (7)
- September 2011 (6)
- August 2011 (8)
- July 2011 (9)
- June 2011 (8)
- May 2011 (11)
- April 2011 (3)
- March 2011 (10)
- February 2011 (3)
- January 2011 (5)
- December 2010 (5)
- November 2010 (6)
- October 2010 (9)
- September 2010 (9)
- August 2010 (3)
- July 2010 (4)
- June 2010 (8)
- May 2010 (8)
- April 2010 (8)
- March 2010 (8)
- February 2010 (10)
- January 2010 (12)
- December 2009 (11)
- November 2009 (8)
- October 2009 (15)
- September 2009 (6)
- August 2009 (13)
- July 2009 (10)
- June 2009 (11)
- May 2009 (9)
- April 2009 (11)
- March 2009 (14)
- February 2009 (13)
- January 2009 (18)
- December 2008 (8)
- November 2008 (9)
- October 2008 (10)
- September 2008 (5)
- August 2008 (6)
- July 2008 (7)
- June 2008 (8)
- May 2008 (11)
- April 2008 (12)
- March 2008 (12)
- February 2008 (13)
- January 2008 (17)
- December 2007 (10)
- November 2007 (9)
- October 2007 (9)
- September 2007 (7)
- August 2007 (9)
- July 2007 (9)
- June 2007 (6)
- May 2007 (10)
- April 2007 (11)
- March 2007 (9)
- February 2007 (4)
Categories
- expository (330)
- tricks (13)
- guest blog (19)
- Mathematics (936)
- math.AC (9)
- math.AG (45)
- math.AP (117)
- math.AT (17)
- math.CA (199)
- math.CO (207)
- math.CT (9)
- math.CV (40)
- math.DG (37)
- math.DS (90)
- math.FA (24)
- math.GM (20)
- math.GN (21)
- math.GR (92)
- math.GT (17)
- math.HO (14)
- math.IT (13)
- math.LO (54)
- math.MG (48)
- math.MP (32)
- math.NA (26)
- math.NT (214)
- math.OA (22)
- math.PR (114)
- math.QA (6)
- math.RA (49)
- math.RT (21)
- math.SG (4)
- math.SP (48)
- math.ST (11)
- non-technical (217)
- admin (49)
- advertising (85)
- diversions (7)
- media (15)
- journals (4)
- obituary (15)
- opinion (41)
- paper (273)
- book (23)
- Companion (13)
- update (26)
- question (128)
- polymath (87)
- talk (69)
- DLS (20)
- teaching (190)
- 245A – Real analysis (11)
- 245B – Real analysis (22)
- The sciences (1)
- travel (26)
###
additive combinatorics AI approximate groups arithmetic progressions Artificial Intelligence Ben Green Cauchy-Schwarz Cayley graphs central limit theorem Chowla conjecture compressed sensing correspondence principle distributions divisor function eigenvalues Elias Stein Emmanuel Breuillard entropy equidistribution Erdos ergodic theory Euler equations exponential sums finite fields Fourier transform Freiman's theorem Gowers uniformity norm Gowers uniformity norms graph theory Gromov's theorem GUE Hilbert's fifth problem ICM incompressible Euler equations inverse conjecture Joni Teravainen Kaisa Matomaki Kakeya conjecture Lie algebras Lie groups Liouville function Littlewood-Offord problem Maksym Radziwill Mobius function Navier-Stokes equations nilpotent groups nilsequences nonstandard analysis Paul Erdos politics polymath1 polymath8 Polymath15 polynomial method polynomials prime gaps prime numbers prime number theorem random matrices randomness Ratner's theorem regularity lemma Ricci flow Riemann zeta function Schrodinger equation Shannon entropy sieve theory structure Szemeredi's theorem Tamar Ziegler ultrafilters universality Van Vu wave maps Yitang Zhang
The Polymath Blog
- Polymath News and AI
- Polymath projects 2021
- A sort of Polymath on a famous MathOverflow problem
- Ten Years of Polymath
- Updates and Pictures
- Polymath proposal: finding simpler unit distance graphs of chromatic number 5
- A new polymath proposal (related to the Riemann Hypothesis) over Tao’s blog
- Spontaneous Polymath 14 – A success!
- Polymath 13 – a success!
- Non-transitive Dice over Gowers’s Blog
33 comments
Comments feed for this article
Anonymous
this is correct and somewhat more understood in arts (but perhaps it should indeed more correct to think of math as a form of art with a rather specific language)
As Bela Bartok said:
competitions are for horses, not for artists (nor for mathematicians)
Anonymous
“Mathematics is only about solving problems.”
If this is wrong, then why does achieving tenure heavily depend on mathematicians solving problems, and why are there so many prizes for solving problems, like the Millennium Prizes? There’s a significant mismatch between what mathematics is supposedly really about, and how mathematics academia structures the incentives to a successful mathematics career.
Anonymous
Historically since we are human solving a problem usually means you’ve discovered an intelligent path to the solution. This article successfully argues that AI has divorced these two concepts and therefore that problem-solving is not a useful benchmark.
Anonymous
İn practice, however, problem solving has always come first. This has been the nature: once a problem has been solved, people quickly lose interest and move on to work on others. (Also most people need to use the statement of a theorem, not the proof.)
Anonymous
This doesn’t ring true to me. It’s not like people move on to any old problem; rather once a technique has seen value in tackling one problem then there is hope in using it to tackle similar problems, or work on natural extensions, or build out some of the results into a wider theory etc.
E.g. people didn’t lose interest in Ricci flow once the Poincaré conjecture was solved, if anything interest in the area grew
Also your last statement (that “most” people only need the theorem and not the proof) is at best partially true in some areas; it is certainly false e.g. in most of analysis.
Anonymous
This is not exactly the case in practice: if you are working hard on an important problem, it is a very painful process and all you want is to find a solution (and be the first to do it); you would not care if the proof is beatiful or not. The novelty comes first in academia; “digestive” work is not valued so much).
Anonymous
The mere fact there are prizes for hard math problems doesn’t justify the argument of “mathematics is only about solving problems”. As Tao said, this is only one of the aims of the field.
Bhupinder Singh Anand
[quote] But mathematicians also want something else from proof. They want understanding (Thurston 1994). They want to know what makes a proposition true. This kind of knowledge trades in mathematical ideas that they can grasp, communicate to other experts, connect with existing knowledge, and use to make further progress. This is the intelligible notion of proof. As of now, it is not clear that OpenAI’s result has given the mathematical community the kind of value that one expects from the intelligible notion of proof. [unquote]
Yes indeed. Moreover:
I: Open AI’s result can claim to illuminate the ‘understanding’ mathematicians expects from a formal proof only if it also validates that the proof interprets as a ‘mathematical truth’ over some categorically communicable domain.
Reasons for the caveat? Three.
1. Understanding Why the Four Colour Theorem is True.
2. The Holy Grail of Mathematics Is Arithmetical Truth, Not Set-Theoretical Proof.
3. Understanding Why Fermat’s Last Theorem is True.
In other words, AI agents must (even if only in principle) be capable of:
(a) distinguishing between ‘reportedly true’ statements and ‘mathematically true’ statements;
(b) validating a Lean theorem as a ‘mathematical truth’ over some well-defined (essentially ‘constructible’) domain.
II: I would further argue that:
(i) if a mathematicians overriding responsibility is to ensure that any ‘proof’ proffered as definitive ‘knowledge’ by an AI formalises some intuitive, pre-formal human ‘truth’ that the AI — like any other formal mathematical language — was originally designed to express, and capture, formally as a ‘proof’;
(ii) then no AI will ever make mathematicians’ responsibility redundant.
Reason? There are mathematical ‘truths’ which an AI can ‘recognise’, but not ‘prove’; as admitted by ChatGPT in the dialogue reproduced in the preprint:
The Gödelian Turing Test: Both Copilot and ChatGPT ‘failed’ this Test
In other words:
- although an AI will undoubtedly become ‘robustly superhuman’ at establishing the internal consistency of a formal proof sequence of a (presumably first-order) mathematical language,
- only a human intelligence can validate that the proof actually formalised the ‘mathematical truth’ of that which was sought to be formalised.
The distinction can be expressed as the:
COMPLEMENTARITY THESIS: Mathematical ‘provability’ and mathematical ‘truth’ need to be interdependent and complementary, ‘evidence-based’, assignments-by-convention towards achieving:
(1) The goal of proof theory, post Peano, Dedekind and Hilbert, which is:
— to uniquely characterise each informally defined mathematical structure S (e.g., the Peano Postulates and their associated, classical, predicate logic),
– by a corresponding, formal, first-order language L, and a set P of finitary axioms/axiom schemas and rules of inference (e.g., the first-order Peano Arithmetic PA and its associated first-order logic FOL),
– which assign unique provability values (provable/unprovable) to each well-formed proposition of the language L without contradiction;
(2) The goal of constructive mathematics, post Brouwer and Tarski, which must be:
— to assign unique, evidence-based, truth values (true/false) to each well-formed proposition of the language L,
– under an, unarguably constructive, well-defined interpretation I over the domain D of the structure S,
– such that the provable formulas of L are true under the interpretation.
In other words:
(a) Whilst the goal of proof theory may be viewed as seeking to ensure that any mathematical language intended to formally represent our pre-formal conceptual metaphors and their inter-relatedness is unambiguous, and free from contradiction;
(b) The goal of constructive mathematics must be viewed as seeking to ensure that any such representation does, indeed, uniquely identify and adequately represent such metaphors and their inter-relatedness;
thus essentially ‘validating’ them in the sense of Per Martin-Löf’s 1987 analysis of the meaning and truth of a proposition, which can be treated as:
Löf’s Thesis: A proposition ‘A’ is a ‘truth’ if, and only if, it can be ‘asserted or judged’ as ‘A is true’ by appeal to some ‘evidence/proof’ for the truth of A which can be ‘validated’.
Anonymous
https://github.com/Lapin0t/grothendieck-cern
https://publish.uwo.ca/~jbell/univ.pdf
https://www.science.org/content/blog-post/business-scientific-publishing
Very excited for the tech behind https://en.wikipedia.org/wiki/2026_Minab_school_attack to solve the hodge conjecture can’t wait this is great what an exciting time to do math!
Anonymous
I think knee-jerk reactions to defend the status quo in mathematical practice are understandable but misguided.
A machine that is able to prove statements that a human has formulated, on the basis of human concepts (e.g. distance & volume) that have evolved through time, would seem helpful to the human endeavour of mathematics rather than destructive. In particular it does not eliminate the role that human mathematicians play in using their intuition in ways that a machine cannot substitute for (at the moment this includes the initiation of a new subject or choosing problems that are of interest to humans).
No doubt many mathematicians would feel displeased that their efforts in solving specific, hard problems have been superceded. But it’s important to try and understand which part of these reactions are reasonable and which are merely hubris.
We should keep in mind that AI is nothing more than technology, designed to serve our purposes
Is it designed to serve our purposes? And ‘AI’ is not what people have the biggest anxieties about, but say the companies developing such systems. They do not exist to serve our purposes.
Anonymous
Without human mathematicians, who would care what math problems can AI solve?
Anonymous
“Mathematics is only about solving problems.”
Mathematics is only about solving problems in the high school mathematics curriculum. If you want to change the perception of mathematics among the general public, many of whom don’t ever attend college, then the high school mathematics curriculum needs to be completely overhauled with significantly less emphasis on e.g. solving problems in their algebra classes.
Anonymous
Pure mathematicians will never win in any curriculum battle at the high school or university level vs the engineers and business leaders who have a “shut up and calculate” attitude towards mathematics. It’s why pure mathematics is getting defunded by universities, and all the money is headed towards research in data science, statistics, applied mathematics, etc.
Anonymous
That’s already being done in high schools across the United States. Go check out Ohio’s Algebra II equivalent classes for example. The data science and advanced quantitative reasoning classes have much less emphasis on getting the answer correct, because you’re dealing with real world data and building mathematical models. There isn’t a single correct answer here because of the messiness of the real world and the inherent limitations of simplified mathematical models to explain the world.
Anonymous
Since the post referred several times to games, I want to make a book recommendation: The Well-Played Game, by Bernard De Koven is an excellent meditation on why we play games. The thesis is that playing a game isn’t really about winning or losing–it is about achieving “the well-played game.” The book discusses the paradoxical need to at once care deeply about the game, but at the same time not to become so competitive that your opponent has to remind you to relax–it’s just a game. Another thesis is that the pursuit of the well-played game has much in common with the pursuit of the well-lived life.
I think many of these lessons carry over to mathematics.
12 September, 2026 at 11:15 pm
Anonymous
In chess, engines have become an oracle that tells chess players what is the “best move”, after which chess players start to theorise why the move proposed by the engine is the “best”. Even as AI produces intelligible proofs, would AI then become an oracle for truth and falsity of mathematical statements or which the job of mathematicians then becomes to digest these statements into what is termed in this blogpost as “logical” proofs?
13 September, 2026 at 12:50 am
Anonymous
The main counterargument for this essay is that the LLM’s could (and do) also help with producing the “intelligible notion of proof”. My main evidence for this claim is in fact from this very blog:
A digestion of the Jacobian conjecture counterexample
Anonymous
I don’t think this is a requirement: “,,,intelligible proof that human mathematicians can understand,,,”
I mean, if aliens showed up with a faster than light starship (to make a fun and extreme example), and they gave us a proof it works, could we understand it? What is they are simply smarter than the smartest human and we could never understand the proof? We could still hop on the ship and explore/infest the galaxy.
If other AI agents understand and accept the proof, would that be enough?
guillaume
Although I do agree that the way we do mathematics today is problematic and could be changed, I think one must be very careful with the idea that with AI we will just have a great new tool to do mathematics in another way. This might be true for me (an active mathematician who already spent years working hard, and most of the time failing on problems), but what about the next generation? How can they even become mathematicians without spending days and months and years trying, and often failing? Even if mathematics is about understanding more than about solving problems, we do not know another way of building understanding than the very patient process of research, and I do not see how it can survive if the use of AI oracles becomes normalized.
The idea that we can use AI for math looks short-sighted to me, I do not see how it is compatible with creating new generations of mathematicians.
This point of view seems (statistically) reflected in what I observe around me: some older or middle-aged colleagues are tempted to use it as a tactical tool, but the PhD students are all terrified and very much against its use.
(note: I wish I missed something and everything turned great in the end… )
Anonymous
About mathematics belonging to humanities. I definitely adhere to this, and I think that most mathematicians do what they do in such a spirit. But if this became the public’s view, we know what this implies in terms of funding…
Mathematicians should acknowledge that humanities are important, which, as a community, is not really what we have done so far. It was just too comfortable to rest on the public’s idea that math=technology=money, which, even we prefer not to think about it, is eventually the reason why math is widely taught and funded (an this is a card that our universities, departments, grant agencies, etc. have played regularly)
Siding with humanities and arts is the right thing to do, but the fight will be tough.
Anonymous
Agreed. IIt’s a stage play that AI companies are doing, first about RH claim, then FLT and now this. During last 2-3 years I worked with AI for numerical verifications and observed that they are nothing for math perspectives or are purely dependent on humans. This is my honest observation, in parallel we humans including junior FMs are playing at both sides worst to worst they are writing articles from other to praise their nonsense results by using the words like Breakthrough. This is absurd and a significant crime. So to put all burden on Ai companies is not justified. Math always survives and AI is a good addition. Dnt affraid. Just do your work. If someone tried to delete this comment then he is a real cowered.
Anonymous
Thank you for the wonderful and thoughtful post!
I recently stumbled into two old Richard Feynman quotes that feel apt for the moment:
- “I couldn’t reduce it to the freshman level. That means we really don’t understand it.”
- “We do not yet know all the basic laws: there is an expanding frontier of ignorance.”
In my own explorations, I’ve found that: (a) while AI is very capable of synthesizing, constructing and expanding from what is currently believed (and therefore in its weights), it struggles with areas that might be deeply wrong but are “against its weights” and (b) the existence of a formal proof might provide a crack in a problem, but it by no means we have captured the whole of the problem or passed Feynman’s test of understanding.
Given we’ve been handed an infinite accelerator to the frontier of ignorance, the path might be something more like the Langlands project to look beneath the classical axioms and strengthen our foundations. Terry’s extraordinary work on Equational Theories could be a lighthouse for the future. What would it look like to re-define the classical types based on their raw magma equational laws to push the limits of an axiom-free foundation for math? The LLMs have no priors for exploring the truncation effect of Nat on a freemagma tree, or the implications of selecting a single magma and arbitrarily labeling it zero.
Anonymous
millions of $s teams of engineers 1000s of watts on 10000 agents in a few days + billions of $s teams of scientists and engineers multi year work and megawatts of power to build the model vs 10-20 mathematicians over 80 years which is less than 1 mw of brain power to get the formulation right to feed into the ai. You call this progress?
Anonymous
I agree with the broader point that mathematics is about more than obtaining correct answers, and that understanding is central to its value. However, I would be cautious about classifying this particular work as merely an answer rather than a solution before its mathematical content has been carefully assessed.
I would be interested to hear from mathematicians who have read the manuscript closely: does it contain new mathematical ideas, useful constructions, or insights that could inspire further work? Even if discovering the argument required enormous computational resources, it does not follow that the argument itself is merely brute force or devoid of mathematical ideas. The resources used to find a proof and the mathematical understanding it offers are distinct questions.
We should also distinguish between a proof that has not yet been understood and one that does not offer understanding. AI may itself help us unpack a long manuscript and identify its conceptual structure. I am not claiming that this particular manuscript necessarily contains important new insights; rather, I think that an assessment of its mathematical value should be grounded in careful engagement with the argument.
There is a related issue within our own mathematical culture. I have heard one mathematician dismiss another’s work as “just technical computation” without new ideas. Sometimes such criticism is justified, but it can also be premature or unfair. Ideas need not take the form of a visibly new conceptual framework; they may also be embedded in difficult technical arguments. As we articulate standards for evaluating AI-generated mathematics, we should reflect on how carefully and fairly we apply those standards to one another. The call for understanding should motivate engagement with a proof, rather than become a substitute for it.
Anonymous
I agree with you that understanding methodology and techniques involved in a proof is very important. But, if this counterexample found more or less by brute force, passes per-review, why to worry? Proof is a proof
Anonymous
I agree that mathematics is about more than correct answers. However, I would hesitate to classify this manuscript as an “answer, not a solution” before its mathematical content has been carefully assessed. Does it contain ideas or constructions that could inspire further work? The enormous computational resources used to discover a proof do not imply that the proof itself is merely brute force or lacks insight. The resources used to find a proof and the mathematical understanding it offers are distinct questions. AI may also help us understand a long manuscript more quickly.
There is a parallel within our own mathematical culture: mathematicians sometimes dismiss others’ work as “just technical computation” without new ideas. Such criticism can be justified, but it can also be premature or unfair. Important ideas may be embedded in technical arguments, rather than expressed as a new conceptual framework. We should reflect on these habits when evaluating AI-generated mathematics.
Anonymous
It will always be valuable for humans, so long as we exist, to support a relatively small group of pure mathematicians who cherish mathematics and its history–even if we soon have AI capable of producing logical and intelligible proofs. It would be a loss to humanity for this group to disappear, just as it would be a loss if people who like to sew were never to sew again simply because machines can manufacture clothes of equal or better quality faster. (If that analogy makes you uncomfortable because it compares mathematics to sewing, then you will be in for a rough time in the AI future of mathematics.)
What AI will do for mathematics is weed out those who view mathematics primarily as a job or as a status-competition to be “won” via awards, breakthrough discoveries, aggressive social one-upmanship, or the thrill of intellectual dominance. The question is how many mathematicians of quality will this do away with? A lot, I suspect–many of whom, had strong mathematical AI not arrived, would have gone on to make great contributions.
But over time a new and gentler equilibrium will be established. To think that pure mathematicians will disappear completely is to take a rather cynical view of the motivations and psychology of most mathematicians. The beauty of mathematics in itself, the struggle to understand for oneself that beauty at a deeper and deeper level within a pleasant community of the like-minded, will reign supreme. And probably for the better.
13 September, 2026 at 12:02 pm
Anonymous
I feel like a lot of discussion about AI in mathematics (and to some extent, the arts and other knowledge disciplines) involves a lot of justified and yet premature existential dread. Frontier models, in their current form, are not sustainable. Not economically, not socially, and not environmentally. No-one really knows what a sustainable model of LLMs will look like and what is technologically possible.
It feels akin to seeing a peaceful but heretofore relatively isolated village suddenly attacked by invaders, who try to carry off what they think is valuable and destroy anything else. That people can and will invade the village may come as a shock, but the exact implications of that can wait until the villagers band together and drive the invaders off.
Anonymous
Disclaimer: I am not a Mathematician.
Lots of the recent AI discussions sound pre-Mochizuki to me. With Mochizuki the public perception of mathematical proofs and the perception of the health of the field changed. If we only had a formalization .. was often heard. Honest people in the field found his papers AI-Slop before the name was invented, nice people called it “as if we got a paper from the future”.
Maybe read about other fields flooded with AI-Papers that have no LEAN or Isabelle/HOL. They have a REAL problem.
On Navier-Stokes: I think it was ripe to be plucked and obviously a multitude of people worked against that goal with similar approaches. With Alpoge involved there is also a conception of “oh AI people A lost against AI people B “.
My prediction: Math tried to get the public excited with stuff like “Millenium problems” and the popularisation of FLT. Now it gets the results: The public is excited about stuff it has heard off. But the news cycle will fade quickly. The next falling millenial problem will get way less fanfare. Remember the 7th man on the moon? Riemann will be the last bang but then AI companies will loose interest in expensive PR-stunts in math. The real problem is people loose interest in learning anything. There will be no junior mathematicians, junior programmers .. you name it – so where will future seniors that guide it or use it come from?
Lets hope for the best, Nils
Anonymous
Thank you, Silvia and Eamon, for sharing your thoughts on this topic! I agree with a lot of what has been said: it is true that current AI models produce proofs of unclear intelligibility, and they are not yet able to produce new theory or create work of aesthetic value, among other things. But for how long do you think this will be the case? You grant that future systems will likely produce genuine, intelligible proofs, but the same reasoning applies to the other goals you list. Just a few months ago, nobody would have believed that a Millennium Prize problem would be solved autonomously by an AI model this year. I suspect that, in a few years, AI models will also be excellent at building new theory, communicating their results, and fulfilling many of the other goals that mathematicians currently value. And I don’t think this should fill people with dread: a world in which these scientific (including mathematical) g can be made quickly and easily by AI models is perhaps a world in which certain people are out of a job, but it is also a world in which the vast majority of people, who are not scientists but would benefit from the advances of science, experience huge improvements in their wellbeing.
I really enjoy this piece.
Some software engineers out there might be a bit tone deaf and label mathematicians being in denial, extrapolating from their own experience in how agentic engineering shocked the software engineering world.
So I wrote this companion piece hoping to translate your message to them. I hope that would be helpful:
Mathematicians aren’t mourning their craft: Translating “After Math” for software engineers
https://blog.kolen.dev/math/after-math
13 September, 2026 at 10:34 pm
Anonymous
As a computer scientist and mathematician that actually refuses to use AI tools myself, I don’t understand how even after this incident, there is an appetite for continued AI usage as a tool. AI is parasitic, and downstream usage of any sort is a tacit approval of possibly the greatest profit-motivated mass theft in history. These tools would not survive without the effectively free labor of millions, and yet not a dime is paid back in compensation. I fail to see how incentives will ever be aligned for humanity as a whole to produce creative and technical works in the future. Even streaming platforms pay their dues to the creators of content they host. Are we not falling into the “middle road” paradoxical trap? Often, a compromise is warranted yes, but sometimes, the correct response is at one of the extremeties.
Leave a comment Cancel reply
For commenters
To enter in LaTeX in comments, use $latex <Your LaTeX code>$ (without the < and > signs, of course; in fact, these signs should be avoided as they can cause formatting errors). Also, backslashes \ need to be doubled as \\. See the about page for details and for other commenting policy.
« Crowdsourcing a list of general resources on the purpose, value, and nature of mathematics
Wimbledon, the U.S. Open, and the future of mathematics »
Blog at WordPress.com.Ben Eastaugh and Chris Sternal-Johnson.
- Comment
-
Reblog
-
Subscribe
Subscribed
-
Already have a WordPress.com account? Log in now.
-
-
Subscribe
Subscribed
- Collapse this bar
%d