Their theorem, read to the last hypothesis.

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 matters 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; the repository contains the general lemma (a smooth compactly supported force gives a uniform L² bound on [0,1)) and nothing invokes it, and the structure that would carry the bound has 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 stands and the physical headline is a paper claim.

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 reads as an oversight rather than an obstacle, and why the unused lemma in R3/CompactEnergy.lean is the tell.

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.