OpenAI Publishes AI-Generated Navier–Stokes Blowup Proof

OpenAI has published a 166-page proof claiming to resolve the Navier–Stokes existence and smoothness Millennium Prize Problem by constructing a three-dimensional fluid flow that develops unbounded velocity in finite time.

The company released both a conventional mathematical paper and a formalization written in Lean, a proof assistant that checks whether each step follows from explicitly stated definitions and assumptions. OpenAI says the proof was generated by approximately 10,000 concurrent agents using an unreleased internal model “significantly more capable” than GPT-6 Astra.

The result has not yet been accepted by the Clay Mathematics Institute or validated through the review process required for a Millennium Prize. As of September 9, it should therefore be described as a published proposed solution, not an officially settled theorem.

1. What the proposed proof establishes

The Navier–Stokes equations describe the motion of viscous fluids such as air and water. In three dimensions, mathematicians have long been unable to prove whether smooth starting conditions must produce smooth solutions for all future times, or whether a singularity can form.

OpenAI’s paper takes the second route. Its principal theorem states that, for every positive viscosity, there is a smooth external force and a solution that begins with zero velocity but becomes unbounded at time \(t=1\). The flow remains spatially confined to a fixed compact region, and its total kinetic energy stays uniformly bounded as the singularity approaches.

This is a stronger and more specific statement than saying a computer simulation became unstable. The paper claims an analytical construction in which the fluid’s maximum speed diverges even though the initial state, applied force and pre-singularity evolution are smooth.

The use of an external force is important. The Clay Mathematics Institute’s official formulation provides four acceptable routes to resolving the problem. Alternatives A and B ask for global smoothness without forcing, respectively in ordinary three-dimensional space and on a periodic domain. Alternatives C and D allow a smooth force and ask for a counterexample in those two settings.

OpenAI claims to establish alternative C in \(\mathbb{R}^3\). Because the constructed velocity and pressure have compact spatial support, the paper says the same construction also produces the periodic counterexample required by alternative D.

The result therefore does not claim that every ordinary fluid flow becomes singular, nor does it provide a closed-form solution for arbitrary turbulence. It constructs particular smooth forces and flows showing that the mathematical model can break down under conditions explicitly permitted by the prize statement.

2. How the finite-time singularity is constructed

The central object in the proof is an axisymmetric vortex that contracts around the origin while rotating and stretching along its axis. As the singular time approaches, fluid spirals inward and its angular and axial velocities increase.

Writing the remaining time as \(\tau=1-t\), the paper gives the vortex core a radial scale proportional to approximately \(\tau^{1/2}\) and a slightly more slowly contracting axial scale. Its characteristic angular and axial speeds grow approximately as \(\tau^{-1/2-h}\), where \(h\) is a small positive parameter below \(1/100\).

The increasingly fast motion is confined to an increasingly small volume. According to the construction, the core’s kinetic energy scales as \(\tau^{1/2-3h}\), which approaches zero for the permitted values of \(h\). That separation between maximum velocity and total energy is how the proof produces unbounded speed without violating the bounded-energy condition in the Clay formulation.

Creating a shrinking vortex is not sufficient on its own. For an arbitrary velocity and pressure field, one could simply define an external force that makes the Navier–Stokes equation hold, but that force might itself diverge at the singular time. Such a construction would not satisfy the problem’s smooth-forcing requirement.

OpenAI’s proposed solution addresses this with localized oscillatory pulses in an annular region surrounding the vortex core. The pulses extract energy from the background shear and generate nonlinear momentum fluxes. Two families of pulses are arranged so that their averaged effects cancel the singular part of the force that the contracting background vortex would otherwise require.

Additional corrections reduce the remaining errors, while an exterior flow governed by viscous diffusion permits the construction to be cut off smoothly in space. The claimed end result is a velocity field that diverges while the residual appearing as the external force extends smoothly through the singular time.

3. A 10,000-agent research process

OpenAI says it began training the unnamed internal model on August 28, 2026. On September 1, after hearing rumors of progress on two Millennium Prize problems, researchers assigned groups of agents to all unresolved problems in the Clay collection and several related questions.

The agents could read a cached version of the internet, execute code and exchange information within groups. Separate groups received different versions of the Navier–Stokes challenge, including both the global-smoothness and finite-time-breakdown alternatives.

An intermediate result reportedly changed the direction of the search. Nearly 100 agents worked for about 50 hours on the regularity problem for the unforced Euler equations, which describe an idealized fluid with no viscosity. After those agents produced a proposed finite-time blowup construction, OpenAI redirected more resources toward the viscous Navier–Stokes problem and supplied the Euler result to the new groups.

