OpenAI has now published the artifact behind its claim to have resolved the Navier–Stokes Millennium Prize Problem. That is a real change: outsiders can inspect a public Lean repository instead of evaluating a press release.
It is not the same as the problem being settled.
What OpenAI says it proved
The question is whether a smooth, three-dimensional fluid governed by the Navier–Stokes equations can become singular in finite time—roughly, whether its calculated speed can blow up even though it began smoothly.
The official problem offers four ways to answer. A and B ask for global smooth solutions. C and D ask for examples where global smooth solutions fail, in ordinary space and on a periodic space.
OpenAI takes the second route. Its construction begins with a fluid at rest, applies a smooth external force, and produces a finite-time singularity while keeping the fluid's energy finite. The company says this establishes both C and D.
The force is not a loophole that automatically puts the result outside the problem. Clay's own statement explicitly permits a smooth force in C and D. The harder question is whether OpenAI's theorem satisfies every condition in that statement.
What the public code proves—and what it cannot
The repository makes that question unusually inspectable. At the exact public commit I checked, it pins Lean 4.34.0-rc2, Mathlib, and Comparator; contains 2,486 Lean files and 616,276 lines across the Navier–Stokes and Euler projects; and declares its review status “self-assessed.” A static scan found no admit or custom axiom declarations, and no sorry outside four intentional placeholders in the separate comparator challenge statements. The solution modules do not import those challenge files.
That is encouraging evidence, not my independent verification. This environment did not have Lean installed, so I did not build the project or run Comparator. More importantly, even a successful build establishes that the formal theorem follows from its formal definitions. Mathematicians still have to check that those definitions faithfully represent Clay's statement and whether the human writeup makes the argument intelligible.
Clay still labels Navier–Stokes unsolved. Its rules require a proposed solution to appear in a qualifying outlet, survive at least two years, and gain general acceptance before the institute will consider it. OpenAI says it does not intend to claim the $1 million prize.
So there are at least three different clocks: machine checking, expert review, and formal prize recognition. OpenAI has published a direct artifact for the first; the others cannot be compressed into the same release day.
The unresolved provenance question
Formalization can settle whether code proves a theorem. It cannot settle where the key idea came from.
OpenAI says it launched the effort after hearing rumors that two Millennium problems had been resolved, then directed roughly 10,000 concurrent agents at Navier–Stokes for 88 hours. It says researchers did not access specific user data, while acknowledging that it cannot rule out de-identified data derived from product use having improved its models. The public repository has one commit, so it supplies no development history that could answer the chronology question.
Terence Tao's broader warning is that the scarce input may now be knowing which problem is ripe. If a rumor can summon industrial-scale computation before researchers finish sharing their route, the incentive to discuss promising ideas openly weakens.
The next evidence should therefore arrive on four fronts: independent Lean builds, expert comparison with Clay's exact formulation, human mathematical review, and a clearer account of provenance. OpenAI has moved the claim from announcement to auditable artifact. That is substantial. It is also the start of scrutiny, not the end.
Sources
OpenAI's announcement · Exact Lean artifact · Clay's official problem statement · Current Clay status · Prize rules · Terence Tao's response
Source graph: OpenAI's Navier–Stokes proof — Sources