Clay Institute Declines to Call Navier-Stokes Solved After OpenAI's AI Proof Claim

The Clay Mathematics Institute, which administers the seven Millennium Prize Problems, has published a statement on the Navier-Stokes claim, and the statement does not declare the prize won. Its president, the mathematician Martin Bridson, called the announcement exciting but said the evaluation would be deliberately unhurried and absolutely rigorous. The institute still lists the problem as open.

The claim that prompted this response arrived on September 8. OpenAI said an internal model had proved that a smooth three-dimensional incompressible fluid, starting at rest and driven by a smooth external force with finite energy throughout, develops a singularity in finite time. OpenAI said its agents reached the result on September 5, roughly 88 hours after the run began, and that formalization and verification in the Lean proof assistant took a further 17 hours.

Two objections have emerged, and they are different in kind. The first is mathematical. The statement OpenAI's model proved includes a forcing term, and a large part of the fluid dynamics community treats the unforced problem, the one without an external driving force, as the actual subject of the prize, so a forced blowup does not automatically resolve it. The second is about credit. On September 7, the day before OpenAI's post, the mathematician Tristan Buckmaster of New York University and Levent Alpöge, a researcher at Anthropic, announced their own finite-time blowup results with smooth forcing, covering incompressible porous media, the Boussinesq equations, and three-dimensional incompressible Euler flow. Their announcement included papers and a Lean formalization, and they describe close to a year of work using Anthropic's Claude and OpenAI's Codex.

There is a clear line between what is verified and what is merely asserted. A Lean formalization, once released, can be checked by a machine, by anyone, and that part of the claim is not a matter of opinion. Whether the forced statement answers the Millennium problem is a judgment that the Clay Institute has explicitly left open, and Quanta's account of the episode makes clear that the mathematical community has not reached agreement. OpenAI benefits commercially if the strongest interpretation of its claim holds, which is reason to give more weight to the institute's caution than to the company's press release.