AGI Has Come for Mathematics
Three years ago, I watched ChatGPT fail a basic counting problem. Now I am watching it change what it means to be a mathematician.
With an anonymous research mathematician and two-time IMO medalist
My first encounter with AI doing mathematics in the wild was a failed attempt to cheat. It was 2023, and I was helping teach an undergraduate mathematics course. During an exam, a student tried to cheat by asking ChatGPT to solve one of the questions. The question was a basic counting problem in combinatorics, the sort of thing a reasonably well-trained middle-school student doing math competitions could solve.
ChatGPT could not solve it. The student came back with the wrong answer, got caught, and the whole operation was an utter failure.
I believe the model was GPT-3.5. My takeaway at the time was roughly that AI was still extremely far from being mathematically serious. If you could not reliably solve this sort of problem, there was an enormous distance between you and anything resembling research mathematics.
The first result that made this picture less comfortable came in 2024, when DeepMind's AlphaProof and AlphaGeometry 2 together solved four of the six International Mathematical Olympiad problems, enough for a silver-medal-level score. This was particularly striking to me because I had competed in the IMO myself and won two medals. I knew firsthand what these problems demanded.
From a counting problem to a wider mathematical world.
Still, there were plenty of reasons to discount the result. The system was highly specialized. AlphaProof worked with formalized problems in Lean and relied on reinforcement learning and large-scale proof search; the geometry problem was handled by a separate geometry system. The problems had to be translated into formal language by humans, and some solutions took up to three days. You could reasonably believe that this was a spectacular engineering achievement without concluding that general-purpose AI was becoming a mathematician.
By early 2025, however, I was already using AI routinely to generate solutions to undergraduate homework problems for courses I was teaching. That was a quieter milestone, but perhaps a more revealing one. The same technology that had recently failed an elementary exam problem was now useful enough to enter my everyday mathematical workflow.
Then came the 2025 IMO. I remember how it felt when I saw the news. Experimental models from OpenAI and Google DeepMind had reached gold-medal level, solving five of the six problems, this time directly from the natural-language problem statements and within the normal contest time limit. The news shook me much more than I expected.
The IMO had been part of how I understood my own mathematical ability for a long time. So, perhaps somewhat pathetically, I spent time trying to solve that year's problems myself. There was a primitive psychological motive behind it: I wanted to reassure myself that I was still better than the machine. I wanted there to remain some benchmark on which I could look at the model and say: yes, this is impressive, but I can still do something it cannot. I don't think I fully appreciated then how temporary that comparison was.
What disturbed me about the IMO result was not merely that one expensive model could perform at the level of a gold medalist. It was the obvious extrapolation. Once one machine can do this, there is no reason to imagine only one of them. You can run hundreds or thousands of copies, have them pursue different approaches, let them criticize one another, and spend an amount of aggregate mathematical effort that no human could match.
There is a common instinct to draw a sharp line between olympiad mathematics and research mathematics. Certainly they are different. Research is longer-horizon, much less well specified, and much more dependent on choosing the right questions and intermediate lemmas. But having spent substantial time around both, I never thought the gap was mystical. Once a research problem is broken into sufficiently concrete pieces, a great deal of research consists of solving difficult but reasonably well-defined subproblems, repeatedly, while maintaining some sense of direction.
So the 2025 IMO result was the first time I seriously thought: this is not going to stop at competitions. A year later, even the small consolation I had been looking for was gone. The models were no longer merely matching olympiad medalists. They were proving results in areas close to my own field that I would have considered serious achievements for professional mathematicians. The comparison had stopped being between AI and talented students. It was becoming a comparison between AI and us.
My own field is combinatorics, so naturally I paid particular attention when AI systems started resolving problems from the Erdős problem collection. The initial reaction to these results was, in retrospect, almost endearing. Erdős left behind an enormous number of open problems, some famous and some obscure. An open problem does not necessarily have to be difficult; sometimes nobody sufficiently qualified has been sufficiently bored. Perhaps the machines were simply exploiting this neglected corner of the mathematical market.
There was a brief period in which this distinction felt important. Yes, AI could solve an Erdős problem, but was it an interesting Erdős problem? Yes, it had produced something new, but was this really mathematical creativity? Perhaps the machine was unusually good at taking a clearly specified question and exhausting the possibilities, while the genuinely important parts of research, including taste, intuition, and conceptual innovation, remained safely human.
This was a reasonable position. It also had a half-life of approximately six months.
In May 2026, an OpenAI model disproved a major conjecture associated with Erdős's unit-distance problem. The planar unit-distance problem is not some question forgotten in the back pages of a problem collection. It is one of the canonical problems of discrete geometry, posed by Erdős in 1946 and studied for eighty years.
How many pairs can be one unit apart?
Put dots anywhere on a flat plane. A unit is one fixed length, shown by the ruler. Count a pair of dots only when they are exactly one unit apart. For a given number of dots, what is the most pairs any arrangement can have?
The open question was about growth: as the number of dots increases, how quickly can that best possible count rise? Erdős predicted a limit only slightly faster than the number of dots. The 2026 result overturned that prediction.
Try a small case
Move B while keeping it one unit from A. What path does it follow? Then choose seven points, move the center dot, and try to restore all twelve connections.
1 pair is exactly one unit apart.
Move B off the circle. The connection disappears.
A to B: exactly 1 unit.
Drag a dot. Near the circle, it snaps to exactly 1 unit. You can also focus a dot and use the arrow keys.
Move a point precisely
Arrow keys and sliders move freely. Use the button to land exactly on the circle.
Two points. One unit-distance pair.
Seven points. Twelve pairs. Each of the six sides and six lines to the center is exactly one unit long.
What was the answer?
Erdős’s predicted growth limit was false. The disproof builds ever-larger arrangements with more one-unit pairs than that limit permits. Its surprising ingredient is algebraic number theory: richer number systems supply many more equal-length differences between points. This settles the conjectured bound; the exact maximum for arbitrary sizes remains open.
Who did the work? An internal OpenAI reasoning model produced the disproof, announced May 20, 2026. Nine mathematicians, including Noga Alon, Thomas Bloom, Tim Gowers and Will Sawin, wrote a human-verified, simplified account.
How can a construction disprove a growth limit?
Write u(n) for the largest count among n points. Erdős predicted u(n) = n1+o(1): for every positive ε, however small, the count would eventually stay below n1+ε. The disproof gives arbitrarily large examples with at least n1+δ pairs for one fixed positive δ. Choose ε smaller than δ, and the examples eventually exceed the predicted limit. Theorem 1.1 of the companion paper gives the precise result.
Then in July came the Cycle Double Cover Conjecture. This one felt different to me because it was much closer to home. The conjecture, originating with Szekeres and Seymour, is one of the central longstanding problems in structural graph theory: every bridgeless graph should admit a collection of cycles covering each edge exactly twice. OpenAI announced a proof, and serious graph theorists, including Jim Geelen and Sang-il Oum, subsequently wrote their own expositions of the argument.
Every line.
Exactly twice.
A graph is a network of dots joined by lines. A cycle is a loop that returns to its starting dot without retracing a line or revisiting another dot. A double cover is a collection of these loops that uses every line exactly twice in total.
The question: does every finite network with no bridge have a double cover? A bridge is a line whose removal splits a connected part of the network. Such a line cannot be part of a loop: crossing it leaves no other way back.
Try a small case
Trace one loop, then choose a collection that makes every line’s counter read 2. Can you predict which lines still need another pass before choosing the next loop?
Start at A. Follow A → B → C → A. Coming back to A closes the loop.
The number on each line counts its passes. The target is 2.
Each counter records how many selected loops use that line. You are checking one graph. The conjecture asks for a double cover of every bridgeless graph.
What was the answer?
Yes, every finite bridgeless undirected graph has a double cover. Here, “undirected” means lines have no one-way restriction. The July 2026 proof establishes this for every such network, however tangled. Its key move assigns two labels to each line so that each label traces closed loops; every line then belongs to two loops.
Who did the work? OpenAI’s proof credits GPT-5.6 Sol Ultra, with the writeup produced by Codex using Sol. Graph theorists Jim Geelen and Sang-il Oum subsequently wrote their own expositions explaining the argument.
How do two labels turn into loops?
After reducing to networks with three lines at each dot, the proof gives every line two distinct labels. At each dot, a given label appears on either zero or two incident lines. Follow one label: wherever you arrive, there is exactly one matching way to leave, so the route closes into a cycle. Because every line has two labels, all these cycles together cover it twice. The hard step is proving compatible labels always exist; the argument uses established graph-flow results and linear algebra.
Our tetrahedron gives a particularly visible double cover: every line borders two triangular faces. That small case was already understood. The general theorem also allows a collection to use the same cycle more than once.
There is a psychological difference between reading a press release saying that AI has solved an important problem in some field you do not know, and watching it solve a problem in your own mathematical neighborhood. I did not need anyone to explain to me that Cycle Double Cover was serious. I knew what kind of result it was. If a human mathematician had solved it, this would have been a career-defining achievement.
And the results kept coming. On August 1, OpenAI reported a collection of other advances on longstanding problems in mathematics and theoretical computer science. Later that month, a prerelease OpenAI model produced a Lean-checked proof for the Erdős–Sós problem in a research benchmark. The conjecture is one of the famous open problems in extremal graph theory.
Can you find every tree?
A tree is a connected network with no loops. It can branch like a star or stretch into a path. The Erdős–Sós question asks: if a network has enough lines, must every tree of a given size appear inside it?
For example, must every five-dot network with six lines contain both of the three-line trees below? Try finding them in this network.
Find the tree hiding in the network
Choose a shape, then select three lines in the network. You can rotate or bend the shape: only which dots connect matters. Extra, unselected lines do not count against you.
Five dots. Six lines. Both tree shapes are hiding here.
A path visits four dots in a row. Its two middle dots each touch two selected lines.
Select three lines to find a path.
These are the only two tree shapes with three lines. Finding both checks this little network; the conjecture asks for a guarantee across networks and trees of every size.
What was the answer?
Yes: once the benchmark’s edge threshold is met, every tree of the requested size is guaranteed to appear. A 26 August 2026 attempt produced the Lean-checked proof. This threshold can require one extra edge compared with the classical conjecture. The repository reports a sharper internal lemma; the benchmark compared the advertised statement.
Who did the work? A prerelease GPT-6 Astra from OpenAI found the proof autonomously in Tom Adamczewski and Thomas F. Bloom’s FrontierMath Erdős benchmark. Bloom reviewed the formal statement for faithfulness. Adamczewski directed the AI-written repository packaging the proof.
How many lines are “enough”?
For a tree with k edges and a graph with n vertices, the classical threshold is more than (k − 1)n/2 edges. The compared statement requires at least (k − 1)n/2 + 1. They differ when (k − 1)n is odd.
Here, k = 3 and n = 5, so both require six edges. The toy checks only the selected lines; containment does not require deleting the network’s other lines.
It is difficult to know how to quantify what happened over those months. Saying that mathematical research had become ten times faster or a hundred times faster would pretend to a precision that we obviously do not have. But subjectively, from inside combinatorics, it felt like watching perhaps a decade's worth of headline progress compressed into half a year.
At some point the creativity debate began to seem beside the point. Maybe the machine is creative. Maybe it is not. I am happy to let philosophers settle the terminology. If you have a machine that repeatedly produces proofs of theorems that professional mathematicians wanted proved, the employment consequences are not greatly altered by whether we decide that its internal experience deserves the word "creativity."
There remained, however, a serious bottleneck. Mathematics is unusual among intellectual activities in that correctness is non-negotiable. If AI becomes capable of producing a thousand difficult proofs in the time humans previously produced ten, we have simply moved the bottleneck from proving mathematics to checking mathematics. A two-hundred-page proof that nobody has the time to read is not yet a very useful foundation for another two-hundred-page proof that nobody has the time to read.
This is why I think one of the most consequential results of this whole period might turn out not to be a new theorem at all. On September 4, Anthropic announced the first complete computer-checked formalization of Fermat's Last Theorem. Dozens of Claude agents worked largely autonomously for eleven days, with occasional high-level human direction, writing about thirteen million lines of Lean and proving tens of thousands of intermediate theorems along the way. The resulting proof is checked by Lean's kernel and uses only its standard axioms.
Fermat's Last Theorem itself, of course, was already proved. The interesting part is the scale. Formalizing modern mathematics has historically been extraordinarily labor-intensive. If models can automatically turn extremely complicated mathematical arguments into formal proof objects, then humans no longer have to personally check every line of each successfully formalized proof.
Can two cube volumes
equal a third?
A square with sides of length a has area a². A cube with sides of length a has volume a³. The little raised number is the power: a³ means a × a × a. With whole-number sides, two square areas can add up perfectly: 3² + 4² = 5².
Fermat’s question: can aⁿ + bⁿ = cⁿ ever work when a, b and c are positive whole numbers and the whole-number power n is at least 3? The cubes below let you explore n = 3. The question covers every higher whole-number power too.
Try to make the volumes match
Keep the blue and orange sides at 3 and 4. Can you find a whole-number gray side that holds exactly their combined volume? Then change any of the three numbers. Switch to squares to see an equality that works.
3³ + 4³ ≠ 5³
27 + 64 = 91. The gray cube holds 125. You are 34 unit cubes short.
Try squares: 3² + 4² = 5² does work. Fermat’s claim is that this equality cannot happen for cubes or any higher whole-number power.
A 3 × 3 × 3 cube holds 27 unit cubes. A 4 × 4 × 4 cube holds 64. Their combined volume is 91, less than the 125 units in a 5 × 5 × 5 cube.
Squares behave differently: 3² + 4² = 9 + 16 = 25 = 5².
What was the answer?
There are no such positive whole numbers, for any whole-number power above 2. For cubes and higher powers, changing the inputs can make the two sides close, but never equal. That is Fermat’s Last Theorem. Trying every number in this playground would still leave infinitely many cases; the proof rules them all out together.
The new achievement in September 2026 was formalization: expressing an existing human argument in Lean, a language whose proof checker verifies the logical steps. It made an already-solved theorem computer-checkable.
How can one proof rule out infinitely many possibilities?
The argument runs backward from an imagined exception to a contradiction. The released proof path follows this strategy:
- Assume an exception exists. After reducing to the necessary exponents, use those numbers to construct a special equation describing a curve, called a Frey curve.
- Apply deeper results. The curve would have to correspond to another kind of mathematical object, called a modular form.
- Reach an impossibility. Those same properties would require a nonzero modular form in a class where every form is zero. The imagined exception therefore cannot exist.
Formalization supplies the precise definitions and logical links behind this outline. It is much more than a search through numbers.
Who did the work? Andrew Wiles proved the theorem, with Richard Taylor helping repair the proof; the work was published in 1995. In 2026, Anthropic researcher Tianyi Peng coordinated Claude agents to formalize it, building on that human proof and existing Lean projects, including the project led by Kevin Buzzard. See Anthropic’s account and acknowledgments and Buzzard’s checking account.
This changes the character of the verification problem. Imagine a machine proposes a conjecture, other machines search for a proof, another set of machines translates that proof into Lean, the kernel checks it, and then the entire system proceeds to build further mathematics on top of the certified result. Humans might want to understand the argument eventually. We might want an elegant exposition. We might want to know why it works. But human comprehension need not be on the critical path between one theorem and the next.
But even the fact that this is now the disclaimer one has to insert is surreal. In 2023, I watched ChatGPT fail a basic counting problem on an undergraduate exam. In 2026, I am adding a cautious caveat because a machine may have just resolved a Millennium Prize Problem.
AGI has come for mathematics.
The disruption inside mathematics is already difficult to describe. A fellow mathematician tells me that research in their group increasingly feels like playing a slot machine. Everyone has a favorite problem. You set agents loose on it, give them papers, try different scaffolding, let them run, and see what comes back. Then you pull the lever again.
The absurd part is that this is rational behavior. If there is some chance that a few days of compute will solve a problem that might otherwise occupy years of your life, of course you run the agents.
I don't know what this does to mathematical academia. It is not even clear to me what a mathematics PhD means anymore. A thesis traditionally represented several years of training culminating in one substantial piece of original work. But if a student can use agents to produce thesis-level results every month, then the old unit of account, one student, several years, one theorem, has broken down. In some ridiculous but increasingly non-ridiculous sense, a graduate student could produce dozens of PhD theses during a PhD.
Perhaps proving theorems becomes cheap and choosing the right theorems becomes valuable. Perhaps explanation becomes more important than discovery. Perhaps mathematicians become managers of large populations of machine researchers. Perhaps this framing too will look quaint six months from now. I don't know what the equilibrium is.
What I do know is that three years ago I watched ChatGPT fail an easy counting problem on an undergraduate exam. Last year I was trying to solve IMO problems to reassure myself that I was still better than the machine. I now know that I am not, and I don't think mathematics academia has begun to understand what that means.
Notes on the results
The Erdős–Sós benchmark's compared formal statement has a small threshold distinction from the classical statement. Its repository describes a stronger internal lemma; the claim here refers to the checked benchmark result.
Fermat's Last Theorem was already proved by human mathematicians. The formalization builds on that work and existing formal libraries. Lean checks a proof against its encoded statement and assumptions; the statement must still express the intended theorem. Lean's validation documentation explains that distinction.