OpenAI says AI generated a Navier–Stokes solution with a Lean proof

OpenAI has published what it calls an AI-generated solution to the Navier–Stokes Millennium Prize Problem, one of the most studied open questions in mathematics. In a post titled “On the Navier–Stokes Millennium Prize Problem,” the company says it is “sharing an AI-generated solution to the Navier–Stokes Millennium Prize Problem, including a writeup and a formal proof in Lean.” Lean is software that checks a mathematical proof one step at a time.

The Navier–Stokes equations describe how fluids such as air and water move, and they are used across science and engineering, from weather forecasting to aircraft design. The problem is one of the Millennium Prize Problems, a short list of unsolved questions set out by the Clay Mathematics Institute, and it remains open. A solution accepted by the wider field would be a major result regardless of who or what produced it.

The formal proof is the notable part of the release. A formal proof is written in a language a computer can read, so each line can be checked automatically and a reader does not have to trust the author’s judgment. That kind of proof still has limits: readers must agree that the statement written in Lean is a faithful version of the problem, and that the checker’s own core is sound. What it removes is much of the guesswork involved in going through a long argument by hand. OpenAI says the release also includes a standard writeup in prose.

Much is still unknown. The announcement is short. The text shared does not name the AI systems used, describe the method, or say how much human input was involved, and it does not point to any review by mathematicians outside the company. It is also not clear from the post when the work was finished or whether the proof has been submitted anywhere for publication. Long proofs often contain gaps that take specialists time to find, and a claim at this level is normally checked by others before it is accepted.

The Clay Mathematics Institute, which defined the problem, has its own criteria for recognizing a solution. The material here comes from OpenAI alone, and there is no independent confirmation that the Lean proof is complete and correct or that it settles the problem as the institute states it.

What to watch is whether OpenAI releases the full Lean files and the writeup, whether the proof compiles and holds up when other people run it, what researchers in fluid dynamics and formal verification say once they have read it, and whether the Clay Mathematics Institute responds. None of those steps has happened in public yet.