On 8 September 2026 a Lean 4 development appeared whose kernel accepts a proof of finite-time breakdown for the three-dimensional Navier-Stokes equations with a smooth, compactly supported force and zero initial velocity, on all of space and on the periodic box. Those are Clay alternatives (C) and (D). On the same day a second group released kernel-checked forced blow-up for the incompressible porous media equation, two-dimensional Boussinesq and three-dimensional axisymmetric Euler. Within seventy-two hours the two most prominent voices in the field were saying in public that unforced blow-up should now be expected too.
We build a database, not fluid theory, so this article does the thing a database company can do with precision.1 It states exactly what has been established and what has not, with dates. It reports what we did to check the published development, with the host, the time and the exit code of every step. And it explains why that work belongs in a database rather than in a blog post.
What is established, as of 11 September 2026
- Clay alternatives (C) and (D), breakdown with smooth forcing, are established by a Lean 4 proof the kernel accepts against a statement that a third party wrote before the proof existed.2 The formal statement lives in Google DeepMind's Formal Conjectures project, pinned at a July 2026 commit, and the proof is matched to it by the Lean community's Comparator tool under two independent kernels. The written argument is purely analytic. There is no numerics and no interval arithmetic in the paper.
- Unforced three-dimensional Euler blow-up from smooth compactly supported data is kernel-checked by the same authors. Its challenge statement is the authors' own, with no third-party upstream, so residual statement-fidelity risk concentrates here.
- Forced blow-up for IPM, 2D Boussinesq and 3D Euler is published by a second group with Lean certificates for two of the three. Their Boussinesq certificate is the relevant precedent for machine-decided interval arithmetic in a fluid proof. They do not claim Navier-Stokes, and we do not represent them as doing so.
What is open
- Clay alternatives (A) and (B), unforced global regularity or unforced blow-up. Untouched by every result above. A compactly supported force satisfies the decay conditions for free, so a forced counterexample says nothing about the unforced problem.
- Removing the force from either construction. The one concrete objection on record, posted publicly on 8 September, is a scaling argument that viscous depletion outruns instability growth along a lacunary frequency sequence in three dimensions. The reply was to study a dyadic model with Boussinesq scaling first.
- A specialist reading of the formal statement. No PDE specialist had signed off on the Formal Conjectures encoding of the Clay text in the sources visible to us. Our own machine-assisted audit of it is the subject of a separate article in this series.
- The Prize. The Clay Mathematics Institute said on 10 September that the problem has apparently been settled and that its evaluation would be deliberately unhurried. The rules require refereed publication followed by a two-year period. The authors have said they will not claim the Prize. Nothing is awarded and nothing is awardable yet.
What we did, with receipts
We rebuilt the published development from source on a machine we control, audited what the two headline theorems depend on, matched the proofs to the pinned challenge statements with the Comparator, and replayed the full import closure of each solution through the kernel from scratch.3 Every step is recorded as a typed verification event with the host, the UTC time and the exit code,4 and those events are what derive the trust tier of the corresponding statement in our evidence twin.
| Event | Outcome | UTC, 11 Sep 2026 | Fact recorded |
|---|---|---|---|
| Static audit | Pass | 13:55 | 2,659 Lean files, 641,332 lines, zero axiom declarations, no unsafe escape hatches, placeholders only in challenge files |
| Statement fidelity | Pass | 14:05 | Challenge file diffed against the Formal Conjectures pin: cosmetic differences only |
| Independent build, Navier-Stokes | Pass | 14:27 | 816 files, about 13 minutes |
| Axiom audit, Navier-Stokes | Pass | 14:27 | Both theorems depend on exactly propext, Classical.choice and Quot.sound |
| Comparator match, Navier-Stokes | Pass | 14:41 | Accepted by the nanoda kernel and the Lean default kernel, 14 min 59 s |
| Independent build, everything | Pass | 14:44 | 11,424 jobs, zero failures |
| Axiom audit, Euler | Pass | 14:44 | Same three axioms |
| Comparator match, Euler | Pass | 16:11 | Same acceptance lines, 13 min 38 s |
| Fresh kernel replay, Navier-Stokes | Pass | 16:59 | Full import closure replayed from scratch, exit 0, 23 min 53 s, about 7.8 GB resident |
| Fresh kernel replay, Euler | Pass | 17:44 | Exit 0, 35 min 38 s |
Why this is a database story
The frontier of an open problem is a graph of statements with evidence attached, and the evidence changes weekly. Statements imply other statements, so a conclusion can never be more established than the weakest premise beneath it. Some statements are open, and an open statement is not a null; it is a typed gap with a cost, a trigger and a falsifier. Some evidence is a registry record, some is a self-report, some is a kernel event you generated yourself, and each kind earns a different tier. When one statement is retracted, everything that rested on it must fall with it, automatically.
Those are storage properties. In 8DB the September frontier is twenty typed atoms, nine implication edges whose restriction maps refuse at write time to let a conclusion outrank its premise, eleven connected components, six typed gaps, and a retraction query that, when pointed at the Navier-Stokes theorem, drops exactly Clay (C) and Clay (D) and nothing else. The tiers are never assigned by hand. They are derived from the events in the table above and from records ingested losslessly from the two public registries that track formal results. The rest of this series takes each of those mechanisms apart.
What we would like from you
- A PDE specialist's reading. Five items remain on the sign-off list for the formal statement, and none of them can be produced by a tool. If you can read the Clay text and the Lean encoding side by side, we will give you the clause-by-clause audit as the starting point.
- An external kernel. Both solutions have been replayed through the Lean kernel and the nanoda kernel. Nobody has yet run them through a third independent checker on this toolchain. If you maintain one, we would like to record the event.
- Your open problem. If you run a research programme whose frontier is a graph of claims with evidence attached, the twin is built for that shape and not for fluids in particular.
Write to hello@8braid.com with the subject "Navier-Stokes evidence twin: frontier review". You will hear back from an engineer.
Sources and further reading
- Clay Mathematics Institute: Navier-Stokes Equation, official problem description
- openai/NavierStokesAndEuler on GitHub, the Lean 4 development
- google-deepmind/formal-conjectures, the pinned Navier-Stokes statement
- tristanbuckmaster/fluid_lean, forced blow-up for IPM, Boussinesq and Euler
- leanprover/comparator, the trusted-statement matching tool
- Public objection on viscous depletion versus lacunary growth, Mathstodon, 8 September 2026 and the reply proposing a dyadic model, 8 September 2026
- Beale, Kato and Majda, Remarks on the breakdown of smooth solutions for the 3-D Euler equations, Comm. Math. Phys. 94 (1984)
- 8DB: Every Number on This Site Has a Harness
Every landscape statement above is dated 11 September 2026 and describes sources visible to us on that day. "Kernel-checked" means a Lean kernel accepted a proof against a pinned statement; it is not a claim that the result is verified, refereed or awarded. 8Braid has no affiliation with the Clay Mathematics Institute, OpenAI, Google DeepMind or any author named or referenced here, and makes no mathematical claim about the Navier-Stokes equations.
Footnotes
-
Nothing in this article is a judgement on the analysis. 8Braid is not qualified to referee the mathematics and makes no mathematical claim of its own; what follows is a record of what was checked, by which tool, on which day. ↩
-
The words we will not use. A Lean result is kernel-checked against a pinned statement. That is the whole of what a kernel acceptance tells you, and it is a great deal. It is silent on whether the pinned statement says what the Clay text says, on whether the kernel itself is sound, on who found the argument and when, and on whether the field agrees the theorem matters. So we do not write "verified" for anything we did, we do not write "proved" for anything we did, and we do not write that Navier-Stokes is solved. The formulation we use in every record is: Clay alternatives (C) and (D), with smooth compactly supported forcing and zero initial data, are established by a kernel-checked Lean proof against a third-party statement written before the proof; Clay is evaluating; alternatives (A) and (B) are open. ↩
-
Rebuilding someone else's Lean project is a commodity step, and at least five other parties had done it by 11 September. It enters our record as an event that promotes a tier, never as a headline. ↩
-
Host: WSL Ubuntu 24.04, 16 vCPU, 30 GB, Lean 4.34.0-rc2, pinned commit of the published repository dated 10 September 2026. The sandbox ran in best-effort mode because the WSL kernel exposes an older Landlock ABI; that caveat is carried in the recorded confidence interval, and the interval's upper bound stays below 0.99 while there is no refereed publication. ↩
Continue the technical conversation
Where could this help your work?
Bring a research question, a database workload or an application you want to build. Let’s connect the ideas in this article to an evaluation that matters to your team.
Discuss this work