OpenAI announced on September 8, 2026 that an internal AI system produced a proof, accompanied by a formalization in the Lean proof assistant, that the Navier–Stokes equations governing fluid motion can develop a singularity in finite time. The company said the result resolves one of the Clay Mathematics Institute’s Millennium Prize Problems. What the Proof Establishes OpenAI shared both a writeup of the proof and its Lean formalization. According to the announcement, the proof shows that an…