The 2026 Navier–Stokes blowup claim: the Lean proof read against its statement

The theorem the certificate proves was not written by the prover. The Comparator challenge file is the Formal Conjectures statement of the four Clay alternatives, added by DeepMind on 2026-05-15 and last touched on 2026-07-27, the revision OpenAI pinned and the revision on main today. The copy differs from upstream in 4 lines, every one an open or a notation. The solution side re-declares the same definitions under the same names, byte-identical once comments are stripped, because Comparator compares every constant reachable from the theorem's type for exact equality. So the question is only whether that statement is Clay's. The rule for reading it: the theorem is a negation — "there exist data for which no solution exists" — so a solution notion weaker than Clay's only makes the theorem stronger; a gap could hide only in a competitor class stronger than Clay's or a data hypothesis weaker than Clay's.

The formal statement is Clay's (C) and (D) with nothing added to the competitor class and nothing dropped from the data conditions. The definitions were written by DeepMind's Formal Conjectures project on 2026-05-15 (#1457), last touched 2026-07-27, byte-identical to main on 2026-09-09; OpenAI's copy differs in imports, attributes, namespace and local notation only. The direction rule: the theorem is a negation, so a weak or junk-valued solution notion only strengthens it; a gap could hide only in a competitor class stronger than Clay's or a data hypothesis weaker than Clay's, and neither occurs.

The paper is an LLM-written account of a machine-found proof; the Lean is the claim. Where the two differ, the page reports the difference and nothing more. One difference mattered to the announcement: OpenAI's page says "its energy remains finite through the entire dynamics, from rest to the formation of the singularity". Theorem 1.1 states it; Lemma 10.4 proves it on paper in three lines that were re-derived here and hold. At the announced commit 8937a8f4 the repository contained the general lemma (a smooth compactly supported force gives a uniform L² bound on [0,1)) and nothing invoked it, and the structure that would carry the bound had no producer. The Millennium alternatives do not need it — a global smooth competitor is excluded by uniqueness on every [0,T] with T < 1, where the candidate's energy is finite by compact support alone — so the formal result stood and the physical headline was, at that commit, a paper claim. At f9e8bc5b it is not: the table's last column says where, and §4b says how far that was checked here.

What makes that omission legible is the Euler theorem in the same repository. the Euler singularity theorem asserts, for a nonzero smooth compactly supported datum: a solution on [0, T*) with 0 < T* ≤ 1, a uniform energy bound on the whole lifespan, maximality as an equivalence (a solution on [0, T] exists if and only if T < T*), the C¹ norm finite on every shorter interval, its limsup infinite at T*, the Beale–Kato–Majda integral infinite, and no global smooth finite-energy solution. That is the positive content of a blowup theorem, formalized. The Navier–Stokes candidate carries nine of those ten kinds of clause; the missing one is the energy. Same team, same week, same repository — which is why this read as an oversight rather than an obstacle, and why the unused lemma in R3/CompactEnergy.lean was the tell. The reading held: f9e8bc5b fills exactly that field with exactly that lemma, in one proof bullet, the day after the audit.

The audit read 8937a8f4, the commit the 2026-09-08 announcement shipped. Upstream moved once, to f9e8bc5b (authored 2026-09-10, the day after this audit), and this record said nothing about it until an outreach research pass found it on 2026-10-05. This is the reading of that commit at the level the audit worked; the computed facts — the diff, the line numbers, the sha256 pins, the build on this machine and the kernel's axiom report — are upstream-f9e8bc5b.json, never retyped here.

What the commit changes. f9e8bc5b proves the paper's Theorem 1.1 as stated, energy bound included: NavierStokesR3.theorem_1_1 : ProblemStatement.breakdownStatement, the statement that sat unproved at the pin. The candidate gains the two clauses the audit found missing or weaker — the uniform energy bound, from the lemma the audit called unused, and the force's support inside t > 0 — and Clay's (C) and (D) are re-derived from theorem_1_1 rather than from the ten-field candidate. The statements Comparator judges are untouched. In numbers, computed from the two commits: 188 files, 173 added and 15 modified, 25,143 lines in and 81 out; nothing under Euler/; the challenge files, the solution-side definitions, R3/ProblemStatement.lean, R3/CompactEnergy.lean and the toolchain pins byte-identical to 8937a8f4. The hole the audit found is the field energy_bounded := ?_ at NavierStokes/R3/ActualCandidate.lean:114, filled at NavierStokes/R3/ActualCandidate.lean:119 by CompactEnergy.uniform_finite_energy (NavierStokes/R3/CompactEnergy.lean:343, unchanged); the force's support inside t > 0 fills force_support at NavierStokes/R3/ActualCandidate.lean:110. theorem_1_1 : ProblemStatement.breakdownStatement is at NavierStokes/R3/Theorem.lean:46; Clay's (C) is now obtained from it at NavierStokes/ComparatorR3Theorem.lean:43 through comparator_of_breakdown (NavierStokes/R3/ComparatorBridge.lean:77), and (D) from the periodic corollary at NavierStokes/ComparatorTheorem.lean:52. In code lines at f9e8bc5b there are still 0 sorry, 0 axiom declarations, 0 native_decide and 0 unsafe across 2,659 files.

Built here, 2026-10-06. Every file the diff touched and everything that imports one — 486 modules — recompiled over the oleans of the 2026-09-09 build, in 25 minutes on 8 cores / 16 GB, darwin 27.0.0; exit 0, no errors; the other 2,173 modules are byte-for-byte the ones built for 8937a8f4. Lake was not used, and why is a fact about this machine, not the proof: the toolchain's compiled lake, lean4export and comparator abort at start on its current OS, while lean runs clean, so tools/build-navierstokes-head.py drives the pinned lean with the compile line Lake records. Then, exactly as for the pin, a scratch file asked the kernel for the axioms of the four declared main results and of the new theorems: only Classical.choice, Quot.sound, propext for all 7; and it types the new theorem as NavierStokesR3.theorem_1_1 : NavierStokesR3.ProblemStatement.breakdownStatement.

Is it the paper's theorem? Comparator does not judge this statement — it judges (C) and (D), which are unchanged — so it was read the way §2 reads those, clause by clause, 9 same and 2 equivalent. Theorem 1.1 is an existence statement with a negation attached, so the direction rule of the statement table applies twice: in the existence part a clause WEAKER than the paper's (a junk value, a missing integrability) would make the theorem cheap, and in the negation a competitor class STRONGER than the paper's would. Neither occurs.

breakdownStatement is the paper's Theorem 1.1 with nothing dropped from the conclusions and nothing added to the competitor class. Unlike (C) and (D), whose statement a third party wrote months before the proof, this statement is OpenAI's own (R3/ProblemStatement.lean, byte-identical at the pin, where it stood unproved under its own docstring, 'the full assertion of Theorem 1.1'); its authority is this reading, not Comparator.

upstream-f9e8bc5b.json pins the 11 files this section rests on by sha256, with copies in corpus/navier-stokes/lean/f9e8bc5b/. Its one decided field — is the energy clause a formal conclusion? — is decided at both commits by the same rule, and the record refuses unless the rule calls 8937a8f4 NOT formal, as the audit read it; it does. The battery re-hashes the copies, re-decides the field from them, checks the line numbers above against the bytes, and rejects 2 planted variants.

Six readers took the paper apart the day after it appeared — §3 with §10, §4 with Appendix B, §5 with Appendix A, §6 with §7, §8 and §9 with Appendix C, and the Lean against all of it — transcribing every statement, tracing the order in which every parameter is fixed, re-deriving what could be re-derived and testing by computer what could be tested. No circularity was found. No error was found. The table records what was verified; the list below it records what the paper asserts rather than displays, ranked by how much rests on it. In a proof whose authority is a kernel, such a list is a reading aid, not a verdict; it is the list a referee of the paper would write.

Asserted, not displayed — ranked.

Slips, each harmless with its margin: Prop 9.5 and §9 Steps 1–2: the −κ_s that Lemma 9.2 attaches to the zero harmonic of a two-wave product is dropped (M_{C*−κ_s} should be M_{C*−2κ_s}); margins 0.08 and 0.4 against κ_s = 10⁻⁵; Lemma 9.2's proof: 'axial transport gains one through D_z' is false for the phase (D_zΦ = p_z = O(1)); the conclusion is unaffected; p. 51: ∂_RΠ_n misses a factor 1/R on Ω_{n−1}; p. 123: 'every power of A_R at most 3/2' is 7/4 as displayed; Young still closes; p. 122, a trap for text extraction: the cutoff family reads φ_{4R}, φ_{8R} in extracted text (dilations, under which three inequalities are false) and φ_R⁴, φ_R⁸ in the PDF glyphs (powers of one bump, under which every step is exact).

The implacable question is not whether the paper reads well but whether a theorem says this cannot happen. The classical obstructions were each set against the construction's own exponents, symbolically, in the battery. None refutes it. One is load-bearing and unstated: for an axisymmetric flow the swirl Γ = r·uθ obeys a drift–diffusion equation with no zeroth-order term, so from rest with a bounded force the swirl stays bounded and |uθ| ≤ C/r; the paper's core has r·uθ = q^{−h}H, unbounded, in its own notation. The axisymmetric background alone is impossible. The theorem survives because the pulses carry nonzero angular frequencies and their Reynolds flux breaks the maximum principle for the angular mean — the physics of the whole construction, and the paper never says so.

A list of asserted steps is only as interesting as its answer in the certificate, so every one was traced into the Lean library and asked a second, harsher question: not "is it discharged" but "is the Lean statement weaker than the paper's claim at that point". 6 are discharged by a proved theorem at full strength, and two of them are stronger than the paper: the endpoint regularity the paper gives as per-order bounds is a genuine smooth extension across t = 1, and the flatness the paper states in one variable is a joint space-time limit, which is exactly the uniformity the reading found missing. 5 are discharged with something altered, and 2 have no counterpart to check. Two of the paper's arithmetic slips are simply absent from the formal object — the exponent ledger carries the term the paper drops, and the comparison argument uses the exponent its own chain gives.

Are the 'sufficiently small/large' parameters explicit numbers in Lean? No. h, N, Λ, C, q_* and the cycle schedule are all existentials or Classical.choice; the only numeric constants are κ = 10⁻⁵, Λ_chart = 4 − √2, X_big = 100, X_i = 110. Nothing in either artifact bounds h numerically.

Is the constructed field non-axisymmetric in Lean (the pulses' nonzero angular frequency)? Yes, and it is proved rather than assumed: the angular mode enters at HarmonicFields.field … (kp : ℤ) (:107); the actual construction fixes angularMode l n : ℤ with the theorem angularMode_ne_zero (ActualInitialization.lean:52). There is no literal ¬Axisymmetric theorem, but the nonzero angular mode is exactly what the swirl maximum principle requires the field to have — the formal object does evade the obstruction the paper never names.

Which theorem asserts the growth, and along what path? ConstructedSlowBase.origin (:892) gives u(t,0) = (1−t)^{−(1/2+h)}·j·e_z and FinalSlowBase.axis_tendsto (:373) sends it to infinity along t ↦ (t,0): the AXIAL component ON the axis. The paper's (10.20)–(10.21) uses a different path, off-axis at r = √(2X_in τ), where the AZIMUTHAL component diverges. Both give lim sup ‖u‖_∞ = ∞; the formal witness is the simpler one, and no Lean theorem bounds the swirl r·u_θ from below.

The same repository carries a second theorem, and it is the more exposed of the two. There exists u₀ ∈ C^∞_{c,σ}(R³) with 0 < T*(u₀) < ∞, whose smooth Euler solution has lim sup ‖∇u‖_{L^∞} = ∞ and ∫₀^{T*} ‖curl u‖_{L^∞} dt = ∞. The Navier–Stokes result is a FORCED breakdown — the force is defined as the residual of a constructed flow. Euler here is unforced: nothing to hide behind. If it stands it is the first finite-time blowup for smooth compactly supported finite-energy 3D Euler.

The step where such arguments die. The solution of the limiting datum is not the limit of the approximants, and Euler's stability constant is exp(C∫‖∇U_j‖_∞) — exactly the quantity that diverges. This is where such arguments usually die. Section 6.2 never compares U_j with U_j'. It compares each U_j with the hypothetical smooth solution u of the limiting datum, under the contradiction hypothesis T*(u₀) > T_∞. For w = U_j − u the only linear coefficient is ∇u (bounded by that hypothesis), the transport by (u+w)·∇ is skew at every derivative order, the cubic term closes under a bootstrap; the Gronwall constant is C·sup‖u‖_{H⁴}, one number fixed before j is chosen. Nothing about U_j enters — not ‖∇U_j‖_∞, not the frequency, not the Gevrey radius. Only the initial difference depends on j, and it tends to zero. Verdict: complete as written; the contradiction hypothesis is used exactly once, to make the constant finite, and never to control the approximants.

Where a flaw would be. The one-sided Hessian bound λ_max ≤ K_B + 1 of (4.29), which makes every displacement boundary-value problem coercive: it needs the sign m·Mv > 0 at every label for τ ≥ 1, and a failure anywhere gives a non-summable increment. The novel analytic device is Claim 2's Gevrey bound on the new particle map, obtained without exponentiating a Lipschitz norm; that is where a flaw would be if there is one.

The two formal shapes. exists_compact_…_singularity matches Theorem 1.1 and is in one respect more precise than the paper: it pins down the solution class that makes T* well defined euler_breakdown_R3 strictly weaker; equating it with blowup needs uniqueness of finite-energy C¹ solutions (the same integration by parts that gives energy conservation) plus Beale–Kato–Majda. That uniqueness FAILS without a decay condition, and the Lean class does impose square integrability and bounded energy — so the two are equivalent for these data. A formalization that dropped the energy fields would make the non-existence true for a reason that has nothing to do with fluids. Note which one carries the energy bound.

Each line is from the document named in it — OpenAI's announcement, Buckmaster's statement, Tao's posts, or a repository's own timestamps — and is held in the pinned corpus. Nothing here weighs them.