x.com/solidSF/status/2102129112462852567

This is inaccurate as stated. Whatever one thinks about whether OpenAI’s Navier–Stokes claim is ultimately correct or accepted by mathematicians, the material OpenAI released was not just “a lemma.”

OpenAI’s paper is a 166-page manuscript titled “Finite time blowup for Navier–Stokes.” Its abstract states a full result, and page 1 gives Theorem 1.1, which claims a finite-time blowup construction for the 3D incompressible Navier–Stokes equations with bounded kinetic energy. The paper then says this establishes alternative (C) in the Clay problem statement, and that a corresponding periodic result establishes (D).

OpenAI’s public Lean repository says the same thing in plainer terms: “For every positive viscosity, we prove two results” and then lists the whole-space and periodic-torus breakdown statements. The formalization file itself labels these as “Main Theorems” and defines navier_stokes_breakdown_R3 and navier_stokes_breakdown_periodic as the relevant theorems.

So the released OpenAI work was presented as a proof with main theorems resolving the breakdown alternatives, not merely as “a lemma.”