A snapshot taken at 19:30 UTC on September 8 recorded 1,109 points and 941 comments on the Hacker News submission for OpenAI's Navier-Stokes announcement. The mathematics runs on a slower clock. The Clay Mathematics Institute will not consider a proposed solution until it appears in a qualifying outlet, at least two years have passed, and the result has gained general acceptance. OpenAI has released a 166-page paper and a Lean certificate, yet the certificate's own metadata calls its review status "self-assessed."
That gap is the immediate story for developers. The public repository turns part of an extraordinary research claim into code that other people can build and inspect. It does not make the definitions, mathematical interpretation, research provenance, or Clay's acceptance process disappear. A checked proof term and an independently accepted solution answer related questions on very different schedules.
The claim uses the forced branch of the problem
The Navier-Stokes equations describe the velocity and pressure of an incompressible fluid. Viscosity smooths changes in velocity, while the nonlinear motion of the fluid can amplify them. In three dimensions, mathematicians have been unable to prove whether smooth starting conditions always remain smooth or whether a solution can develop an unbounded velocity in finite time. The official problem description by Charles Fefferman sets out four acceptable ways to settle the question.
OpenAI claims a counterexample. Its main theorem says that, for every positive viscosity, a fluid starting from rest can be driven by a smooth force that is compactly supported in space and time. The velocity and pressure remain confined to a compact region, and kinetic energy stays bounded, but the maximum velocity becomes unbounded as time approaches one. If the argument holds, this establishes Clay's alternative C in ordinary three-dimensional space. A corollary claims alternative D for a periodic three-dimensional torus, according to the paper's theorem statement.
The external force is an important qualification. Alternatives A and B ask whether smooth solutions always exist when that force is zero. Alternatives C and D expressly allow a smooth force and ask for data for which a global smooth solution cannot exist. OpenAI has chosen a route that the Clay formulation permits. Reviewers still have to establish that every regularity, decay, energy, and domain condition in the construction matches that formulation.
The proposed flow is a collapsing vortex. OpenAI's account says the central swirl narrows, stretches, and accelerates while retaining finite energy. Oscillatory pulses supply a mean momentum flux, and several large terms must cancel so that the force stays smooth even as velocity diverges. The paper develops that construction across ten sections and three appendices; length by itself says nothing about correctness.
A proof certificate developers can build
OpenAI published the formalization under the Apache 2.0 license. The repository targets Lean 4.34.0-rc2, uses Mathlib and Lake, and gives two commands for a local build after elan is installed:
lake exe cache get
lake build
The repository instructions also provide a Comparator path for checking the Navier-Stokes and Euler results with external tools. That matters because a normal successful build uses the Lean process and its installed dependencies, while Comparator can export declarations for a separately implemented checker.
The project's formalization metadata reports zero uses of sorry, Lean's placeholder for an unfinished proof, in the main results and their definitions. It maps theorem 1.1 and the periodic corollary to named Lean declarations. For comparison against the intended question, the project adapts a Navier-Stokes statement from Google DeepMind's Formal Conjectures project rather than relying only on a statement written alongside the solution.
Lean's kernel checks that a proof term has the declared type. The Lean documentation on proof validation is explicit about the remaining trust boundary: the formal theorem must correspond to its intended informal meaning, imported libraries must mean what their authors think they mean, and no unsound assumptions can enter the chain. This is why "zero sorry" is useful evidence without being the last word on a 90-year-old problem.
OpenAI's formalization metadata describes the work as complete and the mapped statements as proved, but it records the review as self-assessed. The public materials read for this article do not document an outside audit of the 166-page argument or its translation into Lean. Running lake build is therefore a good first replication task. It is not a substitute for specialists tracing the definitions back to Fefferman's alternatives C and D.
The discovery run cannot yet be reproduced
OpenAI says it began training a new internal model on August 28 and started testing open Millennium Prize problems after hearing rumors of progress on September 1. The group that produced the Navier-Stokes result used about 10,000 concurrent agents. According to OpenAI's account, the agents reached the result after roughly 88 hours, sending 2.7 million messages and producing about 130 billion output tokens. GPT-6 Astra then spent another 17 hours on formalization and verification.
The company's account says the discovery model is more capable than GPT-6 Astra and remains internal. Agents could read a cached version of the web, run code, exchange intermediate results within groups, and receive consolidated ideas from other groups. The paper and certificate are public outputs, while the model and full research run are unavailable for outsiders to repeat. Developers can reproduce the checker path more readily than the system that generated what it checks.
The dispute is about provenance as well as priority
OpenAI's sprint followed work by mathematicians Tristan Buckmaster and Levent Alpoge. In a four-page statement, Buckmaster credited Diego Cordoba and Luis Martinez-Zoroa with the underlying program of constructing forced blowups. He said that he and Alpoge used Claude and Codex during a year of work, obtained smooth-forcing blowup results for Boussinesq and Euler on August 15, and verified the Euler result in Lean on August 22. Their announced results do not themselves settle the Navier-Stokes Millennium problem.
Buckmaster's statement says that information about his team's progress reached OpenAI before its first prompts were sent. He also said he asked whether their private Codex sessions had entered training and did not receive an answer to that narrower question. The statement alleges that OpenAI researcher Sebastien Bubeck twice proposed removing Alpoge from authorship because Alpoge works at Anthropic. Buckmaster also wrote that he had not seen OpenAI's proof, did not know whether his team's data was used, and was "not accusing anyone of anything." Those limits are part of the allegation, not optional fine print.
OpenAI's public account says its researchers and agents saw none of Buckmaster and Alpoge's work before publication. It says no specific user data was accessed to solve the problem, while allowing that de-identified data derived from their product use might have contributed to model training. OpenAI says its proofs differ substantially and that the Euler results are different: Buckmaster and Alpoge address forced Euler, while OpenAI claims an unforced construction. The post does not answer the reported authorship proposal.
Terence Tao drew a wider lesson from the episode. In a four-part Mathstodon post, he argued that identifying a fruitful open problem is itself scarce research work. A rumor can now trigger a large AI effort before the original project matures, he wrote, which may give researchers a reason to share less. Tao's post is commentary on research incentives, not independent confirmation of OpenAI's proof.
The review cannot run at model speed
OpenAI says it does not intend to claim the Millennium Prize. That choice does not settle the mathematical status of the work. Clay's rules say it does not accept direct submissions, and the two-year period begins only after publication in a qualifying outlet. General acceptance across the mathematics community must come before Clay decides whether a proposed solution deserves its own examination.
The next evidence should be concrete: independent build reports from the published repository, external-checker results, expert audits of the formal definitions, and a readable account that specialists can compare with the prior forced-blowup program. Any fuller disclosure from OpenAI about the prompts, data handling, and human direction would also clarify provenance. Until that work appears, the accurate label is an AI-generated proposed solution accompanied by a self-assessed formal certificate.