marcel blattner | september 26
Introduction
On September 8, 2026, OpenAI published a 166-page paper and a Lean formalization stating that the three-dimensional incompressible Navier-Stokes equations can develop a singularity in finite time. According to the company, a group of roughly 10,000 coordinating agents, running an internal model still in training, produced the proof about 88 hours after the first agents were launched. Coverage and discussion that followed often compressed the event into the statement that OpenAI solved the Navier-Stokes equations.
That statement describes a different activity from the one OpenAI reports. The company addressed the Navier-Stokes existence and smoothness problem, one of the seven Millennium Prize Problems of the Clay Mathematics Institute, which asks a qualitative question about solutions of the equations. OpenAI's paper presents a proof in the breakdown direction, for the formulation that permits an external force. This post separates four objects that the headline merges: the equations, the mathematical problem, the formal statement of the problem, and the machine-checked encoding of the proof. It then relates the case to the argument of an earlier post on this blog, https://www.tangential.ch/blog/other-planets-of-intelligence-what-ai-in-mathematics-indicates-for-other-fields
Two meanings of solving
The Navier-Stokes equations apply Newton's second law to a fluid treated as a continuous medium. For a velocity field u, pressure p, viscosity ν and external force f, they read
∂u/∂t + (u·∇)u = −∇p + νΔu + f, with ∇·u = 0.
The left side is the acceleration of a fluid parcel, the right side collects the pressure gradient, internal friction and the applied force, and the second equation expresses incompressibility.
In engineering, solving these equations means computing an approximate flow for a given geometry, initial state and forcing. Aircraft design, weather forecasting and the study of blood flow rely on such computations, which numerical methods have delivered for decades. Each computation produces one flow for one situation.
In mathematical analysis, the equations raise a question of another kind: whether a flow that starts smooth and with finite energy stays smooth for all time, or whether its velocity can become unbounded within a finite time. Such an event is called a singularity, or blowup. In 1934, Jean Leray proved that solutions exist in a weak, generalized sense; whether they remain smooth has been open since. The question concerns the mathematical model. Real fluids consist of molecules, and the equations describe them at scales far above the molecular, so a singularity marks the point where the continuum description stops applying. The existence and smoothness problem belongs to this second meaning of solving.
The Problem as Clay Posed It
The official problem statement, written by Charles Fefferman, fixes the setting precisely. Initial velocities must be smooth and decay rapidly at infinity, forces must be smooth and decay in space and time, and an acceptable solution must stay smooth for all time with bounded kinetic energy. Fefferman then lists four statements and asks for a proof of any one of them, a design meant to give solvers leeway while "retaining the heart of the problem."
Statements A and B assert global regularity: with the external force set to zero, every admissible initial velocity leads to a solution that stays smooth for all time, in the whole of three-dimensional space (A) or on a periodic domain (B). Statements C and D assert breakdown: some admissible initial velocity together with some admissible smooth force leads to no such solution, in the whole space (C) or on the periodic domain (D).
The two pairs differ in their assumptions as well as their conclusions. A and B concern the unforced equations; C and D let the solver choose the force. A proof of C with a nonzero force leaves A undecided, and the two statements can hold simultaneously. The Millennium Prize Problem can therefore be resolved through C or D while the question whether a fluid without external driving can develop a singularity stays open.
What Construction Shows
The main theorem of OpenAI's paper states that for every positive viscosity there exist a smooth force, compactly supported in space and time, and a flow that starts from rest, stays inside a fixed bounded region, keeps its kinetic energy bounded, and reaches unbounded speeds as time approaches 1. With this force and zero initial velocity, no smooth solution with bounded energy exists for all time. The paper identifies this with statement C and derives D from the compact support.
The flow is a vortex. Fluid spirals inward toward an axis and leaves along it, and the core contracts into a slender column at the origin. With τ denoting the time remaining before the singularity, the core radius scales as τ^(1/2), its height as τ^(1/2 − h), and its typical speed as τ^(−1/2 − h), for a fixed exponent h between 0 and 1/100. The kinetic energy of the core scales as τ^(1/2 − 3h) and tends to zero while the speeds diverge.
The paper names the central difficulty. For any incompressible flow, a force can be defined as the residual of the equation, and the equations then hold by construction. The task is to find a flow that blows up while this residual, with all its derivatives, stays smooth through the singular time. The construction achieves this with oscillatory pulses, seeded by an exponentially small force and amplified by the shear of the vortex, whose averaged momentum flux cancels the part of the residual that would otherwise diverge.
The singular flow is designed first, and the force is the smooth input the equations require to sustain it. The theorem therefore states that the equations, as a mathematical system, admit breakdown from smooth data under a smooth force. Statements A and B ask what the equations do without any force, and they remain open.
The construction extends a line of work. Diego Córdoba and Luis Martínez-Zoroa developed the strategy of amplifying successively finer vortex layers and obtained singularities for the forced Euler equations, the frictionless limit of Navier-Stokes, with forces that lacked the smoothness required in the Clay formulation. On September 7, Tristan Buckmaster of New York University and Levent Alpöge released AI-assisted, Lean-formalized blowup results with smooth forcing for the Euler equations and two related model equations. That day, Terence Tao wrote that a smooth-force construction for Navier-Stokes was now widely expected, and that one without the forcing term should also be possible. Alongside its Navier-Stokes paper, OpenAI released a separate paper presenting blowup for the unforced Euler equations, which are absent from the Clay list. Fefferman told Quanta Magazine that he was thrilled the problem was solved and named Córdoba and Martínez-Zoroa as the heroes of the story.
What the Certificate Covers
According to OpenAI, GPT-6 Astra produced the Lean formalization in about 17 hours. The repository is public and includes instructions for independent checking. A successful check establishes that the formal theorem follows from the axioms of Lean and the definitions of its mathematics library. Whether that formal theorem matches statement C, with its smoothness classes, decay conditions and energy bound, is a separate question, and Quanta Magazine identifies this equivalence as the part of verification that humans still have to carry out.
Other Planets of Intelligence described this gap with an example from Klowden and Tao: a formally certified "disproof" of Fermat's last theorem results when the natural numbers in the formal statement include zero. The verifier certifies the formal statement, not the intended one. A later post, https://www.tangential.ch/blog/the-machine-that-checks-what-lean-is-how-it-works-and-what-it-finds-in-a-tangential-action-space, described the complementary property: Lean's small kernel makes the origin of a proof irrelevant to its acceptance. Both properties apply here. The certificate establishes the encoded theorem regardless of who or what wrote it, and the match between encoding and problem is left to specialists.
Institutional acceptance follows separate rules. The Clay Mathematics Institute accepts no direct submissions and considers a proposed solution only after publication in a qualifying outlet, a waiting period of at least two years, and general acceptance in the mathematics community. OpenAI has stated that it does not intend to claim the prize. As of this writing, the result is a public, machine-formalized, proposed resolution of the forced formulation. "Tackled" describes that status. "Resolved" will describe it once the community accepts the proof. "Solved the Navier-Stokes equation" describes a different activity at every stage.
The Distance between Headline and Theorem
Between the sentence "OpenAI solved Navier-Stokes" and an object that can be checked lie four layers of translation. The first layer is physical: whether real fluids develop unbounded velocities. The second is mathematical: whether the continuum equations, started from smooth data, can lose smoothness. The third is Fefferman's formal statement, which fixes function classes and admits a smooth external force in its breakdown alternatives. The fourth is the Lean encoding. Each translation narrows the claim, and at each one the checked object and the intended question can separate.
Verification strength runs in the opposite direction. The fourth layer has machine checking. The third has Clay's procedure of publication, delay and community acceptance. The second rests on expert judgment about whether the forced formulation captures the substance of the question. The first lies outside the equations, which describe fluids only above molecular scales. The headline sits above all four layers, where no verifier operates, and borrows its credibility from the certificate attached to the lowest one.
The earlier post ordered fields along a verification gradient, by how independently their outputs can be checked, and observed that every verifier checks a proxy. The Navier-Stokes case displays the same gradient inside a single claim: the formulations that circulate most widely are the ones furthest from any verifier.
Provenance Has No Verifier
The announcement also started a dispute about origin. OpenAI states that its effort began on September 1 after its researchers heard rumors that two Millennium Prize Problems had been resolved, rumors it later traced to Buckmaster and Alpöge. The company recognizes their priority for the forced Euler result and claims the Navier-Stokes result. It states that neither its researchers nor its agents saw their work before its public release, and that it cannot rule out that de-identified data from their use of OpenAI products helped improve its models. According to Quanta Magazine, Buckmaster's statement suggests that OpenAI's researchers or agents may have had access to, and benefited from, the work he and Alpöge did with OpenAI's models, and the parties give different accounts of their interactions.
This dispute lies outside what formal verification checks. The property that makes Lean trustworthy, its indifference to the origin of a proof, also makes it silent about origin. Mathematics has strong machinery for deciding whether a result is correct and relies on publication records and professional norms for deciding who produced it. When researchers work with tools supplied by the same companies whose systems compete with them, the second decision depends on records of training data, data access and chronology that are not public.
A Finale Perspective
In his September 7 post, written before OpenAI's announcement, Tao described solving such problems as "only a proxy goal" for the primary goal of mathematical understanding, and wrote that without that understanding even the Navier-Stokes problem carries far less intrinsic significance than popular media sometimes suggest. The same post reports that Buckmaster and Alpöge spent the preceding weeks rewriting their AI-generated proofs toward a readable form, work still in progress; Buckmaster had described the first model-generated proof he received as the worst he had ever read. Other Planets of Intelligence cited Thurston's observation that a proof creates understanding in its author and its readers. In this case the proof came first, and the understanding of why the construction works is produced afterwards, by people reading, rewriting and simplifying it.
In a comment on September 9, Tao wrote that the use of AI without sufficient verification, the initial focus of his warnings and a major concern from 2023 to 2025, is no longer the main source of harm in 2026. He described the Navier-Stokes events as the most visible instance of an industry race toward autonomous AI that, in his view, disregards its value to society, and called on mathematicians to reject uses of AI that serve nominal goals over the field's underlying ones. The case gives that distinction a concrete form. A nominal goal, a Millennium Prize Problem in one of its admissible formulations, now has a machine-formalized candidate resolution. The underlying goals, an understanding of why the construction works and a settled account of who contributed what, are still to be reached.
A sentence matched to the evidence is narrower than the headline. An AI system produced a machine-formalized construction that, if the mathematical community accepts it, resolves the Navier-Stokes existence and smoothness problem through its forced breakdown formulation. Engineers solve the equations numerically as before, and whether a fluid without external driving can develop a singularity remains open.
Further Reading
Image
Credits: Image by Marcel Blattner, August 26