In May, a question about dots on a plane produced an unexpected answer. By September, AI laboratories were publishing arguments about fluid singularities, alongside files intended to let computers check the proofs. Between those announcements came new counterexamples, stronger bounds and a formalization of Fermat's Last Theorem.
The change in AI mathematics deserves more than a running score of conjectures defeated. These results ask different questions, carry different evidence and leave different work unfinished. A counterexample can overturn a belief without finding the best possible answer. An improved bound can be important while the famous conjecture beside it remains open. A computer-checked proof can establish a statement without explaining why its ideas will be useful elsewhere.
This is our examination of the major developments connecting OpenAI's May 20 unit-distance announcement to September's Navier-Stokes claim, with reporting current to September 22, 2026. It includes important intervening announcements and research that grew from them. It is a map of this sequence, rather than an exhaustive inventory of every AI-assisted mathematics paper. We have read the cited announcements, relevant theorem statements, research introductions and verification documentation. We have not independently refereed these proofs or rebuilt their formalizations.
Our central judgment is that the strongest evidence of progress has two parts: machines are producing mathematical arguments worth serious scrutiny, and people are already extracting further mathematics from some of those arguments. Whether that becomes sustained progress depends on the resources devoted to checking, explaining and extending the work.
May: a counterexample opens a new route through geometry
The unit-distance problem is easy to picture. Place a collection of points on a flat surface and count the pairs exactly one unit apart. As you add points, how large can that count become?
OpenAI's May 20 announcement attributed a new construction to an internal general-purpose reasoning model, evaluated on a collection of Erdős problems. It also published a separate companion paper by external mathematicians who examined the argument. The presence of that second document matters: readers can inspect what those mathematicians understood and reconstructed, beyond the laboratory's account of its model. OpenAI's announcement.
The original manuscript constructs infinitely many point sets with at least n^(1+δ) unit-distance pairs, for a fixed positive δ. In plain language, the improvement in the exponent persists as the examples get larger. That contradicts the conjectured almost-linear growth. It does not determine the exact maximum number of unit distances for every number of points, and the broader search for optimal bounds continues. The unit-distance manuscript.
The surprise was where the construction came from. The companion paper connects the geometric result to sophisticated algebraic number theory and names earlier mathematical ingredients. Its authors offer a simplified and somewhat generalized reconstruction. This is a useful example of human work after an AI discovery: identify the mechanism, make its dependencies visible and turn an argument into something other researchers can handle. The mathematicians' companion paper.
A reader looking for the significance of the May result should therefore follow the subsequent papers as closely as the initial announcement. A new technique earns a different kind of credibility when researchers use it to ask and answer further questions.
May to July: the ideas begin to travel
On May 27, Thomas Bloom, Will Sawin, Carl Schildkraut and Dmitrii Zhelezov posted a counterexample to the sum-product conjecture over the real numbers. Roughly, this concerns how much a set expands when its elements are added or multiplied together. Their construction allows both resulting sets to remain smaller than the conjectured near-quadratic scale. The authors explicitly say the unit-distance counterexample prompted them to reconsider number fields of large degree. They also explain that their final construction needs less number theory than the earlier result. The sum-product paper.
That is a concrete instance of an AI-originated result stimulating human-authored mathematics. It does not establish that an AI wrote the follow-on paper, and we should not erase its authors by folding their work into a laboratory's success count.
Cosmin Pohoata's preprint, first submitted June 11 and revised June 28, carries the sequence into the Elekes-Rónyai problem. It gives a polynomial example whose values on suitable sets expand less than expected, using ingredients from the recent unit-distance and sum-product constructions. The paper makes the link between the problems explicit. Pohoata's paper.
On July 6, Sungchul Lee, Pohoata and Daniel Zhu posted a further result about the Minkowski grid. Their construction preserves repeated-distance properties within subsets, with consequences for questions involving repeated distances and isosceles triangles. This is a stronger kind of structure than displaying one unusually rich configuration and leaving its internal behavior unexplored. The Minkowski-grid paper.
The optimistic reading has evidence here. The May result supplied material that other researchers could modify and reuse within weeks. Our proposed measure of success is the production of such usable methods, along with the effort needed to understand them. A raw count of solved problems would miss that distinction.
July: the Jacobian counterexample shows why scope matters
A second striking episode concerned the Jacobian conjecture. Terence Tao's July 21 exposition examines a counterexample produced using Fable AI: a polynomial map in three complex variables that behaves invertibly in a small neighborhood but sends distinct points to the same output overall. The conjecture's general claim fails in three dimensions and above; the two-dimensional case remains open. Tao gives explicit formulas and explains the construction's geometry. Tao's mathematical exposition.
An explicit counterexample can make its essential contradiction relatively accessible to calculation. Discovering why such an example should exist, and how to construct related ones, takes further mathematical work. The Jacobian episode lets readers see those different tasks in published form.
The distinction continued to matter in September. Arno van den Essen's September 15 preprint presents an elementary route to a counterexample equivalent, after linear changes of coordinates, to the example found by Levent Alpöge. This is a new explanation of the construction, not a second independent defeat of the original conjecture. Van den Essen's paper.
For a research manager, this suggests a practical change in what to reward. Funding the person who makes a complicated discovery understandable can unlock as much subsequent work as funding another search for a headline result. That is our assessment of the sequence, not a claim that universities have already changed their incentives.
August: a wider range of mathematical claims
OpenAI's August 1 release presented ten groups of results across mathematics and theoretical computer science. The company says an internal version of Astra generated the arguments; humans worked with the model to prepare manuscripts, and the model produced Lean certificates. This is a different production account from May's single-result announcement, and it makes the contribution of manuscript preparation explicit. The August announcement.
The accompanying collection, updated August 6, reports the following. These are descriptions of the manuscript's claims, not ten separate certifications by BIG CHANGE:
- Sphere packing: a sharper asymptotic upper bound in high dimensions.
- Binary and spherical codes: stronger limits on code sizes at specified separations.
- Group theory: construction of a nonsofic group.
- Operator algebras: counterexamples to Connes's rigidity conjecture.
- Arithmetic complexity: stronger circuit and formula lower bounds for the permanent.
- Quantum games: an exponential parallel-repetition theorem.
- Lattice problems: stronger approximation-hardness results for the closest vector problem.
- Convex geometry: a proof of Ehrhart's volume conjecture.
- Ramsey theory: a superexponential lower bound for multicolor triangle Ramsey numbers.
- Extremal graph theory: counterexamples to compactness and degeneracy conjectures.
The ten-result research collection.
The range is important, but it also makes a single total misleading. Finding a counterexample, improving a bound and proving a general theorem have different consequences. Nor does a result about the difficulty of a mathematical problem automatically demonstrate an attack on a deployed cryptographic system. Applications require their own chain of reasoning and evidence.
On August 10, Anthropic published a more narrowly defined advance near the Riemann hypothesis. It says an unreleased Claude model improved the lower bound on the proportion of zeta zeros lying on the critical line. Anthropic's mathematicians examined the work, outside specialists reviewed the paper, and a formalization was produced. The company expressly says Claude did not solve the Riemann hypothesis and does not expect these techniques to do so. Anthropic's account.
The linked paper states a bound slightly above two thirds, approximately 67.25%, and identifies the preceding analytic results it uses. This is an asymptotic mathematical statement, rather than a claim that checking a large finite sample of zeros proves the hypothesis. The distinction is essential: a lower bound on the proportion does not put every relevant zero on the line. The zeta-zero manuscript.
Other ambitious manuscripts are also circulating. A document hosted on Alpöge's website proposes a complex structure on the six-dimensional sphere. Its construction is available for examination, but the copy we accessed does not establish a reliable announcement date or a complete account of the AI contribution. We therefore include it as a proposal readers may investigate, without promoting it to an independently established milestone in this chronology. The six-sphere manuscript.
Early September: prime gaps expose a verification boundary
The run of announcements also reached gaps between prime numbers. A September 3 preliminary paper from the Axiom collaboration states that infinitely many pairs of consecutive primes are at most 212 apart. It credits Julia Stadlmann's analytic work and the earlier Polymath project. Its Lean certificate also takes analytic estimates and a separately checked variational certificate as hypotheses. This advances the bounded-gap question; the twin-prime conjecture requires infinitely many gaps of exactly two. The Axiom team's paper.
OpenAI's public PrimeGaps186 repository presents a still smaller bound, with a crucial qualification. Its Lean development is conditional on three input axioms covering two estimates from the literature and numerical integral bounds. The repository says the numerical certificate does not discharge those axioms. Readers should therefore distinguish the proposed mathematical argument from the portion formally checked under specified inputs. It would be inaccurate to describe this artifact as an unconditional, fully formal proof from the foundational axioms alone. The PrimeGaps186 repository.
Another OpenAI manuscript addresses long gaps: how large the intervals between consecutive primes can become. It reports an improved lower bound for the largest gaps below a growing threshold. This is a separate extremal question from finding infinitely many nearby prime pairs; progress on one should not be counted as a solution to the other. The long-gap manuscript.
These details make the prime-gap episode particularly useful. Two numbers in a headline can look like a simple race. Once the proof dependencies become visible, the better question is which steps have been established by which methods. Making assumptions explicit is valuable even when a formalization remains incomplete.
September 4: formalization becomes part of the discovery story
Anthropic's September 4 announcement concerns a theorem whose mathematical proof was already known: Fermat's Last Theorem. The claimed achievement is a complete Lean formalization, produced largely autonomously by Claude over eleven days. The company describes human direction and a collaboration platform that helped agents keep track of dependencies. It credits the mathematical proof tradition on which the work rests. The formalization announcement.
The public repository offers more specific evidence than the headline. It states the theorem, records dependencies and documents checks against Lean's standard axioms and Mathlib's version of the statement. It also describes itself as a research artifact that is not maintained. We inspected this documentation; we did not rerun its build. The FLT repository.
If the same tools that produce more candidate arguments can help formalize them, checking capacity can grow too. That is a substantial reason for optimism. Later researchers gain something concrete to inspect. They still need to know whether intermediate results are easy to reuse, whether dependencies remain buildable and who maintains the artifact. The volume of generated code alone cannot answer those questions.
There is a useful institutional choice here. A laboratory can release a proof as a finished demonstration of its model, or support it as infrastructure that other people will work on. Those approaches create different obligations after launch day. Maintenance, explanatory examples and stable references deserve to be part of a research budget.
September 8: what the Navier-Stokes result actually claims
The fluid result brings these questions into sharper focus. OpenAI's September 8 announcement, updated September 10, presents a proposed solution to the Navier-Stokes existence and smoothness problem. It attributes the work to an internal model operating through coordinating agents, and releases a written argument and Lean formalization. OpenAI says it does not intend to claim the Millennium Prize. The announcement.
The manuscript's setting is three-dimensional incompressible fluid motion with positive viscosity and a carefully constructed external force. Starting from rest, the proposed solution develops unbounded velocity in finite time while its total energy remains bounded. The force is smooth and confined in space and time. Its mathematical construction uses a collapsing vortex and corrections arranged so that the remaining force stays smooth. These are claims about solutions to equations, rather than observations from a physical experiment or a new engineering simulator. The Navier-Stokes manuscript.
The external force is central to understanding the scope. Charles Fefferman's official Clay problem description allows smooth forcing in the breakdown alternatives C and D. Its global-smoothness alternatives A and B concern the unforced equations. A valid result of the proposed kind can therefore address an explicitly permitted Clay alternative while leaving the unforced global-regularity question unresolved. Calling the forcing irrelevant would exaggerate the theorem; dismissing it as outside the stated problem would misdescribe the rules. The official problem statement.
OpenAI also released a separate Euler argument, concerning an idealized fluid without viscosity. That manuscript proposes finite-time breakdown from smooth initial data without external forcing. Euler and Navier-Stokes are related equations, but the assumptions and conclusions in these two papers must be kept separate. The Euler manuscript.
The surrounding research history matters. The European Mathematical Society's September 10 statement recognizes the work of Córdoba, Martínez-Zoroa and Zheng, alongside Alpöge and Buckmaster and earlier mathematical contributions. It also raises questions about access, authorship and credit. An account that jumps directly from a model name to a theorem loses the accumulation of ideas that made the work possible. The EMS statement.
On September 11, Clay responded with qualified excitement about the apparent resolution and said its evaluation and allocation of credit would follow an intentionally unhurried process. That is a meaningful institutional response. It is not a prize award or a declaration that every aspect of the work has completed review. Clay's announcement.
For readers, the accurate conclusion is substantial enough without adding more: an AI laboratory has released a proposed proof aimed at a recognized Millennium problem, with inspectable mathematical and formal artifacts, and major institutions are taking it seriously. Broader acceptance, attribution and understanding are still processes with work to do.
A proof check answers a precise question
Formal verification changes the evidence available to reviewers. It should also make reporting more precise.
Lean's own documentation distinguishes a valid proof from the meaning of the statement being proved. A basic successful check establishes that a formal statement follows from its definitions and assumptions. Additional checks can expose unfinished dependencies, audit axioms and compare a proof against an independently specified statement. The documentation describes stronger verification using external checkers and still identifies assumptions that remain. Lean's validation guide.
Imagine a researcher who needs a bound that applies to every input of an algorithm. An assistant supplies a formally correct theorem, but its definition of an admissible input excludes a difficult class. The proof can be correct while the researcher's application remains unsupported. This is a hypothetical example of why the translation between the question and its formal statement needs attention.
Novelty creates another kind of check. A proof system does not settle whether the same argument appeared under different terminology in an older paper, whether the credit is complete, or whether a claimed improvement changes anything important for the application. Those judgments require literature work and subject expertise.
We would therefore ask a laboratory releasing a major result to supply a durable package: the exact claim in ordinary mathematical language, its formal counterpart where available, the proof and dependencies, a clear account of human and model contributions, and a record of what has been reviewed and revised. This is our proposed reporting standard. It gives other researchers a way to locate responsibility and reproduce the relevant checks.
The advisory group addresses a growing coordination problem
The September 21 Advisory Group on Mathematics and Artificial Intelligence announcement arrives against this background. The group says it is independent, unpaid and willing to advise any relevant AI company. Its immediate task is advising OpenAI on the release of further results the company reports having obtained. It promises public recommendations and explicitly says it has no decision-making power inside the companies. The announcement on Terence Tao's blog is a guest post by the group. The group's statement.
OpenAI describes a remit involving review, communication, significance and dissemination. It also says the group is not responsible for advising the pace of its internal mathematical progress. The advisory role should therefore be understood as a channel for scrutiny and coordination, with decisions remaining at the company. OpenAI's advisory-group announcement.
There are reasons to welcome this arrangement. Better coordination can reduce duplicated reviewing work, identify the right specialists and ensure that the description of a result matches what its evidence supports. Its limitations are equally clear: advice needs a response, and independence alone provides no enforcement mechanism. Readers should watch the published recommendations and what companies do with them.
The skeptical case also concerns the purpose of research. The September 11 Math and AI declaration argues that a race to solve listed problems can neglect the development of understanding and the training of future mathematicians. Its signatories describe a risk to the processes through which ideas become teachable and useful. That is a serious position from participants in the discipline, rather than a measurement showing that all AI use has already harmed it. The declaration.
Henry Cohn develops a related argument in a September 15 guest essay on Tao's blog: poorly explained results can impose substantial work on the community that must absorb them. His concern includes incentives for people who do that explanatory work. Correct attribution matters here too; this essay is Cohn's, even though Tao hosts it. Cohn's essay.
The next advance should be easier for someone else to use
The May-to-September sequence supports a hopeful account with concrete examples. A geometric counterexample inspired further constructions. Researchers found clearer ways to explain a surprising polynomial map. Formalization produced additional artifacts through which complicated reasoning can be inspected. The ingredients for a productive relationship between model output and mathematical practice are visible.
The pessimistic scenario is also practical. Laboratories might generate proposed results faster than others can understand them, then count the announcements as completed scientific contributions. Reviewing could become a burden placed on a small group of specialists, while the resources and prestige flow toward the systems producing the backlog. Limited access to the models could deepen the imbalance between those who generate discoveries and those expected to assess them.
Our view is that laboratories, funders and journals should measure both sides of the process. Track candidate discoveries, but also track independent scrutiny, useful simplifications, repaired arguments, reusable formal libraries and subsequent work. Give credit to the people who make a result intelligible. Publish corrections with the same persistence as announcements.
For a reader trying to follow the next breakthrough, the most revealing question is specific: what can another researcher now do that they could not do before? The answer might be construct a counterexample, establish a stronger guarantee, check a difficult argument or teach a new method. That is where the progress of AI mathematics becomes progress in mathematics.
