OpenAI Shares AI-Generated Solution to Navier–Stokes Millennium Prize Problem

OpenAI has published an AI-generated solution to the Navier–Stokes Millennium Prize Problem, accompanying the writeup with a formal proof implemented in Lean. While interactive theorem provers allow the machine's deductive steps to be checked mechanically line by line, the mathematical community and the Clay Mathematics Institute have yet to independently review the work. The release reflects the expanding reach of automated reasoning into long-standing foundational mathematics.