OpenAI Says Famous Fluid Equations Can Break Down, and Publishes Files Anyone Can Check
OpenAI has published two manuscripts claiming that smooth solutions to the Navier-Stokes and Euler equations, which describe how fluids move, can break down after a finite time, and has released computer-checkable versions of both proofs. The company posted the files to a public GitHub repository on September 8, 2026. The manuscripts have not been peer-reviewed and have not gone through a journal.
Publishing the proofs in checkable form means outsiders can test the argument instead of taking it on trust. The repository holds formalizations written in Lean 4, a language in which software verifies every step of a proof, and its README gives instructions for running an independent checker, Comparator, over both results. The files carry an Apache 2.0 license, so anyone can rerun the check.
According to the repository, OpenAI claims to prove two Navier-Stokes results for every positive viscosity. On all of three-dimensional space, it says, there are smooth starting conditions and an applied external force for which no smooth solution lasts for all time with bounded energy. On a repeating cube, it says, there are smooth periodic starting conditions and a force for which no smooth solution lasts for all time. Both statements rely on that external force. The Euler claim does not: OpenAI says it builds a smooth starting velocity, confined to a limited region, whose flow develops a singularity in finite time under the unforced Euler equations, meaning the solution stops being smooth.
OpenAI identifies the two Navier-Stokes results as alternatives (C) and (D) in the Clay Mathematics Institute's official description of the Millennium Prize Problem, written by Charles L. Fefferman. Those are the two branches in which solutions break down. Clay's published rules put any claim a long way from a prize: the institute takes no direct submissions, and will consider a proposed solution only after it has been published in a qualifying outlet, two years have passed, and it has won general acceptance in the global mathematics community.
The repository credits the Lean statement of the Navier-Stokes problem that it checks against to the authors of Google DeepMind's Formal Conjectures project, which OpenAI adapted.
