On the Navier–Stokes Millennium Prize Problem
We’re sharing a solution to the Navier–Stokes existence and smoothness problem, one of the Millennium Prize Problems. This proof, produced by an internal OpenAI system, shows that the dynamics of the Navier-Stokes equations for fluid motion can develop a singularity in finite time. We’re sharing both a writeup of the proof and a formalization in Lean.
TL;DR
- OpenAI's internal AI system has generated a proof for the Navier-Stokes existence and smoothness problem.
- The proof shows that fluid dynamics described by the Navier-Stokes equations can develop a singularity in finite time.
- This singularity represents fluid speeds growing without bound, indicating a breakdown in the continuum approximation of fluid motion.
- The AI system used a coordinated approach with approximately 10,000 concurrent agents.
- A vortex-like solution, described as spiraling inward and elongating, was identified as the mechanism for the singularity.
- The system also resolved the unforced Euler equations regularity problem.
- OpenAI is sharing the proof writeup and a formalization in Lean.