OpenAI also used Codex to consolidate useful intermediate findings and circulate them across groups. The company says the successful Navier–Stokes construction emerged on September 5, approximately 88 hours after the first agents were started.

The Navier–Stokes effort generated 2.7 million agent messages and about 130 billion output tokens. Across all of the mathematical problems attempted during the project, the systems generated 4.9 million messages and approximately 300 billion output tokens. OpenAI executives separately told Axios that the computing cost was in the millions of dollars.

The generation model has not been released, making the experiment impossible for outside researchers to reproduce directly. GPT-6 Astra was used for the later formalization and verification stage, which OpenAI says required another 17 hours; it was not the model that originally found the proof.

4. What the Lean formalization does—and does not—settle

OpenAI has released the Lean 4 source code under an Apache 2.0 licence. The repository contains formalizations for both the Navier–Stokes and Euler results and provides build instructions using Lean 4.34.0-rc2, Mathlib and Lake.

A machine-checked proof materially strengthens the submission because Lean requires the formal argument to type-check against a precise statement. It can detect missing logical steps that might be obscured in a long natural-language derivation, and other researchers can download and rebuild the public files.

Formal verification does not by itself establish that the formal theorem captures every condition intended by the Millennium Prize formulation. Specialists still need to inspect the definitions, assumptions, imported results and correspondence between the 166-page analytical argument and the Lean statement. Independent experts must also assess whether the mathematical construction behaves as claimed.

The Clay Mathematics Institute does not accept proposed solutions through direct submission. Under its rules, a solution must first appear in a qualifying publication, at least two years must pass, and the result must gain general acceptance in the global mathematics community before the institute will consider it.

OpenAI says it does not intend to claim the $1 million prize. That decision does not shorten the validation process or convert the company’s announcement into institutional recognition.

5. Concurrent research and unresolved provenance questions

OpenAI says the rumor that prompted its September 1 effort was later connected to NYU professor Tristan Buckmaster and Anthropic researcher Levent Alpöge. Their concurrent work concerned finite-time blowup for the forced Euler equations and related fluid systems, rather than the viscous Navier–Stokes result released by OpenAI.

According to OpenAI, its Navier–Stokes proof and Lean verification were completed on September 6. The company then contacted Buckmaster and Alpöge because it believed they might also have solved Navier–Stokes, and proposed coordinating publication while recognizing their priority. OpenAI says it subsequently learned that their result addressed forced Euler instead.

Buckmaster publicly questioned whether knowledge of the outside project caused OpenAI to race toward the same broader research direction and raised concerns because drafts had been processed through Codex. OpenAI says neither its researchers nor its agents accessed the pair’s work before its public release and that the resulting proofs use substantially different approaches.

The company nevertheless states that it cannot completely rule out the possibility that de-identified data derived from their use of OpenAI products had previously contributed to model training. No public evidence currently establishes that the internal model reproduced their drafts, and Buckmaster has not claimed to know whether his data was used.

The episode creates a concrete governance problem for AI-assisted research. Scientists using hosted models for unpublished work must be able to determine whether their inputs are retained, used for training or visible to the provider. When the same provider can deploy much larger agent systems as a competing researcher, technical data controls and auditable provenance become part of scientific credit—not merely product privacy settings.

Frequently Asked Questions

Has the Navier–Stokes Millennium Prize Problem officially been solved?

No. OpenAI has published a proposed solution, but it has not completed the Clay Mathematics Institute’s publication, waiting-period and general-acceptance requirements.

Does the proof show that ordinary water can reach infinite speed?

No. It constructs a specific mathematical flow with a carefully designed smooth external force. Infinite velocity signals a breakdown of the continuum equation, not a prediction that a physical fluid literally accelerates without limit.

Was GPT-6 Astra the model that found the proof?

No. OpenAI attributes the discovery to an unreleased internal model more capable than GPT-6 Astra. Astra was used during the 17-hour Lean formalization and verification stage.

Can researchers inspect the result?

Yes. OpenAI released the 166-page paper and the Lean 4 formalization publicly. The internal model and the full agent infrastructure, however, are not publicly reproducible.

Is the proof about forced or unforced Navier–Stokes equations?

It uses a smooth external force. That is allowed under alternatives C and D of the Clay Mathematics Institute’s official problem statement.

Sources

• Original OpenAI announcement on X
• OpenAI: On the Navier–Stokes Millennium Prize Problem
• OpenAI paper: Finite Time Blowup for Navier–Stokes
• OpenAI’s Navier–Stokes and Euler Lean formalizations
• Clay Mathematics Institute’s official Navier–Stokes problem statement
• Clay Mathematics Institute’s Millennium Prize rules
• The Guardian: OpenAI claims to have solved maths problem that stumped humans for decades
• Axios: OpenAI’s historic math solution overshadowed by credit controversy