OpenAI has published an AI-generated solution to the Navier-Stokes Millennium Prize Problem, one of seven unsolved problems with a $1 million prize each from the Clay Mathematics Institute. The submission includes a written proof and a formal verification in Lean, the theorem-proving language used to mechanically check mathematical logic. If valid, this is the first Millennium Prize Problem solved by an AI system.
The Lean formalization is the detail that matters most here. Written proofs can contain subtle errors that survive peer review for years. A Lean proof is machine-checked, meaning the logical structure is verified step by step against formal axioms. That does not guarantee the problem is solved, it guarantees the proof is internally consistent. The mathematical community will now determine whether the formalization correctly encodes the actual problem.
Read the full writeup and Lean proof to understand which specific variant of the Navier-Stokes problem is addressed, global regularity or finite-time blowup, and what assumptions the proof rests on. The gap between a technically valid Lean proof and a Clay Institute prize claim is significant, and the details of that gap are exactly what makes this worth reading.
[READ ORIGINAL →]