OpenAI claims a Lean-verified solution to the Navier–Stokes Millennium Prize problem, and the first objection is about who got there first
OpenAI says 10,000 coordinating AI agents spent 88 hours producing a finite-time singularity proof for the 3D Navier–Stokes equations, with a Lean formalization to back it. The trouble is that a parallel team at NYU and Anthropic posted closely related results 12 hours earlier, and one of them is now publicly asking whether OpenAI's models had access to his work.
On Saturday, September 5, OpenAI says roughly 10,000 coordinating AI agents arrived at a resolution of the Navier–Stokes problem about 88 hours after the first agents were launched, according to CNBC’s September 9 reporting on the company’s announcement. What they reportedly produced is a finite-time blowup — a point at which the velocity field in the 3D Navier–Stokes equations becomes singular — together with a Lean formalization intended to mechanically check the proof. Quanta Magazine’s coverage from September 8 describes the result as a candidate resolution of one of the seven Clay Millennium Prize Problems, with a writeup and a Lean-verified proof released publicly.
The result, if it holds, would settle a question that has been open in roughly its current form since Jean Leray introduced the modern weak formulation of the equations in the 1930s: whether smooth solutions to the 3D incompressible Navier–Stokes equations can remain smooth for all time, or whether some initial data forces a singularity in finite time. The Millennium Prize formulation asks the existence question. OpenAI’s claim is the second, more dramatic outcome — and, crucially, one that has been a target of serious mathematical attack for years. Quanta notes that the route OpenAI’s agents followed leaned heavily on a strategy developed by Antonio Córdoba and Ángel Martínez-Zoroa, which had been seen as a plausible path toward a singularity construction.
The novelty here isn’t only mathematical. The 10,000-agent setup — long-running autonomous agents coordinating on an open research problem, with the proof then ported into a proof assistant — is itself a first at this scale. Nature’s September 18 coverage frames the announcement as a proof that a singularity exists in finite time, alongside the Lean formalization, and reports that physicists and mathematicians are now debating what the result would mean for fluid dynamics research if it survives scrutiny.
The trouble is the timing. Quanta’s account places OpenAI’s public announcement roughly 12 hours after NYU mathematician Tristan Buckmaster and Levent Alpöge of Anthropic posted their own closely related results independently. The two efforts converged on similar ideas; Buckmaster has since publicly questioned whether the route OpenAI’s models took to the solution is too similar to his and Alpöge’s to be coincidence, and asked whether OpenAI’s models had been trained on or had access to their sessions in OpenAI’s Codex environment. He has stopped short of claiming direct evidence of misuse.
CNBC’s reporting carries OpenAI’s response: the company says its researchers and agents did not see Buckmaster and Alpöge’s work until it was released publicly, that no specific user data was accessed, and that while it considers contamination unlikely, it cannot rule out the possibility that de-identified data drawn from product usage helped improve the models in ways relevant to this problem. That’s a deliberately hedged statement, and it’s the version of events the mathematics community is now being asked to evaluate alongside the proof itself.
The structural worry this exposes is bigger than any single dispute. If the most capable AI systems for mathematical research are also the systems whose users — including rival research groups — are actively writing proofs in, then the ordinary expectation that prior work is cited and credited has to be replaced by something stronger: a verifiable separation between what a model was trained on, what it has seen in context, and what it generated on its own. OpenAI’s own concession that it cannot fully rule out de-identified data leakage is, on this reading, less a denial and more an admission that the current audit trail doesn’t actually settle the question Buckmaster raised. Until it does, even a formally verified Lean proof is going to be read in two layers at once: as a mathematical claim, and as evidence about the integrity of the system that produced it.