Verified, Not Understood: What the Navier–Stokes Proof Certified and What It Left to People

Machine verification certifies the statement it is given. It does not certify that the statement says what its authors meant, or that the explanation people read is the proof that was checked. This paper uses the September 2026 Navier–Stokes episode to show where that boundary sits. OpenAI announced a 166-page proof, with a Lean formalization, that a smooth fluid at rest can develop a singularity in finite time when a smooth external force is applied, settling alternatives (C) and (D) of the Clay Mathematics Institute's problem as Charles Fefferman wrote it. Separating the chain from intent to proof into five layers, the paper finds that the machine-checked layers held on the cited record: the formal theorem was compared against an independent formalization of Fefferman's text and accepted. This paper did not rebuild the proof or read the full Lean development; that check rests with the parties who ran it.

Research library