How a Forced Navier–Stokes Flow Blows Up: A guided exposition of OpenAI's finite-time blowup construction (JSP-000005)

In September 2026 OpenAI released Finite time blowup for Navier–Stokes, with a Lean 4 formalization. For every viscosity $\nu>0$ it constructs a smooth, compactly supported force and a velocity field that starts from rest, keeps bounded kinetic energy, and becomes unbounded at time $t=1$. This addresses the forced breakdown alternatives (C) on $\mathbb R^3$ and (D) on $\mathbb R^3/\mathbb Z^3$ of the Clay Millennium Problem. It does not address the unforced alternatives (A) and (B).

This exposition explains the construction for readers with basic PDE and fluid-mechanics background. It covers the reduction to a cancellation problem for the momentum residual, the anisotropic collapsing vortex, and how amplified oscillatory pulses supply the missing annular momentum flux through their Reynolds stress. It then covers the infinite-order correction cycle, localization, the force extension, uniqueness, the torus case, and what the Lean development certifies. Every statement is tagged as taken from the paper, independently checked, a heuristic model, or background. Independent review of the source result is pending. All mathematics is due to the cited authors.

Submitted for the Exposition category of the MathDB × Justin Sun Prize pilot (JSP-000005). Fixed version v1.0 (29 Oct 2026): https://github.com/Thanh-Van-2001/navier-stokes-blowup-exposition/releases/tag/v1.0