LucentFire Reports · independent verification · 12 September 2026

We rebuilt OpenAI's Navier–Stokes proof on a desktop

It compiles. There are no unproven gaps. And the theorem is narrower than the headlines — exactly as narrow as OpenAI's own README says it is.

Checked by Glazier Stillwater · LucentFire, a BenevolentSky LLC service
Subject: github.com/openai/NavierStokesAndEuler · the announcement

BuildPasses11,424 jobs, exit 0

Unproven gapsNonein the proof path

AxiomsStandardthe usual three, nothing added

Does it mean the headline?Noforced case, Clay (C) and (D)

What this is, and what it isn't

Nobody here is a fluid dynamicist. This is not a review of the mathematics, and it makes no judgment about whether the argument deserves the prize.

It is the check a non-specialist can run and almost nobody publishes: does the released artifact build on someone else's machine, does it hide unproven gaps, and does the formal statement say what the headlines say? All three answers are below, with the commands to reproduce them.

What was run

Step	Result
`lake exe cache get`	8,747 mathlib files fetched
`lake build`	11,424 jobs · exit code 0 · 38 minutes
Toolchain	`leanprover/lean4:v4.34.0-rc2`, mathlib pinned to the same tag
Machine	Ryzen 9 7950X · 16 cores · 127 GB RAM · Windows 11
Scale of the proof	2,659 Lean files · 641,332 lines

The gap checks

A formalization can compile and still be hollow. These are the tells, and reading them needs no mathematics.

Tell	Found	Where
`sorry`	5	All inside `ComparatorChallenges/`, whose own header calls them deliberate challenge placeholders. The proof path never imports that module.
`admit`	0	—
`native_decide`	0	Would move trust from the kernel to the compiler
`unsafe`	0	—
declared `axiom`	0	—
“uses sorry” warnings	0	across the whole build

The axiom audit

This is the check that cannot be talked around. Lean reports every assumption a theorem ultimately rests on, so a smuggled hypothesis appears here no matter how the paper is written. Printed by our build, not read from theirs:

'NavierStokes.Comparator.navier_stokes_breakdown_R3'
    depends on axioms: [propext, Classical.choice, Quot.sound]
'NavierStokes.Comparator.navier_stokes_breakdown_periodic'
    depends on axioms: [propext, Classical.choice, Quot.sound]
'Euler.euler_breakdown_R3'
    depends on axioms: [propext, Classical.choice, Quot.sound]
'Euler.exists_compact_smooth_euler_singularity'
    depends on axioms: [propext, Classical.choice, Quot.sound]

Those three are the ordinary foundations of mathematics in Lean. Nothing else was added anywhere in the dependency graph of the headline results.

What the theorem actually claims

The Navier–Stokes result, verbatim from the repository:

theorem navier_stokes_breakdown_R3 (nu : ℝ) (hnu : nu > 0) :
    ∃ (u₀ : ℝ³ → ℝ³) (f : ℝ³ → ℝ → ℝ³),
    InitialVelocityConditionDecay u₀ ∧ ForceConditionDecay f ∧
    ¬ (∃ v p, NavierStokesExistenceAndSmoothnessRn nu u₀ f v p)

The highlighted f is an external force, chosen by the construction along with the initial fluid.

That makes this Clay alternatives (C) and (D) — “breakdown of Navier–Stokes solutions.” They are official routes to the Millennium Prize problem. They are not the unforced global-regularity question most people mean by “the Navier–Stokes problem,” which remains open.

The construction goes further, and says so plainly:

theorem theorem_1_1_with_initial_rest (ν : ℝ) (hν : 0 < ν) :
    ... ∀ t : ℝ, |t| ≤ 3 / 8 → ∀ x : Space,
        u (t, x) = 0 ∧ p (t, x) = 0

The fluid starts at rest — velocity and pressure identically zero for an initial interval — and the chosen force does all the work. Their own file header calls it “unconditional whole-space forced Navier–Stokes blowup.”

The Euler result is the unforced one, and by this reading it is the more striking of the two: smooth, compactly supported, divergence-free initial data whose solution to the unforced Euler equations goes singular in finite time, with no external force anywhere in the statement.

The finding that surprised us

We went looking for the gap between a press release and an artifact. We found one — and it isn't OpenAI's.

Their README names Clay alternatives (C) and (D) in its first paragraph and says “initial data and forcing” in the same breath. The repository is precise about what was proved. The overstatement — “AI solved Navier–Stokes,” unqualified — lives in the coverage.

So the honest summary is the least dramatic one available: a real proof of a real Clay alternative, machine-checked, accurately described by its authors, and widely reported as something larger.

What this check does not settle

Whether the formal statement faithfully captures the Clay problem's intent. That is a mathematician's judgment and this report does not make it. A proof can compile perfectly and formalize a subtly different claim — the one failure mode a build cannot catch.
Whether the formalization covers the whole 166-page paper or the central argument with prose around it.
Anything about the dispute over credit.

Disclosure One party to the reported credit dispute is a researcher at Anthropic, and this check was performed using a model made by Anthropic. The build results above are machine facts and do not depend on that. The framing might, so it is declared.

Reproduce it yourself

git clone --depth 1 https://github.com/openai/NavierStokesAndEuler.git
cd NavierStokesAndEuler
lake exe cache get
lake build

With elan installed, that is the whole procedure.

Checking the largest mathematics claim of the year cost one download and thirty-eight minutes of a desktop CPU. The proof reportedly took ten thousand agents, eighty-eight hours, and about twenty-two million dollars of compute to find.

Finding is expensive. Checking is nearly free. That asymmetry is the whole reason to check.