OpenAI announced on September 8, 2026 that an internal AI system produced a proof, accompanied by a formalization in the Lean proof assistant, that the Navier–Stokes equations governing fluid motion can develop a singularity in finite time. The company said the result resolves one of the Clay Mathematics Institute’s Millennium Prize Problems.
What the Proof Establishes
OpenAI shared both a writeup of the proof and its Lean formalization. According to the announcement, the proof shows that an initially smooth fluid at rest, with a smooth force applied to it and its energy remaining finite through the entire dynamics, develops a singularity within a finite amount of time. Versions “A” and “B” of the official problem formulation would yield a proof, while versions “C” and “D” would yield a disproof; OpenAI said its system established “C” and also “D,” resolving the problem.
The solution is a vortex, a spinning swirl of fluid that spirals inward and grows increasingly elongated. Its central region shrinks while speeding up in such a way that its energy stays finite. The technical challenge, OpenAI said, was for the breakdown to arise from the fluid’s own motion rather than an imposed infinite force: the terms describing acceleration, pressure gradients, momentum transfer, and viscosity must grow large yet cancel precisely, leaving a smooth external force even as the fluid’s velocity grows without bound.
OpenAI framed the release as a report on the progress of its AI models and said it does not intend to claim the Millennium Prize for the result.
The Problem’s History
The Navier–Stokes equations apply Newton’s second law of motion to a fluid treated as a continuous medium rather than a collection of individual molecules, and they are used in aircraft design, weather forecasting, and the study of blood flow. A singularity means fluid speeds growing without bound within a finite amount of time, behavior a real fluid cannot exhibit. Its development despite viscosity, which tends to smooth out motion, would mark a breakdown of the continuum model, and the longstanding open question has been whether that breakdown can occur in a three-dimensional incompressible fluid whose motion starts smoothly.
The equations date to nineteenth-century work by Claude-Louis Navier and George Gabriel Stokes. In 1934, Jean Leray proved that solutions exist in a generalized sense, but whether they always remain smooth went unanswered. The Clay Mathematics Institute named Navier–Stokes one of seven Millennium Prize Problems in 2000; the prizes were announced on May 24, 2000, at the Collège de France in Paris, and CMI’s Board of Directors designated a $7 million prize fund with $1 million allocated to each problem. CMI’s problem page lists Navier–Stokes as unsolved, noting there is no proof for the most basic questions of whether solutions exist and are unique. The Poincaré Conjecture stands as the only solved problem among the seven.
The Agent System Behind the Proof
OpenAI said it has been training a new internal model since August 28, 2026, describing it as significantly more capable than GPT-6 Astra, with what it called unprecedented performance in its benchmarks, including mathematics; the model’s training is ongoing. On September 1, 2026, after hearing rumors that two Millennium Prize problems had been resolved, the company launched an effort to evaluate the model on all open Millennium Prize problems and a few other high-impact problems.
The effort used a system of coordinating agents powered by the internal model, with access to a cached version of the internet and the ability to run code, subdivided into groups that could communicate within each group. The group that produced the Navier–Stokes resolution involved on the order of 10,000 concurrent agents, operating under the monitoring and isolation safeguards OpenAI said it applies to all of its frontier model evaluations.
As a preliminary, agents resolved the regularity problem for the Euler equations, the limit of Navier–Stokes with the viscosity term removed, in the unforced variant where no external force is applied. Nearly 100 agents worked approximately 50 hours on that disproof, a result OpenAI said surprised it. The company then shifted agents to Navier–Stokes, prompted them with the Euler resolution, updated them to a further-trained version of the model mid-effort, and used Codex to consolidate the most useful insights across groups.
The agents arrived at the Navier–Stokes resolution on September 5, 2026, about 88 hours after the first agents were launched; Lean formalization and verification took an additional 17 hours via GPT-6 Astra. Across all attempted problems, the agents sent 4.9 million messages and used about 300 billion output tokens; the Navier–Stokes work accounted for 2.7 million messages and approximately 130 billion output tokens.
Concurrent Work and OpenAI’s Account
The announcement also addresses the circumstances around the effort. OpenAI said its project began September 1 after a rumor it later connected to Levent Alpöge, an Anthropic employee, and Tristan Buckmaster, a mathematics professor at NYU. After completing its project and Lean verification on September 6, 2026, believing from the rumor that the pair also had a Navier–Stokes solution, OpenAI said it reached out to offer a concurrent release of its result and to recognize their priority in a joint announcement, at which point it learned they had a resolution of the forced Euler problem. OpenAI said it offered the pair visibility into all of the prompts it used and, later, the proof itself, and that it recognizes the priority of their forced Euler work.
On data use, OpenAI stated that its researchers and agents did not see any of the pair’s work through any means until it was released publicly, and that no specific user data was accessed in order to solve the problem. The company added that it cannot rule out that de-identified data derived from the pair’s usage of its products helped improve its models, while noting that the proofs differ significantly, including the precise results proved in the Euler case: forced versus unforced.
On September 7, 2026, Buckmaster publicly announced three results with Alpöge: finite-time blowup with smooth forcing for incompressible porous media, for Boussinesq, and for three-dimensional incompressible Euler, posting the papers and a Lean formalization. In an accompanying statement, he described nearly a year of personal collaboration using Anthropic’s Claude and OpenAI’s Codex, an August 15, 2026 breakthrough, and an August 22, 2026 Lean verification, and recounted a September 3, 2026 email to an OpenAI mathematician and September 6 calls in which, he wrote, OpenAI offered two proposals that he declined. He emphasized that he is making no accusation against anyone.
OpenAI said it is now focusing on understanding the internal model and using what it learns to guide and pace how it pursues further advances in capability.