The Proof as the Machine Checked It: The Verified Lean Formalization of the Navier–Stokes Blowup Argument
The Lean formalization of the OpenAI Navier–Stokes blowup argument, presented as a mathematical proof: the formal statement, the proof structure, a per-step mapping (math step ↔ Lean lemma ↔ verification status), the (10.19)′ repair as the formalized bridge, and the signed verification report as the evidence layer.
The companion to the counterexample paper answers the other question a green verdict raises: what exactly was verified, and where is each piece?
This paper walks the verified Lean formalization at the fork’s pinned commits — the OpenAI base repository rebased to Lean 4.34.1 with prebuilt dependencies, plus the two repair commits — as a mathematical proof. The formal statement, the proof structure, and a sixteen-row mapping table that ties every step of the paper’s argument to the Lean lemma that carries it: file, line, commit, and verification status. Each row was machine-checked against the fork (the mapping table is regenerated from a TSV and grep-verified by the test harness on every commit — a citation that drifts from the code breaks the build).
The paper makes the trust model explicit. The verification job does not
recompile the dependencies: the job workspace carries a fully prebuilt
.lake, and lake build in the job replays — the Lean kernel
re-verifies every olean against its source hash and proof term in the
checking environment. Only the challenge files build fresh. A green build
means every proof term was re-checked by the kernel, and the reference
checker re-checks the target theorems with a second, independent Lean
kernel (landrun + nanoda), with the axiom baseline audited to
{propext, Classical.choice, Quot.sound}.
The repair commits are treated as first-class content: the (8.19) m+4 torus-inverse lemma (the paper’s estimate, formalized and kernel-accepted on the first attempt) and the corrected (10.19)′/(10.17)′ estimates (Paper1019Repaired.lean) — with the open closure row stated plainly as not yet a verdict.
The evidence layer is the signed verification report itself: schema 3,
self-contained (the frozen contract embedded, verified against both bound
hashes before inclusion), with the per-criterion evidence, the environment
capture, and the signature. The offline verification command — the one that
lets you re-check the report without the platform — is in the paper’s
appendix and in the release’s evidence/ directory.
Companion pieces: the counterexample, the step-by-step walkthrough, and the code in detail.