The Navier–Stokes equations model fluid motion. OpenAI said its internal AI system produced an analytical proof that an initially smooth fluid at rest could develop a singularity in finite time under a smooth external force, while retaining finite energy. The company identifies the result with statements C and D in the Clay Mathematics Institute’s formulation. An October 6, 2026 preprint argued that OpenAI’s Lean formalization does not correspond to its written proof. OpenAI’s announcement and the later critique concern both the claimed result and how it was formalized.
What OpenAI says its proof covers
OpenAI described a result for the three-dimensional incompressible Navier–Stokes equations, with the fluid initially at rest and a smooth external force. A finite-time singularity is a breakdown in the smooth behavior of a solution after a finite interval. OpenAI said the fluid’s energy remains finite in the construction and identified the claim with statements C and D of the Clay problem.
The company also said it does not intend to claim the Millennium Prize. For background on the earlier debate about human review, see NeoTeo’s coverage of OpenAI’s Navier–Stokes claim.
OpenAI reported that roughly 10,000 concurrent agents reached the result about 88 hours after launch. The company said Lean formalization and checking took a further 17 hours using GPT-6 Astra. It also reported 2.7 million messages and about 130 billion output tokens for the effort.
The Euler and Navier–Stokes results use different conditions
The three results discussed in OpenAI’s announcement and Scientific American’s October 22 reporting differ in their equations or external-force conditions.
| Result | Equation | External-force condition |
| Buckmaster–Alpöge result | Euler | Forced |
| OpenAI result | Euler | Unforced |
| OpenAI result | Navier–Stokes | Smooth external force |
A forced equation includes an external force; an unforced one does not. OpenAI described its Euler result as unforced, while its Navier–Stokes construction uses smooth external forcing. Scientific American described the Euler result by Tristan Buckmaster and Levent Alpöge as forced. Those conditions are part of what each result addresses.
What the Lean critique challenges
Lean is a proof assistant: it checks a proof expressed in a formal language against the definitions and rules encoded there. That check applies to the formal statement and proof. A separate question is whether that formal statement corresponds to the claim made in ordinary mathematical prose.
In a preprint submitted October 6, Alexander Bastounis, Fabian Circelli, and Anders C. Hansen argued that OpenAI’s Lean formalization does not correspond to its natural-language proof. Their arXiv abstract frames the issue as a gap between the formalized argument and the written one. The dispute is therefore about the relationship between those two representations of the claim.
The disputed route to the result
Scientific American reported that Buckmaster suspects OpenAI’s work drew on a line of research pursued with Levent Alpöge. The same report described OpenAI’s forced Navier–Stokes construction as distinct from the Spanish program associated with Diego Córdoba and Luis Martínez-Zoroa, and recounted differing expert views of how the approaches relate.
OpenAI said user inputs after July 3, 2026, including Buckmaster’s Codex and ChatGPT use, could not have influenced its model or the mathematical results. That is the scope of the company’s stated cutoff; Buckmaster’s suspicion and OpenAI’s response remain competing accounts of the work’s lineage.
