When the Lean kernel accepts a proof, exactly one thing has been established: the term the authors wrote has the type the statement declares. Everything else about the result is a separate question. Is the kernel sound? Does the statement say what the mathematicians think it says? Does the mathematics community agree the theorem is the one that matters? The first is addressed by replaying through independent kernels. The third is addressed by referees. The second, statement fidelity, is the residual risk that formal verification does not remove, and in September 2026 it sat under a Millennium Prize problem.
The Navier-Stokes breakdown proof was matched by the Lean community's Comparator tool against a statement in Google DeepMind's Formal Conjectures project, written in May 2026 and pinned at a July commit, well before the proof existed. That separation of statement author from proof author is the right design. It still leaves the question of whether the Lean text encodes the Clay Institute's prose. So we audited it.
How the audit was scored
The Clay text for alternatives (C) and (D) has eleven numbered conditions plus errata, and the two alternatives assert that some smooth data and force exist for which no smooth bounded-energy solution exists. For a breakdown theorem the safe directions are asymmetric. On the data side, the Lean class must be a subset of Clay's class, because exhibiting data from a smaller class is a stronger result. On the solution side, the Lean class must be a superset, because non-existence in a bigger class is stronger. Any clause where the Lean class could be smaller on the solution side or larger on the data side is a concern, not a cosmetic difference.
Each clause was scored Faithful, Equivalent With Argument, or Weaker Than Clay, with a direction and a falsifier written down at scoring time.
The results
| Clause | Clay condition | Verdict |
|---|---|---|
| C-D-0 to C-D-3 | Smooth divergence-free datum, the equation, the divergence constraint, the initial condition | Faithful |
| C-4 | Decay of every mixed partial of the initial datum | Equivalent, now kernel-checked |
| C-5 | Decay of every mixed space-time partial of the force | Equivalent, now kernel-checked |
| C-6 | Solution smooth on the closed half-space | Equivalent with argument; flagged ambiguous |
| C-7 | Bounded energy | Faithful |
| D-8, D-10 | Periodicity of data and of the solution | Faithful |
| D-9 | Time decay of the periodic force | Equivalent, now kernel-checked |
| D-11 | Smoothness in the periodic case | Same as C-6 |
| D-errata | Pressure periodicity | Concern |
| Logical form, zero datum, junk values, weak-solution sign | The existential shape, the exhibited zero datum, guards against vacuous satisfaction | Faithful |
Sixteen of seventeen clauses are faithful or equivalent. The one concern is real and specific. The Lean statement of (D) requires the pressure to be periodic. The Clay text of 2000 does not; a periodic velocity admits a pressure with a non-periodic linear drift in space, which the Lean class excludes. The Lean solution class is therefore smaller than Clay's, which for a breakdown theorem is the concern direction. The requirement follows the Clay Institute's own published errata, and the (D) proof consumes the field, so this is not cosmetic. It does not touch (C), on which the headline result rests. In the evidence twin it reduces the upper bound of the interval on Clay (D) from 0.98 to 0.956 and opens a typed gap whose trigger is a ruling from the Institute.
Replacing English with lemmas
Three clauses, C-4, C-5 and D-9, were scored Equivalent With Argument. The Clay text bounds every mixed partial derivative of every component of a vector field, for every order and every polynomial weight. The Lean encoding bounds the operator norm of the iterated Frechet derivative instead. The statement's author had noted this as the largest divergence he knew of and argued that finite-dimensional norm equivalence made the two the same, and asked for a double check. No Lean lemma of that equivalence existed.
We wrote one. The file contains twenty-two theorems in the Formal Conjectures project's own namespace. The three headline statements say that the operator-norm bound holds for all orders and weights if and only if the Clay bound holds for every mixed partial of every component, where the partial is the iterated derivative applied to a tuple of standard basis vectors and read at one coordinate. The argument is elementary: basis vectors have norm one, the operator norm is bounded by a finite sum over basis tuples, components are bounded by the norm and the norm by the sum of components, and constants are summed over the finitely many tuples and components. It is generic over any finite family of unit vectors spanning the space. It was built against the pinned statement with warnings as errors, and every one of the twenty-two theorems depends only on propext, Classical.choice and Quot.sound.1
Two things about that lemma matter more than the lemma. First, it is a property of two phrasings, kernel-checked, and the record says so: it changes no confidence interval and moves no atom toward a solution of the problem. Second, it turns a sentence in a sign-off list into a falsifier a machine can run: the module failing to build against the pinned statement, or its axiom list growing, would re-open the clause. The sign-off list dropped from six items to five.
What remains for a human
The five remaining items cannot be produced by a tool, and the record says which they are: a specialist reading of the smoothness clause, since a weaker reading of "smooth on the closed half-space" would enlarge the solution class; a ruling from the Institute on the pressure-periodicity errata; a ruling on whether a zero initial datum with nonzero force is admissible, which the proof exhibits; a review of the two bridge files that connect the authors' proof to the challenge statement; and confirmation of a second senior endorsement of the statement. Our audit is the input to those judgements.2
Why the database matters here
A fidelity audit is only useful if it stays attached to the statement it audits, survives the statement being relabelled or re-pinned, and degrades the confidence of everything downstream by exactly the right amount. In 8DB each clause is a typed verdict with a falsifier on the edge from the theorem to the Clay alternative it implies; the one concern reduces the upper bound on (D) and nothing else; the three kernel-checked equivalences are recorded as a verification event that raises no tier by rule; and when the Formal Conjectures project relabelled (C) and (D) as solved on 11 September, the diff against our pin was recorded as its own event, showing that only docstrings and attributes changed. Nothing in the audit lives in a spreadsheet or a paragraph. It lives on the graph.
What to bring us
- Your reading of clause (6). If you work in PDE and can say whether smoothness on the closed half-space is the intended class, that single judgement closes one of the five items.
- A statement you have formalised. If you maintain a formal encoding of an informal problem, we will run the same audit shape against it and give you the clause table.
- The generic lemmas. Ten of the twenty-two are pure multilinear and Euclidean facts. If you want them upstream, tell us where they belong.
Write to hello@8braid.com with the subject "Statement fidelity audit: Navier-Stokes". You will hear back from an engineer.
Sources and further reading
- Clay Mathematics Institute: official problem description, with errata
- google-deepmind/formal-conjectures, FormalConjectures/Millenium/NavierStokes.lean
- leanprover/comparator
- Mathlib documentation: iteratedFDeriv and iteratedFDerivWithin
- 8DB: The Week Navier-Stokes Moved, and What a Database Company Did About It
- 8DB: What an Independent Evaluator Should Be Able to Run
The audit described here is machine-assisted and was not performed or signed off by a PDE specialist. "Kernel-checked" means a Lean kernel accepted the lemmas against the pinned statement on 11 September 2026 on a Windows 11 host with Lean 4.33.1; it is not a claim that anything is verified in a broader sense. The lemmas concern the equivalence of two phrasings of decay conditions and make no statement about the Navier-Stokes equations. 8Braid has no affiliation with the Clay Mathematics Institute, Google DeepMind, OpenAI, the Lean community or any author referenced here.
Footnotes
-
Kernel-checked against the pinned Formal Conjectures statement on 11 September 2026, on a Windows 11 host with Lean 4.33.1, with warnings as errors. The lemmas are a property of two phrasings of decay conditions; they make no statement about the Navier-Stokes equations and are not a claim that anything is verified in a broader sense. ↩
-
The audit is machine-assisted, not a specialist sign-off. It is not a substitute for any of the five remaining judgements, and the record labels it machine-assisted rather than specialist. ↩
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