The Lean Code Is Verified; the Paper's Argument Is Not: A Counterexample to the Pressure-Flux Estimate in "Finite Time Blowup for Navier–Stokes"

OpenAI’s September 2026 manuscript “Finite Time Blowup for Navier–Stokes” carries a Lean formalization. We verified that formalization as a single bounded FalseGreen Job — the full fork compiles with the prebuilt proof artifacts replayed through the Lean kernel, the target theorems are re-checked by an independent reference checker with two different Lean kernels, and the axiom and proof-hole audits pass. The verdict is Accepted.

This paper is about what that verdict does and does not say.

Walking the manuscript’s argument step by step — the comparison lemma, the difference-energy identity, the pressure recovery, the two flux sums, the closure — shows that the chain breaks at one place: the pressure-flux estimate (10.19). Its derivation makes three claims about the supports of its cutoff functions. Each claim is false — for every admissible choice of cutoff, not just a bad one:

• the gradient bound |∇χ_R| ≤ CR⁻¹φ_{7R} fails on a nonempty shell,
• the pairing with CR⁻¹φ_{3R}|w| is impossible: the supports are disjoint,
• the monotonicity link ‖φ_{3R}w‖₃ ≤ ‖φ_{2R}w‖₃ is reversed.

The paper then shows that the bound in (10.19) is not merely unproved — it is false under its own quantitative hypotheses. For a smooth divergence-free counterexample family (explicit, with all the hypotheses of the derivation holding), the pressure flux through the annulus is nonzero for every ε > 0 while the right-hand side of (10.19) is exactly zero. The flux scales as ε² — exact, structural, not fitted — with the numbers generated by a numpy-only script that is part of the release.

The paper closes with the honest scope: (8.19), the other flagged estimate, is sound — we formalized it in Lean and the kernel accepted the paper’s argument as written. The Lean code proves a different argument (an A_R-dependent flux bound, which is what the geometry requires) — so a green verdict verifies the code, not the page. And the repair’s ingredients (corrected estimates (10.19)′ and (10.17)′) are formalized and kernel-verified, with the full closure the one honestly-open item.

The one-liner: the Lean result is verified; the paper’s argument is not — and at (10.19) the paper’s argument is invalid as written.

The full paper, with the verbatim quotations, the counterexample construction, and the reproducible script:

• Read the paper (PDF)

This is the first of four companion papers on the Navier–Stokes formalization. The companion pieces: the verified formalization, mapped to the page, the step-by-step walkthrough of the argument, and the Lean code itself, in detail.