Inside the Verified Proof: A Step-by-Step Walkthrough of the Lean Navier–Stokes Formalization

The technical companion of the series: what the verified Lean code actually does. Every code listing in the paper is verbatim from the repository at a pinned commit.

Six parts, in order:

1. The repository, and what “verified” means here — the trust model of a prebuilt-.lake replay: the Lean kernel re-verifies every proof artifact against its source hash and proof term in the checking environment; only the challenge files build fresh. Plus the axiom policy (propext + choice, nothing else) and the directory layout.
2. The theorem surface — the target theorems verbatim (the R3 and periodic blow-up, the Euler companion), the bridge module where the paper’s §10.3 lives in Lean, and the closure chain as the code organizes it.
3. The torus machinery — the coefficient machinery behind (8.19): rapid decay, the product majorant, the symmetric split, the lattice sum — the code’s m+5 route and how the paper’s m+4 claim follows.
4. The R3 comparison machinery — the cutoff geometry, and the flux estimate the code actually proves (the A_R-dependent bound), read against the page’s (10.19): what the geometry requires, and why the page’s pairing cannot work.
5. The Euler side — the companion singularity statement and the alignment check’s scope.
6. What we added, and what the kernel decided — the two repair commits (the (8.19) m+4 lemma; the corrected (10.19)′/(10.17)′ estimates), the verification job, and the one open row: the full closure under the corrected estimates.

The paper closes where the series starts: a green verdict says the Lean object proves itself, re-checked by a second kernel. It does not say the page’s argument is correct. The gap between those two sentences — worked symbol by symbol, with the kernel as referee for what is formalizable and a counterexample for what is not — is the subject of the counterexample paper and the walkthrough.

• Read the paper (PDF)

Companion pieces: the counterexample, the verified formalization, and the step-by-step walkthrough.