Navier-Stokes: OpenAI's published solution: for programmers

Learn what OpenAI solved, inspect the fluid equations in the Workbench, and explore computation and checked reasoning in Osprey.

For programmers. Choose the other audience version or browse the complete series.

Navier-Stokes: OpenAI's published solution: for programmers (2:18). Captions are on; choose a chapter to jump to it.

Lean is the development oracle for compatible proofs; Osprey checks them independently. Known unsound reference behaviour must be refused, and changing a discipline requires fresh proof validation.

What this demonstrates

On 8 September 2026, OpenAI published a solution with a Lean formalization: smooth forcing produces a finite-time singularity from initially smooth fluid at rest while energy remains finite. The films explain that result before exploring Osprey. The periodic two-dimensional Taylor-Green flow is a separate numerical example with measured residuals; the Workbench exercise checks a propositional implication under explicit premises. Separately, Osprey checks selected computability, work-counter and number-theory exports from openai/math, while the complete headline theorem remains to be ported. The recorded computation and residual checker are production assets in the separate TikTok repository; the source link below opens the Workbench lesson.

Read the guide and try it yourself. Osprey is actively evolving; the guide distinguishes the recorded demonstration from current corpus progress.

Actual source

Continue learning

Use the Workbench · Current Mathlib port evidence · All twelve films

Transcript

  1. Navier-Stokes equations describe how fluids move. In September twenty twenty six, OpenAI published a solution of the three-dimensional existence and smoothness problem, with a Lean formalization. Smooth forcing can drive a fluid initially at rest to a finite-time singularity: its speed grows without bound while energy stays finite. Let's explain that result, then explore real Osprey code and its proof workbench.
  2. Open the Navier-Stokes lesson in Osprey. Velocity tells us how the fluid moves. Pressure pushes it around. Viscosity spreads out motion and removes energy from this flow. The lesson writes these relationships as equations, with a second equation requiring the fluid to stay incompressible.
  3. This is the actual Osprey program used for the picture. It calculates the flow’s spatial shape and how its strength falls over time. The renderer uses those numbers to draw the moving fluid. Separate numerical checks measure how closely the calculated field satisfies the equations.
  4. Watch the four rotating cells lose strength. No external force keeps them going. The energy readout falls as viscosity dissipates the motion. This is a known exact solution in two dimensions, with a domain that repeats at its edges. Osprey evaluates its formula, so we can compare the calculation with a known answer.
  5. The published proof has a precise statement and a Lean formalization; the lesson also supplies a much smaller propositional exercise. Assume there are two possibilities, and one has been ruled out. Show that the other must hold. Write the assumptions, consider each case, and watch Osprey check the proof. The words smooth and blowup name propositions here; the exercise teaches how a conclusion follows from assumptions.
  6. Open the lesson to explore the symbols and try the remaining-outcome exercise. Osprey already checks selected supporting lemmas from the published OpenAI sources. The complete Navier-Stokes proof is a larger port still to do. You can run this fluid calculation and build your own small checked arguments today.