OpenAI's Navier-Stokes claim splits the math community
OpenAI’s formalized Navier-Stokes result is unverified, while a dispute over credit, training data and math research intensifies.
OpenAI’s claimed solution to the Navier-Stokes existence and smoothness problem has prompted a dispute over proof, priority and who sets the pace of mathematical research.
The company says it used tens of thousands of autonomous agents to produce results addressing two alternatives in the Clay Mathematics Institute’s Millennium Prize Problem: breakdown of smooth Navier-Stokes solutions on either whole-space ℝ³ or the periodic torus ℝ³/ℤ³. The work is not yet independently verified, which is required for a result attached to a $1 million prize.
OpenAI has published a Lean 4 formalization repository with more detail than the headline claim. For every positive viscosity, it says there are smooth initial data and forcing such that no global smooth solution exists under the stated conditions. Its companion Euler result constructs smooth, compactly supported, divergence-free initial velocity on ℝ³ whose unforced incompressible flow develops a finite-time singularity. Near that time, the velocity’s C¹ norm becomes unbounded and the time integral of the vorticity’s L∞ norm diverges.
That is a precise claim, but formal verification and mathematical acceptance are not the same thing. The repository can be built with Lean 4.34.0-rc2, Mathlib and Lake, and points to instructions for independent checking with Comparator.
It does not establish that outside mathematicians have accepted the proof, that the Clay institute has ruled on it, or that anyone has qualified for the Millennium Prize.
The Navier-Stokes question concerns whether three-dimensional incompressible fluid equations can always retain smooth solutions, or whether a singularity can form in finite time. OpenAI’s repository frames its Navier-Stokes statements as alternatives (C) and (D) in Clay’s official problem description: a breakdown result on ℝ³ and a corresponding result on ℝ³/ℤ³.
The popular shorthand that an AI system “solved Navier-Stokes” compresses highly constrained mathematical claims, their formalization, their review and their eventual standing in the literature into a single verb.