What OpenAI put online
OpenAI has published the material behind its claim to have found a finite-time singularity in the three-dimensional Navier-Stokes equations: a write-up on its own site, a paper, and machine-checkable proof files in a public GitHub repository. The company said it does not intend to claim the Clay Mathematics Institute’s $1 million Millennium Prize for the result.
That is the change from Monday, when the claim existed only as a description passed between researchers. The repository contains Lean 4 formalisations, built against Mathlib and released under Apache 2.0, for two Navier-Stokes cases at positive viscosity - one on the whole space and one on the periodic torus - and for a companion Euler construction. Anyone with a Lean toolchain can now run the certificate rather than take the claim on trust.
The numbers OpenAI reports
The compute figures come from OpenAI and have not been independently audited. The company said the work used an internal model it describes as significantly more capable than GPT-6 Astra, and that roughly 10,000 agents ran concurrently for about 88 hours in early September, producing on the order of 130 billion output tokens. A further stretch of about 17 hours, as reported by The Next Web, went into formalising the argument with GPT-6 Astra.
Those are inputs, not evidence. The evidence is the Lean file, and Lean does not care how many agents wrote it.
Why the prize is not being claimed
The Clay formulation of the Navier-Stokes problem is split into four statements. OpenAI says its result establishes statements C and D - the breakdown alternatives, which resolve the problem by exhibiting a solution that fails to stay smooth. It also says it will not claim the prize.
The reason is in the construction. The fluid starts at rest and a smooth external force is applied throughout, and the singularity develops under that forcing. Whether a forced example counts for the classical question is a judgement for mathematicians and for Clay, not for a proof assistant. The institute’s own page still lists Navier-Stokes as an open problem.
The credit fight is still running
The result lands in the middle of an argument Aivio News reported on Monday. Tristan Buckmaster of NYU and Levent Alpoge of Anthropic posted their own AI-assisted, Lean-verified blowup proofs for the porous medium, Boussinesq and Euler equations, and Buckmaster published a statement describing how OpenAI approached him about the timing and authorship of the Navier-Stokes result. OpenAI’s Sebastien Bubeck called that account false and inflammatory.
Quanta Magazine reported that Princeton’s Charles Fefferman, who wrote the official problem statement, called Diego Cordoba and Luis Martinez-Zoroa the heroes of the story - the pair whose non-computational method both efforts build on.
What to watch
Two things are now checkable rather than arguable. The first is whether independent mathematicians compile the Lean files and confirm they prove what the write-up says. The second is whether the Clay Mathematics Institute says anything about forcing terms. Until it does, the honest description is that a machine-verified singularity exists and its relationship to the prize question is unsettled.
