From the airflow grazing an airplane wing, to the massive vortices circling the atmosphere, to the blood pumped from a beating heart, fluid motion has long been treated as a continuum and described within the framework of differential equations. The system of equations derived by Claude-Louis Navier and George Gabriel Stokes in the early 19th century forms the backbone of modern engineering and earth science. But embedded within this supremely practical set of formulas lies a fundamental question that has stumped mathematicians for roughly 90 years.
Does a fluid starting from a smooth initial state continue moving smoothly forever, thanks to the friction-like action of viscosity? Or does its velocity suddenly leap to infinity at some instant, causing the very description of it as a continuum to break down?
On September 8, 2026, OpenAI announced that it had produced its own answer to this question. The company claims that an unreleased internal model it is developing analytically proved that a finite-time singularity (blowup) occurs in the three-dimensional incompressible Navier-Stokes equations, and that it completed formal verification of the proof using the interactive theorem prover Lean. The target was "Statement C" and "Statement D" of the Millennium Prize Problems set by the Clay Mathematics Institute — the statements asserting that, under smooth applied forcing, the smoothness of solutions breaks down.
However, the announcement was not welcomed as a purely celebratory moment for mathematics. Fierce debate has erupted at the boundary between the mathematics community and AI research, touching on friction over priority with a group of mathematicians who had been preparing similar prior results around the same time, the transparency of the verification process, and the value of humans "understanding" a lengthy proof generated by a machine.
The Clay Institute's Formulation and the Limit Where Smoothness Breaks Down
The problem of existence and smoothness for the Navier-Stokes equations is one of the seven Millennium Prize Problems designated by the Clay Mathematics Institute (CMI) in 2000. According to the official formulation written by Charles Fefferman, the $1 million prize is awarded for proving or disproving any one of the following four statements (A, B, C, and D).
| Statement | Spatial setting | Forcing term $f(x,t)$ | Essence of the claim |
|---|---|---|---|
| (A) | 3D Euclidean space | 0 (no forcing) | A smooth global solution always exists |
| (B) | Periodic boundary conditions (torus ) | 0 (no forcing) | A smooth global solution always exists |
| (C) | 3D Euclidean space | Smooth, decaying forcing exists | A smooth solution ceases to exist in finite time (blowup) |
| (D) | Periodic boundary conditions (torus ) | Smooth, periodic forcing exists | A smooth solution ceases to exist in finite time (blowup) |
Looking back at history, French mathematician Jean Leray showed in 1934 that generalized solutions called "weak solutions" exist globally in time. But whether such weak solutions are unique, and whether they retain infinitely differentiable smoothness throughout, remained unresolved.
What's worth noting here is that while Statements A and B ask about eternal smoothness in a setting with "no forcing" ($f=0$), Statements C and D allow for the existence of blowup in a system with "physically reasonable smooth forcing" applied. A physically reasonable solution means that the velocity field $u$ and pressure $p$ are -class, and that the fluid's total kinetic energy (the integral of over ) remains finite over time.
- No forcing (f=0)
- With smooth forcing
データを表で見る
| No forcing (f=0) (Statement category) | With smooth forcing (Statement category) | |
|---|---|---|
| Statement A (global smoothness) | 1 | 0 |
| Statement B (torus smoothness) | 1 | 0 |
| Statement C (finite-time blowup) | 0 | 1 |
| Statement D (torus blowup) | 0 | 1 |
The proof OpenAI claims targets precisely these Statements C and D. The company says it constructed a scenario in which a smooth forcing is continuously applied to an initially still, smooth fluid, resulting in a singularity where velocity diverges to infinity within a finite time.
According to the company's own explanatory materials, the constructed solution has the dynamics of a vortex filament: the fluid spirals inward while being stretched axially like spaghetti. As the central region contracts sharply while accelerating its rotational speed, the fluid's total energy remains finite. The mechanism is one in which the acceleration term, pressure gradient, momentum transport (advection term), and viscous dissipation term that make up the Navier-Stokes equations all grow extremely large while precisely canceling each other out — with the forcing term itself remaining smooth throughout, even as the velocity gradient alone becomes unbounded.
The fact that the fluid's velocity reaches infinity does not predict that real gases or liquids move at infinite speed. As OpenAI itself acknowledges, real fluids are collections of molecules, and in regions where the velocity gradient has grown to the extreme, the very approximation of treating fluid as a continuum loses its validity. This means the equations have mathematically exposed the boundary line beyond which one must return to the perspective of kinetic theory or statistical mechanics to describe the system's behavior.
An 88-Hour Search Guided by 10,000 Agents and 130 Billion Tokens
According to a blog post published by OpenAI, the proof was derived by an unreleased internal model — said to have "significantly greater capability than GPT-6 Astra" — whose training began on August 28, 2026. Training of this model is reportedly still ongoing, and it had shown extremely high mathematical reasoning ability on internal benchmarks.
According to the company's explanation, the search project got underway in earnest on Tuesday, September 1, 2026. Having heard rumors that two of the Millennium Prize Problems had been solved, the research team decided to test the capabilities of this new model by setting it loose on unsolved Millennium Problems and related important challenges.
The system was composed of a fleet of autonomous agents equipped with cached web browsing privileges and a code execution environment. The agents were divided into multiple groups that communicated with one another as they worked. In the group ultimately responsible for solving Navier-Stokes, up to 10,000 agents reportedly operated in parallel simultaneously.
| Search phase | Scale of agents deployed | Time required | Mathematical challenge addressed |
|---|---|---|---|
| Initial exploration (Euler equations) | About 100 agents (per company blog) | About 50 hours | Regularity breakdown of the inviscid Euler equations with no forcing |
| Pivot to Navier-Stokes | Up to about 10,000 agents | About 88 hours (cumulative from the start) | Constructing a singularity in the Navier-Stokes equations, including the viscous term |
| Formal verification (Lean) | Using GPT-6 Astra | About 17 hours | Syntax checking and axiomatic consistency verification of the entire proof |
In the initial phase of the search, the team set the regularity problem for the "incompressible Euler equations" — corresponding to the limit of the Navier-Stokes equations with the viscosity term removed — as a test case. At this stage, roughly 100 agents worked cooperatively for about 50 hours and derived a solution in which a singularity forms in the forcing-free Euler equations.
Following this success, the research team reassigned agent groups that had been allocated to other Millennium Problems toward analysis of the Navier-Stokes equations. In doing so, they used Codex to aggregate intermediate findings from each agent group and cross-feed useful approaches back to other groups as prompts. Furthermore, as the search progressed, agents were progressively updated to newer versions of the internal model that had undergone additional training.
As a result, on Saturday, September 5, roughly 88 hours after the search began, the agent fleet arrived at an analytical proof of finite-time blowup for the Navier-Stokes equations. Formalization and verification using the interactive proof assistant "Lean" was then carried out using GPT-6 Astra, with the work reportedly completed 17 hours later.
Across all trials, the total number of messages exchanged between agents reached 4.9 million, with output totaling roughly 300 billion tokens. Of that, 2.7 million messages and approximately 130 billion tokens were devoted specifically to solving the Navier-Stokes problem.
However, some discrepancies exist between these operational figures as described in the company blog and those reported externally. According to OpenAI's press briefing as reported by the British popular science magazine New Scientist, about 1,000 agents were deployed for 50 hours on the Euler equations, after which the subsequent expansion to Navier-Stokes was completed by about 10,000 agents in roughly 11 hours. The computational cost, converted into customer billing rates, is said to amount to roughly $15 million. A report by the Indian economic media outlet Moneycontrol also cited OpenAI Vice President Mark Chen as describing the computational cost as "emphatically in the millions of dollars." It has also been reported that Sébastien Bubeck described the effort as "roughly a 1,000x scale-up" compared to past mathematical achievements, though the specific absolute values of computation or token counts being compared have not been disclosed in any publicly available materials confirmed so far.
Notably, OpenAI has positioned this achievement as a "snapshot of progress" toward the advanced AI it is aiming to build, and has explicitly stated that it does not intend to claim the Clay Mathematics Institute's $1 million prize.
A Collision With Prior Research and a Reprise of "Deep Blue vs. Kasparov"
Behind OpenAI's flashy announcement, a complex dispute over priority and information access surfaced with researchers who had been working at the frontier of pure mathematics.
At the center of it was collaborative research by Tristan Buckmaster, a mathematics professor at NYU's Courant Institute, and Levent Alpöge, a mathematician employed by the AI company Anthropic. Ahead of OpenAI's announcement, the pair published a series of preprints showing that, under smooth forcing, singularities form in finite time across three fluid models: the incompressible porous media equation (IPM), the two-dimensional Boussinesq equations, and the three-dimensional incompressible Euler equations.
This research built on a program pioneered by Diego Córdoba and Luis Martínez-Zoroa of the Autonomous University of Madrid and the Institute of Mathematical Sciences (ICMAT) in Spain. The two had demonstrated singularity formation using "rough forcing," but Buckmaster and Alpöge, by leveraging large language models (LLMs), succeeded in refining the forcing into a smooth function and extending the result to the three-dimensional Euler equations.
According to a personal statement Buckmaster published, their effort was an independent collaboration conducted outside of their employers or affiliated institutions, using Anthropic's Claude and OpenAI's Codex (GPT-5.6 Sol, later Astra). Astra's use was reportedly limited mainly to assisting with paper writing and auditing. They also reportedly obtained a solution for blowup in a "hypodissipative Navier-Stokes equation" with weaker-than-standard viscosity, but held off on publishing it because the Lean formalization had not been completed and a presentable draft paper was not yet finished.
The timeline is tense. On September 3, Buckmaster sent a personal email to an OpenAI mathematics researcher. Subsequently, in discussions on September 6 with OpenAI staff including Bubeck, he says he was told that OpenAI's internal model had generated a roughly 100-page proof showing Navier-Stokes blowup under smooth forcing in both and (Fefferman's Statements C and D).
According to Buckmaster's statement, OpenAI initially explained that "there was little human intervention," but as he pressed for details, he began to have doubts about the consistency of that explanation. He also says OpenAI proposed a simultaneous announcement or sole authorship credit, which he declined. In his statement, Buckmaster chooses his words carefully:
"I have not seen OpenAI's proof. I do not know what their model did or how it worked. Nor do I know whether our data was used. I am not accusing anyone of anything."
OpenAI, for its part, has explained the sequence of events in its blog post and at a press briefing. The company says it began the project on September 1 after hearing rumors that "a Millennium Problem had apparently been solved," and that once Lean verification was completed on September 6, it inferred that the other party had also solved Navier-Stokes and proposed a joint announcement. It was only during that discussion, OpenAI says, that it learned Buckmaster and Alpöge's result concerned the forced Euler equations rather than Navier-Stokes.
OpenAI denies that its researchers or agents had any access to the other party's draft or proof prior to publication, and denies accessing any specific user data. However, it did not fully rule out the possibility that anonymized data from product usage contributed to improving the model's performance. Furthermore, the company counters that its own Euler equations result concerned the "no forcing" case, and that the structure and target theorem of its proof are fundamentally different from Buckmaster and Alpöge's "with smooth forcing" case. At the press briefing, Bubeck denied ever using the other party's prompts or proof to guide the model, and Mark Chen also denied accessing data from work still in progress.
Buckmaster compared the entire episode to the 1997 "Deep Blue vs. Garry Kasparov moment," when the reigning world chess champion was defeated by a computer. At the same time, he acknowledged issues with the writing quality of the Euler equations preprint he published, admitting that it contained rough AI-generated passages he self-deprecatingly called "AI slop." He has called on the mathematics community to begin a deliberate, unhurried discussion about model training data, attribution of credit, peer review systems, and the priorities of mathematics as a discipline.
The Gap Between Formal Certainty and Human "Understanding"
What position do the proof PDF and Lean code published by OpenAI occupy in establishing mathematical truth? What matters here is the logical boundary of what a formal proof assistant like Lean does and does not guarantee.
What Lean verification guarantees is syntactic and deductive correctness — that is, whether the stated theorem is logically derived based on the defined axioms and inference rules. However, Lean itself cannot judge whether the formalized statement strictly matches the physical and mathematical requirements of the Navier-Stokes problem as specified by Fefferman. If there is even a slight discrepancy or an unnatural assumption in the decay conditions of the initial data, the definition of forcing smoothness, or the function space to which the solution belongs, then even if the Lean code compiles successfully, it would not constitute a true solution to the Millennium Problem.
Fields Medal laureate Terence Tao of UCLA, in a blog post on September 7, 2026, praised Buckmaster and Alpöge's result as "a breakthrough across three simplified models — IPM, 2D Boussinesq, and 3D Euler" — while pointing out that they themselves had not reached blowup for the Navier-Stokes equations proper.
Tao stated that he did not see any decisive obstacle in principle preventing an extension of these techniques to Navier-Stokes, and that he could not rule out the possibility that the forcing term might eventually be removed altogether — but he argued that enormous technical difficulties still remain. Tao further emphasized that the primary value of such mathematical research lies not simply in the fact that "a problem has been solved," but in the digestible mathematical insight underlying the method of solution that humans can absorb. His stance is that a solution lacking a deep structural understanding does not carry the intrinsic importance to mathematics that the general media's excitement might suggest.
On September 5, just before the announcement, Tao had also posted on social media that he was not aware of any notable progress on Navier-Stokes, warning that even if an autonomous AI were to fully solve the problem, if the search process remained a black box, its value to mathematics would be "close to zero."
| Comparison item | OpenAI announcement (September 8, 2026) | Alpöge & Buckmaster preprint | Clay Institute (Fefferman formulation) | Independent third-party verification status |
|---|---|---|---|---|
| Target equation | 3D incompressible Navier-Stokes equations | IPM, 2D Boussinesq, 3D Euler (hypodissipative NS unpublished) | 3D incompressible Navier-Stokes equations | Alpöge et al.'s Euler result is being checked by mathematicians; OpenAI's NS result is unverified |
| Treatment of forcing term | Smooth forcing present (Statements C and D) | Smooth forcing present | Statements A/B have zero forcing; C/D allow smooth forcing | Scrutiny needed as to whether OpenAI's construction satisfies Fefferman's decay conditions |
| Form of proof | PDF published on company site plus Lean formalization code | arXiv preprint plus Lean formalization code | Publication in a peer-reviewed journal plus 2 years of community scrutiny | No official approval or review report exists from the Clay Institute |
| Degree of AI involvement | Automatic derivation by a fleet of roughly 10,000 autonomous agents | Human mathematicians led the work, using LLMs to assist writing and partial derivations | Not specified (human comprehensibility is effectively a premise) | A gap remains between machine-checkable formalization and human conceptual grasp |
According to a report by the Dutch technology outlet The Next Web, immediately after the announcement, Buckmaster and colleagues had already published their paper along with machine-verifiable Lean code, whereas OpenAI had not made the details of its paper publicly available at the time of the press announcement. A link to the paper's PDF and its Lean formalization was subsequently added to OpenAI's official index page, but peer review and independent verification by the mathematics community have only just begun.
Naturally, there is at present no fact of the Clay Mathematics Institute having approved this proof or certified the Millennium Prize Problem as solved. Under the prize's award rules, a paper must be published in a high-standard peer-reviewed mathematics journal and must then withstand two years of broad scrutiny by the mathematics community as a mandatory condition.
What the Unsolved Equation Asks About the Contours of Intelligence
What this announcement raises is a dual challenge: the physical interpretation of fluid dynamics, and the evaluation of scientific discovery made by AI.
First, there is the matter of what this means for the physical description of fluids. OpenAI's construction here is an existence proof that drives a mathematical system of equations toward a singularity by continuously applying a specifically and cleverly designed smooth forcing. As David Silvester of the University of Manchester commented to New Scientist, both Buckmaster and colleagues' result and this latest attempt are an "important stepping stone" toward a full resolution, but the question of greatest engineering interest — whether, in an isolated system with no forcing, turbulence arises spontaneously from natural flow and a singularity spontaneously forms (Statements A and B) — remains untouched. The Navier-Stokes calculations used in aircraft design and daily weather forecasting are not going to break down tomorrow.
Second, there is the matter of transparency in evaluating AI model capability. The performance, benchmark results, and scale of computational resources deployed that OpenAI has reported for its "unnamed internal model" are, at this point, entirely based on the company's own unilateral claims, and cannot be reproduced by independent outside researchers under the same conditions.
The points to watch going forward are clear. Does the published Lean code faithfully reproduce every one of the axiomatic conditions in Fefferman's formulation of Statements C and D, without omission? And can mathematicians read through the logical development of the generated proof and digest it as a new mathematical tool or concept?
Whether true physical insight exists beyond the flow velocity said to diverge to infinity at the singularity, or whether what lies there is instead a sprawling logical labyrinth produced by brute-force computational search, is a judgment that will be entrusted not to an algorithm, but to the rigorous reading yet to be done by flesh-and-blood mathematicians.