OpenAI reports an AI-generated Navier–Stokes proof
A September 8 announcement releases a proposed proof and Lean code for scrutiny, with smooth forcing central to the claim.
A major claim, with evidence to inspect
OpenAI announced on September 8 that an internal AI system produced a Navier–Stokes proof, releasing a mathematical writeup and Lean formalization. The company reports finite-time breakdown with smooth external forcing and finite energy.
Which statement is being claimed?
The accompanying repository identifies alternatives C and D of the Millennium problem: breakdown in three-dimensional space and in a periodic domain. Readers should retain the forcing condition when describing the result. The repository provides build commands and instructions for independent checking with Comparator.
What comes next
MathsAI has not rebuilt the certificates or independently verified the argument. This article reports a research announcement; it does not certify mathematical acceptance or a prize decision. Inspecting the precise statement and its correspondence to the written proof is the next task for expert readers.