OpenAI’s announcement of 8 September 2026 states that the work “resolves the Navier–Stokes Millennium Prize problem by establishing statement ‘C’ (and also ‘D’)”, produced by an internal system running “on the order of 10,000 concurrent agents”, and that they “do not intend to claim the Millennium Prize for this result”. CHECKED
Two things follow that are worth stating before any audit. First, this is a breakdown result, not global regularity: it asserts that smooth data can produce finite-time singularity. Fefferman’s (C) and (D) are the negative alternatives, and resolving either resolves the problem. Second, there is no peer review, and no journal submission is mentioned. An announcement plus a repository is the whole of the public record.
A formalized theorem of the right shape can be true and not be the problem. The shape here is
and everything rests on four definitions: the conditions on the initial velocity and the force, and the notion of solution being negated. The logical directions are not symmetric, and this is the whole of the risk:
That second line is the failure mode. It is the same species as WP-104’s finding that Fin 6 was an instance rather than a consequence: a statement that looks like the target and quietly is not.
The challenge file carries a header saying it is copied from Google DeepMind’s Formal Conjectures project at commit 8bf45ed, with “imports, metadata attributes, namespace, and local notation” adapted. That is a checkable claim rather than a reassurance, so it was checked.
Stripping comments, docstrings, attributes, imports, open/ namespace lines and blank lines from both files leaves 80 code lines upstream and 72 in the OpenAI copy. The full unified diff is 17 lines, and the only substantive difference is a deletion: COMPUTED
— the two positive alternatives (A) and (B), which they are not claiming, removed along with their placeholder proofs. Every definition is byte-identical to DeepMind’s: divergence, IsOnePeriodic, InitialVelocityCondition, InitialVelocityConditionDecay, ForceCondition, ForceConditionDecay, NavierStokesExistenceAndSmoothness and both its Rn and Periodic extensions. The breakdown theorem statements are DeepMind’s own sorry-ed challenges, discharged.
The “quietly narrowed” failure mode is closed, and closed structurally rather than by inspection: OpenAI could not have narrowed the target statement, because they did not author it. The audit question moves one layer out, to whether DeepMind’s formalization is faithful to Fefferman — which is a question about a public, independently maintained artifact, and a far better thing for a claim to rest on.
Read against Fefferman’s official statement, the inherited definitions carry his numbered conditions across without visible loss: CHECKED
| Fefferman | Lean |
|---|---|
| (1) the equation on $t \ge 0$ | navier_stokes, with derivWithin on Set.Ici 0 |
| (2) divergence-free | div_free |
| (3) initial condition | initial_condition |
| (4) $|\partial^\alpha u^\circ| \le C(1+|x|)^{-K}$, all $\alpha, K$ | decay : ∀ m K, ∃ C, ∀ x, ‖iteratedFDeriv ℝ m u₀ x‖ ≤ C / (1 + ‖x‖)^K |
| (5) force decay in $x$ and $t$ | decay on ↿f over univ ×ˢ Ici 0, bound $C/(1+\|x\|+t)^K$ |
| (6) $v, p$ smooth on $\mathbb{R}^n \times [0,\infty)$ | velocity_smooth, pressure_smooth — ContDiffOn ℝ ∞ |
| (7) finite, uniformly bounded energy | integrable ($L^2$ at each $t$) and globally_bounded_energy |
Forcing is permitted in Fefferman’s (C) and (D), so the presence of $f$ is not a dodge; and the decay conditions bind the witness, which makes the theorem harder to prove rather than easier.
Across 2,486 Lean files and 616,276 lines, excluding the two ComparatorChallenges reference files, each of which declares in its own header that it retains intentional placeholders: COMPUTED
Note what this is and is not. It is a statement about the source text. It is not a build, not a type-check, and not an axiom report. A file with no sorry in it may still fail to compile.
The repository ships Comparator challenges and instructs the reader to install landrun, lean4export and nanoda_bin before running them. That is worth spelling out, because it is a better arrangement than most formalization claims come with: the proof term is exported and re-checked in an independent third-party kernel (nanoda, not Lean’s own), inside a sandbox (landrun), against a statement file the claimant did not write. Each of those three closes a different way a formalization claim usually goes wrong, and together they mean the axiom question this corpus normally has to ask by hand is answered by the tooling — provided the tool is actually run.
The proof is not verified here. No build was run. The toolchain is v4.34.0-rc2, a different pin from this corpus’s v4.32.0, and building 616,276 lines against a matching Mathlib was out of scope. Nothing above should be read as saying the theorems are proved. OPEN
The Euler side is unaudited. exists_compact_smooth_euler_singularity asserts a compactly supported smooth divergence-free field with finite lifespan, unbounded $C^1$ norm and divergent vorticity integral — Beale–Kato–Majda — and carries a non-triviality clause A.field ≠ 0, which is the clause a sceptic checks first. Its supporting definitions have not been read. OPEN
And the Euler challenge statement is theirs. The structural argument of §3 does not extend to it, and the asymmetry is visible in the two files’ own headers. The Navier–Stokes challenge says it is copied from DeepMind at a pinned 40-character commit. The Euler challenge says it is adapted from the same upstream file at main — no commit — and describes itself as “the whole-space breakdown alternative specialized to zero viscosity and zero external force.” A specialization is authored. Its normalised code lines are consequently not a subset of upstream’s, so on that side there is no diff that could settle the question and no pinned version to diff against. Nothing here says the Euler statement is unfaithful; what it says is that the cheap check available for Navier–Stokes is unavailable for Euler, and the Prop has to be read rather than traced. COMPUTED OPEN
The bridge layer is unread. The solution file proves the challenge statements “using ComparatorBridge adapters”, and adapters are where scope slips. The diff in §3 constrains this usefully — the adapter must land on a Prop it did not author — but the adapters themselves were not examined. OPEN → closed at the statement layer 2026-09-10, §9.
And no mathematical opinion is offered. Whether the argument is correct is not a question this note is competent to answer, and a clean statement layer is not evidence that it is. What is established is narrower and worth having on its own: the thing being proved is the thing that was asked.
Two weeks before the announcement, on 25 August 2026, Lloyd N. Trefethen (Professor of Applied Mathematics in Residence, Harvard SEAS) posted Reflections on the Millennium Problems (arXiv:2608.24965, math.HO). It argues that the Riemann Hypothesis, P vs. NP and Navier–Stokes have each quietly lost much of their original practical leverage, for three different reasons, and have consolidated into “primarily academic challenges”. CHECKED
On Navier–Stokes his reason is that research since 2000 — Chen and Hou in particular (PNAS 122, 2025) — has made the candidate blowup scenarios look ever more special: “the farther removed from ‘wet’ fluid mechanics”, with the necessary initial conditions “too contrived”, and the singularity-forming configurations possibly unstable in themselves. And then, of a resolution that had not yet been announced:
“It is fascinating to speculate what may happen if it is proved that singularities can arise. I think that in this case, the next scientific challenge will be not so much to modify the NS equations to make them more physical, which might have been the original expectation, as to understand why those singularities have so little consequence.”
He is describing, in advance, the exact branch that was taken. That is worth recording for two reasons. It is the strongest available answer to the question this note deliberately does not ask — not is the proof right but what would being right be worth — and it comes from someone with no stake in the announcement, written before it. And it sets the honest register for reading the claim: a (C) result would be a genuine and historic mathematical event whose consequences for fluid mechanics may be close to nil, which is a different thing from either a breakthrough in engineering or a triviality.
Trefethen closes by asking why long-open problems drift toward the theoretical, and speculates: “To resolve a problem one way or another, we need to find a handle to grab it by. Maybe these handles have something to do with what gives a problem, as it were, measurable consequences. Perhaps problems that remain open for a century despite intense efforts to solve them tend to be so smooth that they glide through both our theory and our practice, like neutrinos, hard to catch.”
That is Chapter 26’s argument in another vocabulary. A handle is a ledger: the thing a claim has to produce to be more than a description — a capacity, a cost, or a count that can come back empty. Ch 26 says a framework producing none of the three has not identified a source of order; Trefethen says a problem forbidding little is a problem with nothing to grab. Unlike the resonances WP-29 refuses, these two share a mechanism rather than a number: both are claims about whether a statement has measurable consequences, and both conclude that consequence is what makes a thing tractable. Recorded as a convergence, not as evidence for either.
§7 left three things open. Two of them are settled here, both by reading source rather than by running anything, and both still strictly about the statement.
The submission does not prove anything against the challenge file. It proves against NavierStokes/ComparatorDefinitions.lean, whose header explains why: the adapters’ import closure must contain no reference placeholders. That module is the place a narrower statement would enter if one were going to, so it was normalised and compared line for line against the challenge file. COMPUTED
Nothing is added. The Props the proofs are stated against are the ones the claimant did not author, and the adapter has no room to introduce a weaker solution notion or a stronger data condition, because it introduces nothing at all. ComparatorSolution.lean then restates (C) and (D) under the reference names and calls #print axioms on both. That the two calls are there is checked here; what they print is not, and no build was run.
(C) is existential in the initial velocity, so what is supplied for u₀ decides how strong the instance is. In ComparatorR3Theorem.lean it is supplied as fun _ => 0 — the zero field, with its decay obligation discharged by a lemma rather than assumed. COMPUTED
By §2’s asymmetry that is a strengthening: conditions on the data make a theorem harder, never easier, and the zero field is the least contrived initial datum available. Forcing is present, as Fefferman’s (C) and (D) permit and as §4 already recorded — and what this is not is unforced blow-up. Nothing in this note says otherwise.
On 9 September 2026 Olga Holtz (Professor of Mathematics, UC Berkeley) published a public assessment of the announcement that asked, among other things, for independent scrutiny of “whether the formal statement matches the intended theorem.” That is the question this note was written to answer, asked independently and a day later, which is the best evidence available that it was the right question. Her reading of the construction — a three-dimensional incompressible fluid at rest, forced, energy bounded, the force smooth through the singularity — agrees with §4 and with the witness above, and prompted the two checks in this section. CHECKED
Her note also raises questions of research priority and provenance of the discovery, including concerns attributed to others. Those are outside this note’s scope and are not adopted here. This paper audits a statement against an upstream file; it has no instrument for adjudicating credit, and relaying an allegation is not auditing it. The distinction Holtz draws is the one this paper depends on: a verified theorem can settle a mathematical question and cannot, by itself, settle scientific credit. §3’s finding is provenance of the statement and says nothing about provenance of the proof.
§9 closed by naming what it could not reach: “That the two calls are there is checked here; what they print is not, and no build was run.” That sentence is now out of date, and not because anything was built. The repository states the answer in a file this note had not read. COMPUTED
Audited at HEAD f9e8bc5, 2026-09-10, toolchain leanprover/lean4:v4.34.0-rc2: 2,659 Lean files, 641,332 lines — Euler/ 1,839 files and 211,578 lines, NavierStokes/ 816 and 429,279, ComparatorChallenges/ 2 and 472.
The repository root carries formalization.yaml, declaring itself against the mathlib-initiative formalization.schema.json at v0.4. For each of the four headline declarations it records the file, the declaration name, a sorry_count, and an explicit axiom list. All four entries are identical in the last two fields: COMPUTED
The same file records review: status: “self-assessed” and, under automation, method: agent, models: GPT-6 Astra, framework: Codex. The absence of peer review that §1 had to infer from the announcement is declared in the repository, in the same machine-readable file as the axiom list.
Both Comparator configurations carry a permitted_axioms field holding exactly those three names. That is a stronger object than a printed list: the independent checker is told what the proof is allowed to depend on and fails if it depends on more, so the axiom discipline is a gate in the verification pipeline rather than a line of output a reader is trusted to notice. COMPUTED
The five live in the two challenge files, whose own header calls them intentional placeholders, and §9 established the firewall from the other side: the solution adapters import ComparatorDefinitions and never the challenge module. A sorry in this repository cannot reach a headline theorem by construction, and the declared sorry_count: 0 is consistent with that architecture rather than with an assertion about it.
Journal Vol. Ω No. 9 argued that the axiom line goes unquoted because the vocabulary for it does not exist, and cited the Fermat formalization having to spell the three axioms out in prose — “because there is no standard citation for them.” There is one, and it is in use. A schema with a per-declaration axioms: field, published under the mathlib initiative and populated here alongside sorry_count, automation disclosure and review status, is the layer that page said did not exist yet. It existed while the page was being set. CHECKED
The revised claim is narrower and survives: the habit forms where the stakes are high enough to require it, and this is the highest-stakes formalization of the month. What Vol. 9 should have said is that the layer is new and unevenly adopted, not absent — and that the interesting census is no longer how many projects print the line, but how many populate the field.
A declared axiom list is a claim in a metadata file. It is not kernel output, and reading it is not running it. Everything in this section is a statement about what the repository says about itself — consistently, in three places, in a form designed to be checked — and the check itself still requires lake build and the four #print axioms calls that §9 found in place. This note has now declined to run that build three times. That is a limit of the note, not a finding about the proof. OPEN
The proof layer remains unaudited here, and nothing in this section speaks to it. What §10 adds is that the disclosure layer of this submission is, on the evidence of its own files, better than the practice the corpus has spent two pages complaining about.
[1] OpenAI, “Navier–Stokes solution”, announcement, 8 September 2026.
[2] github.com/openai/NavierStokesAndEuler — audited at HEAD, 9 September 2026.
[3] github.com/google-deepmind/formal-conjectures,
FormalConjectures/Millenium/NavierStokes.lean at commit
8bf45ed70d48b2b2a501de9c00b26bfa38c573ee — the upstream statement.
[4] L. N. Trefethen, “Reflections on the Millennium Problems”, arXiv:2608.24965v1
[math.HO], 25 August 2026 — Harvard SEAS; the RH zero count (12,363,153,437,138 on the
critical line), the P vs. NP typical-case argument, and the Navier–Stokes “so little
consequence” passage.
[5] J. Chen and T. Y. Hou, “Singularity formation in 3D Euler equations with smooth initial
data and boundary”, Proc. Nat. Acad. Sci. 122 (2025).
[6] C. L. Fefferman, “Existence and Smoothness of the Navier–Stokes Equation”,
Clay Mathematics Institute official problem description.
[7] github.com/leanprover/comparator; nanoda, an independent Lean kernel.
[8] This corpus: WP-29;
WP-30; WP-104;
Book 4 · Ch 26.
[9] O. Holtz, public assessment of the Navier–Stokes announcement, 9 September 2026 —
quoted at §9 for the request for statement-level scrutiny and for the description of the
construction; its priority and provenance claims are noted as out of scope and not adopted.
[11] formalization.yaml at the repository root, schema v0.4, mathlib-initiative/formalization.yaml — the per-declaration axioms, sorry_count, automation and review fields read at §10; and ComparatorChallenges/{Euler,NavierStokes}.json for permitted_axioms.
[12] This corpus: Journal Vol. Ω No. 9, “Two Instruments, Thirty Years, Neither Quoted” — the claim §10 corrects.
[10] Every COMPUTED figure in this note is regenerated by
wp107-verify.py, standard library only. Blocks [1]–[4] fetch the two
statement files; blocks [5]–[6] need a checkout and report SKIPPED without one:
python3 wp107-verify.py --repo NavierStokesAndEuler.
§3, the copy’s line count. Read 71; the count is 72 under the normalisation this note states. The 71 came from additionally dropping variable {n : ℕ}, which binds the dimension in every definition below it and is statement content rather than scaffolding. The diff length of 17 lines, and the finding that every changed line is a deletion, are unaffected.
§5, the exclusion. Read “the challenge reference file”, singular. There are two, and the Euler one carries the only two sorrys in the repository. Both are excluded on the same stated ground and not a wider one: each declares its placeholders intentional in its own header.
Both figures are now assertions in wp107-verify.py and cannot decay silently a second time.