On 8 September 2026, OpenAI announced an AI-generated solution to the existence and smoothness problem for the Navier–Stokes equations. Those equations describe the motion of incompressible fluids—air, water, blood—as a continuous medium, not molecule by molecule. The package includes an analytical writeup and a Lean formalization.
Two names in the announcement need translation. The Clay Mathematics Institute is the body that, in 2000, listed seven Millennium Prize Problems—central open questions in mathematics, each carrying a one-million-dollar prize. Navier–Stokes is one of them. The official statement of that item was written by Charles Fefferman. The announcement says the construction establishes alternatives “C” and “D” in that text—and, in the same breath, that the company does not intend to claim the Millennium Prize.
Those two sentences belong together. A machine-checkable proof of breakdown—fluid speed growing without bound in finite time—with a smooth force and bounded energy closes a precise statement. It does not, by itself, close the dispute over priority, over what the community treats as “the” Navier–Stokes problem, or over institutional acceptance of a prize claim.
What Clay actually asks for
Fefferman’s official note, Existence and Smoothness of the Navier–Stokes Equation, offers four alternatives. (A) and (B) ask for global existence and smoothness with the external force identically zero, on Euclidean space and on the periodic torus. (C) and (D) ask for breakdown: there exist smooth initial data and a smooth force—under the decay or periodicity conditions in the statement—for which no smooth, bounded-energy solutions exist on the whole interval ([0,\infty)).
That is a textual fact, not a charitable reading: (C) and (D) allow a smooth external force. Those who insist that “the real problem” is unforced regularity are stating a historical and physical preference—unforced regularity—not correcting a misreading of Clay’s PDF. Mixing the two impoverishes the argument.
What Theorem 1.1 constructs
The paper Finite Time Blowup for Navier–Stokes (OpenAI) states, in Theorem 1.1, that for every viscosity (\nu > 0) there exist a force (f \in C_c^\infty(\mathbb{R}^3\times(0,\infty))), a compact set (K), and smooth fields (u,p) on (\mathbb{R}^3\times[0,1)) satisfying the Navier–Stokes equations, starting from rest, supported in (K), with (L^2) energy uniformly bounded, yet (\limsup_{t\uparrow 1}|u|_\infty=\infty). Hence there is no smooth solution on ([0,\infty)) with the same force and initial datum and uniformly bounded energy.
The paper itself ties this to Fefferman’s alternative (C); compact support, via Corollary 10.6, yields the corresponding construction on (\mathbb{T}^3) and thus (D). OpenAI’s announcement states the same conclusion: a finite-time singularity with a smooth force and finite energy, establishing “C” and also “D”.
The mechanism described in the paper and the announcement is a self-similar vortex: inward spiral, axial stretch, an ever-slenderer “spaghetti” core. The technical challenge is not to insert an infinite force by hand; it is to make the equation’s terms—acceleration, pressure, transport, viscosity—become large and cancel so that the residual (the force) stays smooth while velocity becomes unbounded.
That is what formalizable mathematics can close: the (C)/(D) statement with force.
What Lean closes—and what it does not
Lean is a proof assistant: a system in which theorems and proofs are written in a formal language and checked by a small, trusted kernel. If checking succeeds, the machine has accepted the logical chain of what was written—whether a human or an agent produced the text. The public repository openai/NavierStokesAndEuler is the artifact to inspect in that sense.
OpenAI describes an internal model “significantly more capable” than GPT‑6 Astra—the company’s frontier workhorse for computer use and long tasks—in training since about 28 August 2026; a multiagent system; the Navier–Stokes group on the order of 10,000 concurrent agents; safeguards, monitoring, and isolation as in the company’s frontier evaluations. Separate agent groups were prompted with A/B (regularity) and C/D (breakdown). Earlier, the system resolved unforced Euler regularity—the zero-viscosity limit of Navier–Stokes, another classic blowup question, but off Clay’s prize list (~100 agents, ~50 h). For Navier–Stokes, agents reached a resolution about 88 h after launch (Saturday, 5 September); Lean formalization and verification took about 17 additional hours via GPT‑6 Astra. Reported totals: ~4.9 million messages and ~300 billion output tokens across all attempted problems; ~2.7 million and ~130 billion for Navier–Stokes alone.
If the Lean formalization is correct, what it delivers is machine-checkable mathematics: the (C)/(D) statement is closed as a formal object. Elsewhere I have argued that AI needs a checker and that agents write the code, not the proof. Here the verifier is Lean. That is progress in evidence, not in press-release tone.
What Lean does not decide:
-
Priority. The announcement situates the effort from 1 September, inspired by rumors later tied to Levent Alpöge (Anthropic) and Tristan Buckmaster (NYU). After Lean verification (6 September), OpenAI offered a concurrent release; learned they had forced Euler; states it did not see that work until public release; and recognizes their priority on forced Euler, noting that the proofs differ (forced versus unforced already in the Euler case). That is OpenAI’s account. It is not a priority verdict issued by the Lean kernel.
-
What the community calls “the” problem. Much of the analytic culture treats unforced regularity—alternatives (A)/(B), or the analogous force-free question—as the heart of the matter. Preferring (A)/(B) is a legitimate scientific judgment. It does not authorize saying OpenAI “missed Clay’s statement” by targeting (C)/(D).
-
Prize acceptance. OpenAI says it does not intend to claim the Millennium Prize and frames the post as a progress report—“not a culmination,” a snapshot of the pace of AI. Clay evaluation, when it happens, takes time; inventing a rejection or an endorsement the Institute has not published would be fabricated journalism. What is documented is: a formalized (C)/(D) proof; a company that does not claim the prize; an open dispute over the cultural weight of “solving Navier–Stokes” with force.
Limits the announcement already makes visible
The result does not resolve (A) or (B). It does not claim unforced regularity. The unforced Euler result the agents found, per the announcement, is also not on Clay’s prize list—Fefferman himself notes that Euler is important and open, but off the prize list. The internal model remains unreleased; agent counts, hours, and tokens are self-reported. Lean closes the formal chain of what was written; it does not, by itself, audit the provenance of every intermediate insight in the swarm—the same tension that appears when AI gets more aligned and harder to audit or when auditable control of action trajectories becomes the scarce resource.
How to read a claim of this kind
For readers who evaluate AI claims, the useful criterion is not the page title. It is the map statement → artifact → verification → remainder.
- Fact: Clay’s PDF formulates (C)/(D) with a smooth force allowed; Theorem 1.1 and the announcement claim to establish exactly that; a writeup and a public Lean repository exist.
- Cautious inference: if the formalization is correct, the mathematics of (C)/(D) is no longer open in the formal sense of the chosen statement.
- Hypothesis / open dispute: whether “solving Navier–Stokes” in public conversation means unforced regularity; who holds priority on which variant; what Clay would do with a prize claim that OpenAI itself says it will not make.
The complex harness already showed that a short ranking does not replace a flow exam. Here the flow exam is different: read Fefferman, read the theorem, open the Lean, separate what was formalized from what the headline sells.
Formalization can close the statement. The dispute—priority, the name of the problem, the prize—remains human work, public evidence, and institutional time. Ideas under construction; evidence in public.