A machine proof of a Millennium Prize problem, checked in Lean

OpenAI — Navier–Stokes existence and smoothness — OpenAI published a proof, produced by an internal model, resolving the Navier–Stokes existence-and-smoothness problem — one of the seven Clay Millennium Prize Problems, open for roughly 90 years. The answer is negative: the model constructs a finite-time blowup, a configuration in which a vortex tightens and spins ever faster while the fluid's total energy stays bounded. OpenAI says the run took 88 hours across as many as 10,000 concurrent agents, and that the argument was verified in Lean on 6 Sep 2026. Machine-checked is the strongest part of the claim and is not the same as accepted: the Clay Institute's criteria require peer-reviewed publication and a waiting period. A credit dispute followed — OpenAI began work on 1 Sep after a rumour it later traced to Levent Alpöge and Tristan Buckmaster, whose result turned out to concern the forced Euler equations, a related but distinct problem.