The formal statement

What the Lean proof proves, clause by clause, and what a build on one laptop established on 24 September 2026.

A machine-checked proof settles one question and raises another. It settles whether the stated proposition follows from the axioms. It raises whether the stated proposition is the one the prose claims. This page is the second question, for the two Navier–Stokes theorems in the repository openai/NavierStokesAndEuler.

What was run

The repository was cloned, the pinned toolchain installed (Lean 4.34.0-rc2, a fixed Mathlib commit), the Mathlib cache fetched, and lake build run on all three libraries. The build completed with exit code zero.

Item	Result
Navier–Stokes modules	816 files, about 430,000 lines
Euler modules	1,839 files
Build jobs	11,424, all succeeded
Wall time	4 h 28 min on 28 cores (5 h for user time; the two slowest Euler modules took 15 min each)
`sorry` in either library	none
`axiom` declarations	none
Axioms of (C), (D), the paper's Theorem 1.1, and the periodic corollary	`propext`, `Classical.choice`, `Quot.sound` only

The axiom lists were obtained with #print axioms against the built modules. Those three axioms are the standard foundation of Mathlib; sorryAx did not appear. The repository's Comparator challenge, which checks at kernel level that the solution's definitions are identical to an independent reference, was not run: it requires landrun, a Linux sandbox. The textual diff below is the informal version of that check.

Whose statement it is

The formal statement of alternatives (C) and (D) was not written by the authors of the proof. It is a copy of the encoding of the Clay problem in Google DeepMind's Formal Conjectures project, pinned to commit 8bf45ed. Diffing the copy against the upstream file shows only three changes: the placeholders for alternatives (A) and (B) are removed, the namespace is renamed, and two category attributes are dropped. The definitions are otherwise identical. The proof then supplies the two theorems that the reference leaves as sorry. This separation is the point: the people who chose the definitions are not the people who proved the theorem.

The clauses

The theorem for (C), as Lean prints it, is

navier_stokes_breakdown_R3 : ∀ nu > 0,
  ∃ u₀ f,
    InitialVelocityConditionDecay u₀ ∧ ForceConditionDecay f ∧
      ¬∃ v p, NavierStokesExistenceAndSmoothnessRn nu u₀ f v p

Each named condition is a structure whose fields are Fefferman's numbered conditions.

Lean field	Fefferman	Formal content
u₀ div_free, smooth	(2), (3)	$\nabla\cdot u^\circ=0$ everywhere; $u^\circ\in C^\infty$.
u₀ decay	(4)	for every order $m$ and every $K$, some $C$ with $\\|\partial^m u^\circ(x)\\|\le C(1+\|x\|)^{-K}$.
f smooth	(5)	$C^\infty$ on $\mathbb{R}^3\times[0,\infty)$, as a function of $(x,t)$ jointly.
f decay	(5)	every space-time derivative bounded by $C(1+\|x\|+t)^{-K}$ for $t\ge0$.
navier_stokes	(1)	$\partial_t v + (v\cdot\nabla)v = \nu\Delta v - \nabla p + f$ for all $x$ and $t\ge0$, with $\partial_t$ the one-sided derivative within $[0,\infty)$ at $t=0$.
div_free, initial_condition	(2), (3)	$\nabla\cdot v=0$ for $t\ge0$; $v(x,0)=u^\circ(x)$.
velocity_smooth, pressure_smooth	(6)	$v,p\in C^\infty(\mathbb{R}^3\times[0,\infty))$.
integrable, globally_bounded_energy	(7)	$\\|v(\cdot,t)\\|\in L^2$ for each $t\ge0$ and $\exists E\ \forall t\ge0:\ \int\|v\|^2\,dx < E$.

The negation quantifies over all $v$ and $p$ with these properties. Nothing is assumed about the competitor beyond the list: no decay of $v$ at infinity, no growth condition on $p$, no energy inequality. That is stronger than some readings of the prose and is what the paper's Lemma 10.5 pays for with its Riesz-transform control of the pressure.

The periodic theorem replaces the decay conditions by 1-periodicity in each coordinate, requires the force to decay in time only, and requires the pressure as well as the velocity to be periodic, following the erratum to the Clay statement.

Two readings that were made

The time derivative at zero. Fefferman writes the equation on $t\ge0$. The encoding uses derivWithin relative to $[0,\infty)$, so at $t=0$ the equation is imposed with a one-sided derivative. This is the natural reading and it is a reading.
Divergence at non-differentiable points. The divergence is defined as the trace of the Fréchet derivative, which Mathlib sets to zero where the function is not differentiable. For the smooth fields in the theorem this junk value never arises, but it means "divergence-free" alone does not imply differentiability.

From the paper's theorem to the Clay quantifiers

The paper's Theorem 1.1 is encoded separately, in the project's own conventions. Its candidate has zero initial velocity, a force with compact support in $\{t>0\}\times\mathbb{R}^3$, velocity and pressure supported in one compact set $K$ for every $t<1$, a uniform energy bound on $[0,1)$, and speed unbounded in every left neighbourhood of $t=1$: for every $M$ and $\delta$ there are $t\in(1-\delta,1)$ and $x$ with $|u(t,x)|>M$. The theorem, also checked here, is

theorem_1_1 : ∀ ν > 0, ∃ u p f K,
  CandidateProperties ν u p f K ∧ ¬ Nonempty (GlobalFiniteEnergySolution ν f)

A bridge module derives the Clay form from it: the initial datum is the zero field, which satisfies (4) trivially; a compactly supported smooth force satisfies (5); the argument order is swapped from $(t,x)$ to $(x,t)$; and the viscosity is normalized to one by the rescaling on the scales page. The periodic corollary compresses the supports into a quarter cube and sums integer translates, as in Section 10.5 of the paper. The whole chain, from the candidate to the two Clay statements, carries the same three axioms.

What this does not establish

A successful build shows the formal proposition is a theorem of Lean's type theory plus three axioms. It does not show that the 166-page prose is correct, only that a proof of the same statement exists in another language; the prose is the human-readable account and could contain errors the formal proof does not share. It does not show the formal definitions match Fefferman's intent beyond the reading above, which any reader can repeat from the table. And it says nothing about alternatives (A) and (B). The reproduction is nonetheless the strongest check available to anyone with a laptop and an afternoon, and it passed.

Back to what is settled.