News · 2026-09-08

OpenAI says an internal model resolved the Navier-Stokes Millennium Problem

OpenAI said on September 8, 2026 that an internal model produced a proof that the equations governing fluid motion can break down in finite time, resolving one of the seven Millennium Prize Problems. The company published both a written proof and a machine-checked formalization in Lean, and said the work was done by roughly 10,000 AI agents running in parallel for 88 hours. OpenAI also said it does not intend to claim the associated $1 million prize.

Key facts

• The result was reached on Saturday, September 5, about 88 hours after the first agents were launched; Lean verification took a further 17 hours.
• The group that produced it involved on the order of 10,000 concurrent agents, which exchanged 2.7 million messages and used roughly 130 billion output tokens on this problem alone.
• OpenAI says the proof establishes statements "C" (and also "D") of the official Clay Mathematics Institute formulation.
• Primary source: OpenAI's announcement, On the Navier-Stokes Millennium Prize Problem, with the proof PDF and the Lean formalization on GitHub.

The Navier-Stokes equations are Newton's second law written for fluids. They treat water or air as a smooth continuous substance rather than a swarm of molecules, and they underpin aircraft design, weather forecasting and the study of blood flow. The open question, unresolved for roughly ninety years, is whether that smooth description can destroy itself: can a fluid that starts out perfectly well behaved reach infinite speed in a finite amount of time? If it can, the equations stop describing the real world at that instant, and you would have to go back to tracking individual particles.

OpenAI says the answer is yes. In its own description, the solution is "a vortex, a spinning swirl of fluid, that spirals inward and gets increasingly elongated, like spaghetti." The central region shrinks while speeding up, and it does so in a way that keeps the total energy finite, as physics requires. The delicate part is that the competing terms in the equations — acceleration, pressure, momentum transfer, viscosity — must all grow large while cancelling each other precisely, so that the force applied from outside stays smooth even as the fluid's velocity runs away to infinity.

Here is the detail most coverage got wrong. The Clay Institute's official problem, as written by Charles Fefferman, does not demand a single specific answer. It says that "to give reasonable leeway to solvers while retaining the heart of the problem, we ask for a proof of one of the following four statements." Statements (A) and (B) assert that smooth solutions always exist, with no external force. Statements (C) and (D) assert the opposite — that there exists a smooth starting flow and a smooth external force for which no smooth solution survives. Proving (C) or (D) resolves the problem. Several outlets reported that the forced version does not count; the official rules say it does.

How the proof was found is its own story. Since August 28 OpenAI has been training a new internal model, which it describes as "significantly more capable than GPT-6 Astra." On September 1, after hearing rumours that two Millennium problems had been resolved, it pointed a system of coordinating agents at every open Millennium problem at once. The agents could read a cached copy of the internet and run code, and were split into groups that could talk within themselves. Different groups were given different variants of the problem. The agents first cracked an easier warm-up — the analogous blowup question for the Euler equations, with viscosity removed — using nearly 100 agents over about 50 hours. OpenAI then redirected its resources at Navier-Stokes and fed the Euler result back in as a prompt, periodically using Codex to consolidate the most useful insights from each group and cross-pollinate them.

Think of it as a very large research department with no sleep and no ego, where the manager's main job is reading everyone's notes each morning and telling the next shift which three ideas are worth pursuing. Across all the problems it attempted, the system sent 4.9 million messages and burned about 300 billion output tokens.

Why it matters: this is the first time a major lab has claimed a Millennium Prize result and shipped a formal artifact with it. The Lean repository is Apache-2.0 licensed, builds against Mathlib, and includes a directory for independent proof-checking — which means the central claim is, unusually, falsifiable by anyone with a machine and patience. That is a direct response to the pattern this site has documented before, when OpenAI published ten math claims with Lean proofs and no named authors and three days later nobody had publicly compiled them.

The honest caveat is large. Nothing here has been through peer review, no independent mathematician has yet confirmed the Lean build or, more importantly, confirmed that the formalized statement is the theorem people actually care about — a proof assistant will happily certify an airtight proof of the wrong thing. The written proof runs to roughly a hundred pages. And the announcement arrived in the middle of a public dispute over credit with the mathematicians working the same route, which is why OpenAI's post carries a section titled "Concurrent work" at all.

Primary source, verified: read the paper →

Ground Truth. (2026, September 8). OpenAI says an internal model resolved the Navier-Stokes Millennium Problem. Ground Truth. https://groundtruth.day/news/openai-says-an-internal-model-resolved-the-navier-stokes-millennium-problem.html

@misc{groundtruth:openai-says-an-internal-model-resolved-the-navier-stokes-millennium-problem,
  title  = {OpenAI says an internal model resolved the Navier-Stokes Millennium Problem},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {sep},
  url    = {https://groundtruth.day/news/openai-says-an-internal-model-resolved-the-navier-stokes-millennium-problem.html}
}

Topics: openai · mathematics · ai-agents · millennium-prize · formal-verification · lean