Navier–Stokes, 8 September 2026

OpenAI published a note and a Lean formalization that it says establishes Clay statements C and D. DIU OS rebuilt that public artifact on one pinned revision. The case stays inconclusive. A status on one layer is not the status of the case.

Why this page exists

DIU OS uses the tools OpenAI published with this claim: Lean 4, Lake, and the public repository. The page does not set out to refute the proof, and it does not adopt the headline.

The manifesto states the rule. What is computed is a checkable status of a claim — relative to explicit assumptions, the model, the computation, and the evidence. “Truth is computed, not asserted” names that mission. It does not stamp a run as true.

A gene is where that rule becomes an object someone else can rerun: the equation, the source, what the model leaves out, and one check. This record is the same discipline applied to a claim we did not write. Constitution §1.1 and §1.2.

Why there are four statements

The Clay problem, in Charles Fefferman’s official statement, asks for a proof of one of four alternatives. Any one of them meets the problem as written. An external force does not make C or D a different problem: the statement lists them.

(A) Whole space, no external force. A smooth solution with finite energy exists for all time.

(B) Periodic torus, no external force. A smooth solution exists for all time.

(C) Whole space, a smooth force is allowed. There exist smooth data and a smooth force for which no such global solution exists.

(D) Periodic torus, a smooth force is allowed. There exist smooth periodic data and a smooth force for which no global smooth solution exists.

The independent challenge text (Google DeepMind, pin 1cbcb19a) says the same thing in Lean. On that pin, A and B still carry sorry and are marked research-open. OpenAI’s repository also contains a finite-time singularity for the Euler equation, which has no viscosity. Euler is not one of the four Navier–Stokes statements.

The analytical note describes a fluid that starts at rest, under a smooth force, with kinetic energy staying finite, while the maximum speed becomes unbounded as time approaches 1. The authors assign the whole-space result to C and the periodic corollary to D. This page does not re-derive that construction.

How the check was run

Pin the bytes. Checkout f9e8bc5b38b6e212696e8a30e3e91517af887bbd. Toolchain leanprover/lean4:v4.34.0-rc2. Mathlib 85e3a25e006c35636f0e53b0e9296caca2685bc0. The challenge citation one commit behind this pin is 8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538.
Read the sources before trusting a grep. On 18 September a line scan found no tactical sorry in NavierStokes/ or Euler/, four intentional placeholders in ComparatorChallenges/, and no added axiom, native_decide, or unsafe.
Compare definitions with the challenge text. The C and D wording and the eleven shared definitions match that file textually. Elaborated types of those definitions matched byte for byte on the same machine. The project’s Comparator exporter was not run.
Rebuild with the checker the authors publish. On 19 September, operator Bakhtiyor Ruzimatov, one x86 Linux workstation: lake build NavierStokes Euler, LEAN_NUM_THREADS=2, about 4 hours 47 minutes, 11421 jobs, exit code 0.

Earlier the same day, a build of the statement targets only (lake build NavierStokes.ComparatorDefinitions ComparatorChallenges.NavierStokes) finished 8764 jobs. Wall-clock time for that pass was not written down.

The rebuild did not call a language model. No token count was measured, and none is reported. Announced figures for agents and tokens are the authors’ statement. The repository has no trace of them, so they are not entered here as a result of this check.

What the kernel printed

NavierStokes.Comparator.navier_stokes_breakdown_R3
  axioms: propext, Classical.choice, Quot.sound
NavierStokes.Comparator.navier_stokes_breakdown_periodic
  axioms: propext, Classical.choice, Quot.sound
Euler.euler_breakdown_R3
  axioms: propext, Classical.choice, Quot.sound
Euler.exists_compact_smooth_euler_singularity
  axioms: propext, Classical.choice, Quot.sound

Those three names are Lean’s standard logical basis. They are not an extra axiom that the Navier–Stokes claim is true. Derivability of these four names does not transfer to Fefferman’s prose, to a Clay decision, or to the credit dispute.

Where the code is, and where it is not

The Lean sources stay in openai/NavierStokesAndEuler at this pin. This site does not copy them.

There is no GitHub Actions run and no GitHub Release of this check. The builder log was a local file and is not retained. A run number that does not exist is not evidence.

A third party repeats the rebuild from the public pin:

git clone https://github.com/openai/NavierStokesAndEuler.git
cd NavierStokesAndEuler
git checkout f9e8bc5b38b6e212696e8a30e3e91517af887bbd
lake build NavierStokes Euler

What stays open

Whether the Lean statement is Fefferman’s statement. Comparator was not run. That reading needs people, not another exit code.
Clay’s recognition. The Institute looks after peer-reviewed publication and further community vetting. OpenAI says it does not intend to claim the prize.
Credit, private sessions, and the search trace. Those records are not in the repository. Nature reported the dispute on 17 September 2026.

The layer-by-layer vector, including what 8Braid and others published, is on diu-os.com/#/claims/navier-stokes.