Shortly before midnight on 7 September 2026, Tristan Buckmaster, a mathematician at NYU, published a four-page statement, three preprints and a Lean repository. At noon on 8 September, OpenAI reported that an internal model had solved the Navier-Stokes existence and smoothness problem, one of the seven Millennium Prize Problems. Twelve hours lie between the two publications, and inside them sits a dispute about who saw what, and when. "Navier-Stokes solved" is the question that gets typed; the honest answer has three parts that the coverage merges into one. Is the proof correct? Whose method is it? What did the vendor's systems see of the other side's work? Only the first question has an instrument. A Lean checker ran for 17 hours and settled it. The other two are governance questions, and I read the case as a governance case, because they are exactly the questions a team faces the moment it has put unpublished work into a vendor's coding agent. My position: nothing that happens after the announcement answers them. They are answered before the first prompt, by a plan, a setting and a contract, or they stay open.

What is the Navier-Stokes problem?

The Navier-Stokes problem asks whether the solutions of the three-dimensional incompressible Navier-Stokes equations with smooth initial data stay smooth for all time, or whether a solution can develop a singularity: a finite point in time at which the fluid's velocity grows beyond every bound. The Clay Mathematics Institute put the question on its list of seven Millennium Prize Problems in 2000, one million dollars per problem. The official problem description by Charles Fefferman offers four alternative statements to choose from and says so explicitly: "we ask for a proof of one of the following four statements".

The equations are Newton's second law, written for a fluid that is treated as a continuum rather than as molecules, with a viscosity term for internal friction and an optional external force f (gravity, a propeller). The four statements differ in two switches, the domain and the force:

StatementDomainExternal force fClaimStatus, 13 September 2026
(A) Existence and smoothnessR³f = 0For every smooth, decaying, divergence-free initial velocity, a smooth solution with bounded energy exists for all timeopen
(B) Existence and smoothnessR³/Z³ (periodic box)f = 0The same for periodic initial dataopen
(C) BreakdownR³smooth f allowedThere exist a smooth initial velocity and a smooth force for which no smooth solution with bounded energy exists for all timeOpenAI, Theorem 1.1, Lean-checked
(D) BreakdownR³/Z³smooth f allowedThe same, periodicOpenAI, Corollary 10.6, Lean-checked

Two things follow from the table, and both are missing from most reports. (A) to (D) are not four stages of one task but four doors, and Clay accepts whoever opens one of them. And (C) and (D) do not contradict (A) and (B): a fluid that a smooth external force can drive into a singularity says nothing about a fluid that is left alone. The question without a force, the one most analysts mean when they say "Navier-Stokes", stays open; Terence Tao wrote on 7 September: "it should even be possible to do without the forcing term" (Tao, 2026). The route through a smooth force is also the route Buckmaster means: the one "Luis and Diego opened and the one Levent and I had quietly chosen to attack. Almost nobody else I know of was working on it" (Buckmaster, 2026).

Is the Navier-Stokes problem solved?

By Clay's text yes, by Clay's procedure not yet, and the distance between the two is measured in years. There is a precedent. Poincaré stated his conjecture in 1904, Perelman published his proofs on arXiv in 2002 and 2003, Clay awarded the prize on 18 March 2010 (Clay Mathematics Institute), and Perelman declined it (phys.org, 2010). Seven years from preprint to prize is the institute's tempo, and its rules are written for it: "CMI does not accept direct submission of proposed solutions", publication in a qualifying outlet, "At least two years must have passed since publication", "general acceptance in the global mathematics community". OpenAI's paper is a PDF on a CDN; the clock is not yet running, and OpenAI says it does not intend to claim the prize: "We do not intend to claim the Millennium Prize for this result" (OpenAI, 2026). "Solved" is correct by Clay's text and premature by Clay's procedure. Both halves count.

What did OpenAI prove?

OpenAI's paper "Finite time blowup for Navier–Stokes" (166 pages, 8 September 2026) states as Theorem 1.1: for every positive viscosity there is a smooth external force with compact support in space and time under which a fluid starting from rest develops an unbounded velocity before time 1 while its kinetic energy stays bounded; the compact support makes it possible to transplant the construction into the periodic box, which yields (D) as Corollary 10.6 (OpenAI, paper). Written out, the statement has six components, and each corresponds to a part of Fefferman's (C):

Theorem 1.1 (OpenAI, 2026-09-08)
Viscosity:  ν > 0, arbitrary
Force:      f ∈ C_c^∞(R³ × (0,∞); R³)
            smooth, compact support in space and time
Start:      u(·, 0) = 0
            fluid at rest
Support:    supp u(·,t) ∪ supp p(·,t) ⊂ K
            one compact set K, for all 0 ≤ t < 1
Energy:     sup_{0≤t<1} ‖u(t)‖_L² < ∞
            kinetic energy bounded
Blowup:     lim sup_{t↑1} ‖u(t)‖_L∞ = ∞
            velocity unbounded before t = 1
=> no smooth solution with bounded energy
   on R³ × [0,∞): statement (C)
=> compact support: the same construction
   on T³ = R³/Z³: statement (D)

The picture OpenAI supplies is a vortex that winds inward and stretches along its axis "like spaghetti", shrinking and speeding up as it goes, while the terms of the equation grow large and cancel so precisely that the external force stays smooth. The Lean formalization lives in the repository openai/NavierStokesAndEuler (Lean 4.34.0-rc2, Mathlib); its README names both results as alternatives (C) and (D) and ships instructions for independent checking with Comparator.

How the proof was found counts for everything that follows, so here is OpenAI's own account. Since 28 August the company had been training a new internal model, "significantly more capable than GPT‑6 Astra", the model presented on 3 September. For Tuesday 1 September, OpenAI notes: "we heard rumors that two Millennium Prize problems had been resolved", and a run at all open Millennium problems began. The agents ran in groups, could read a cached copy of the internet and execute code; separate groups were given the (A)/(B) and (C)/(D) variants. A side task fell first, the Euler equations without a force (viscosity zero): "Nearly 100 agents worked together for approximately 50 hours", a 57-page paper. OpenAI then pulled agents off the other problems, gave them the Euler solution as a starting point ("prompted these agents with the Euler resolution"), switched to a further-trained model during the run and merged the groups: "cross-pollinated the agent groups by using Codex to consolidate the most useful insights from each agent group". The Navier-Stokes group comprised "on the order of 10,000 concurrent agents"; the result arrived on Saturday 5 September, about 88 hours after the start; "Lean formalization and verification took an additional 17 hours via GPT‑6 Astra". The run sent 2.7 million messages and consumed about 130 billion output tokens (OpenAI, 2026).

Two details of this account carry weight later. The run began on a rumor, four days after the model's training began. And the run was steered: humans decided which result which agents would get, and Codex, the product, merged the intermediate results. OpenAI adds that it kept "the same strict safeguards that we apply to all our frontier model evaluations, including monitoring and isolation"; what a swarm of OpenAI agents does with less of both is documented in the post on the OpenAI Hugging Face incident from July.

What does the Lean proof assistant check, and what does it not?

Lean is a proof assistant: a small, auditable kernel checks whether every step of a formal proof follows, by the rules of logic, from earlier steps and from the definitions and theorems of the Mathlib library. When the project builds, the formal statement is a theorem. A green build says nothing more. It does not say that the formal statement is the intended one, not who had the idea, and not where the inputs came from.

The first gap is a reading task, and a finite one. I put Theorem 1.1 next to Fefferman's (C). (C) requires a smooth, divergence-free initial velocity and a smooth force that satisfy two decay conditions and for which no smooth solution with bounded energy exists for all time. The zero initial velocity is smooth, divergence-free and decays; a smooth force with compact support satisfies every decay condition; the energy bound is in the theorem. The formal statement matches the informal one. That check cost twenty minutes and a PDF reader, and it is the only part of the affair that a third party can finish. Everything else in dispute lies outside the kernel, and each piece has its own instrument:

  1. Is the proof correct? Instrument: the Lean kernel plus a human reading of the statement. Answered.
  2. Whose method is it? Instrument: the literature, the timestamps, a reading of both proofs. Partly answered; for the rest there are Clay's two years.
  3. What did OpenAI's systems see of the other side's work? Instrument: OpenAI's internal logs. There is no external instrument, and there will not be one.

Who had the method first?

Both sides give the same first answer, and they are names no headline carries. Buckmaster: "The credit for the basic idea of this program goes to Diego Córdoba and Luis Martínez-Zoroa, who for several years have been exploring the construction of forced blow ups." Tao describes the program as building the solution in stages, "repeatedly adding small high frequency corrections to a previous (forced) solution", and links the pair's preprint (arXiv:2410.22920). OpenAI's paper cites Córdoba and Martínez-Zoroa in its introduction. From there the chronologies diverge: two accounts that agree on most of the facts and not on what they mean.

  • 15 August 2026. Alpöge and Buckmaster, in a personal collaboration "free of any institutional agreements or official involvement by either of our employers", prove blowup with smooth forcing for Boussinesq and 3D Euler. Tools, per Buckmaster: "Anthropic's Claude, OpenAI's Codex, especially with GPT-5.6 Sol and, more recently, Astra"; he pays "a large bill to OpenAI" from his own research funds. Lean checks the proof on 22 August.
  • 28 August. OpenAI begins training its new internal model.
  • 1 September. OpenAI hears the rumor and launches the agents. Buckmaster writes that Alpöge "had received tips that information about our progress had been passed to OpenAI".
  • 3 September. Buckmaster writes to a mathematician at OpenAI, says the rumor probably refers to him, and asks that nobody rush an AI write-up into publication. A reply the same day, together with an offer of compute.
  • 5 and 6 September. The agents are done; Lean is through on the 6th. At 12:45 on Sunday the 6th, Buckmaster is asked to talk "at any point today". Two calls, Sébastien Bubeck on both, Alpöge on neither. He is told the result is "Existence of forced blowup in R3 and T3", "option c and d in Fefferman", about 100 pages. He asks when the first prompt was sent; the answer, after a while: "in the past few days, after information about our work had reached OpenAI". He asks whether the model "had been trained on, or had access to, our sessions in Codex, into which we had been putting all our drafts for the whole of this project. I was told the model did not look up user data. I asked again, about training, and I did not get an answer." Two proposals: he publishes Euler and OpenAI publishes Navier-Stokes the day after, or he writes up OpenAI's result himself, without Alpöge as an author. He declines both and announces that he will go public. The reply he reports: "Why would you ruin your career?"
  • 7 September, night. Statement, three preprints, Lean repository. His last word on the data: "I have not seen OpenAI's proof. I do not know what their model did, or how. I do not know whether our data was used. I am not accusing anyone of anything."
  • 8 September, noon. OpenAI's announcement recognizes "the priority of their work on forced Euler", states that "no specific user data was accessed in order to solve this problem", and contains, in its first version, the sentence: "While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models" (wording as quoted the same week by Smithsonian Magazine). Bubeck to Fortune: "We did not use their prompts or proofs to prompt our models or direct our agents."
  • 10 September. OpenAI replaces the sentence: "Following an investigation, we have confirmed that Buckmaster's Codex prompts over the two months preceding this announcement and paper on September 8, 2026, could not have influenced the system in any way, including through training. The OpenAI internal model used for this result was developed through large-scale reinforcement learning on top of a previously pretrained model."

On the method, the record is clearer than the tone. OpenAI's Euler result is one without a force, Alpöge and Buckmaster's one with; OpenAI's Navier-Stokes result is one with a force, so the door the two had chosen. OpenAI writes that the proofs "differ significantly"; Buckmaster had not seen OpenAI's proof when he wrote. One factual conflict stays open: OpenAI's page says the two had worked "using an internal Anthropic model", Buckmaster names Claude, Codex, GPT-5.6 Sol and Astra and calls the collaboration personal. Both are on the record, and from outside it cannot be resolved. What is settled is the price of the race. Buckmaster calls his own Euler write-up "AI slop" and writes that the two "would have preferred to spend weeks turning the LLM generated proofs into something readable"; Tao writes that they "were forced to release their preliminary preprints before they were completely digested and polished, due to external events", and: "the actual solving of these problems is only a proxy goal for the primary goal of developing mathematical understanding and insight".

What did OpenAI see of the Codex sessions?

Nobody outside OpenAI can know that, and this sentence is the finding, not a complaint. The statement of 10 September is the strongest a vendor can make: an investigation, "could not have influenced the system in any way, including through training", a model built by reinforcement learning on top of an earlier pretrained model. It is at the same time a statement by the party that holds the only logs, and two of its properties deserve a slow reading. It covers "Buckmaster's Codex prompts over the two months preceding" 8 September, while the drafts went into Codex "for the whole of this project", about a year by his account. And within 48 hours the wording moved from "cannot rule out" via "categorically impossible" (an OpenAI spokesperson to the ABC) to "could not have influenced ... in any way". I have no reason to doubt the final version. I also have no way to check it, Buckmaster just as little, and no team in the same position would have one.

What can be checked is the mechanism, because both vendors document it. A coding-agent session leaves the machine, lands in the vendor's storage for a retention period and from there moves into a training corpus or does not, depending on two things: the plan the account runs on, and a setting. This is what the two vendors' pages said on 13 September 2026 (I read both that day; OpenAI's help article carried the note "Updated: 2 days ago"):

Product and planTraining on contentRetentionSwitch
OpenAI: Free, Plus, Pro (with Codex)Yes, unless opted outTemporary Chats: 30 days, never trained on"Improve the model for everyone" off; Codex Settings
OpenAI: Business, Enterprise, APINo, by defaultEnterprise Privacy pageOpt-in only
Anthropic: Free, Pro, Max (with Claude Code)Yes, when the setting is on5 years (on), 30 days (off)Settings → Data privacy controls
Anthropic: Team, Enterprise, APINo, except Development Partner Program30 days; Zero Data Retention on requestContract, organization admin

The rows carry the vendors' wording. OpenAI in its Help Center: "When you use our services for individuals such as ChatGPT and Codex, we may use your content to train our models", and on the second switch: "Codex has separate controls for allowing training on full environments ... adjusting your settings in the ChatGPT interface or privacy portal will not affect these"; Temporary Chats are deleted after 30 days and never trained on, the regular history stays; for business customers: "By default, we do not train on any inputs or outputs from our products for business users", with opt-in as the only way in (Data Controls FAQ). Anthropic on the consumer plans: "including when they use Claude Code from accounts associated with those plans", with a choice that was due by 8 October 2025 (Anthropic, 2025); on the commercial ones, which include Bedrock, Vertex and Claude Gov: "Anthropic does not train generative models using code or prompts sent to Claude Code under commercial terms", Zero Data Retention for qualified Enterprise accounts (Claude Code documentation).

Buckmaster's sentence reads differently in front of this table. He paid "a large bill to OpenAI" from research funds and put all drafts into Codex. Which row he was in is not public and cannot be determined from outside. On a personal plan with the default setting, the first row applied, and the vendor's page says what that row means; on a Business plan or via the API, the second applied. The difference between "our sessions may have been training data" and "our sessions were contractually excluded" was, during the Sunday calls, an account setting that nobody in those calls could see. Codex data protection and Claude Code data protection are, at this point, not compliance topics but the question of which row a project is in.

Data flow of a Codex session: draft, session at the vendor, retention, training switches, training corpus, model, agents; external verifiability ends at the vendor

How does a team protect unpublished work from the AI vendor?

By settling, before the first prompt, which product and plan the work runs on, whether every training switch is off and where each one sits, which retention applies and how the team proves its own priority without the vendor's help; and by writing that down with a date, because the vendor's page will change and the record has to say which version applied. The question Buckmaster asked on 6 September is unanswerable on 6 September. On the day a project begins, it is one line.

The record is a small file next to the project:

# ai-tools.yaml: data terms of one project,
# fixed before the first prompt
project: euler-blowup-smooth-forcing
recorded: 2026-09-13
tools:
  - product: OpenAI Codex (CLI, IDE, Cloud)
    account: ChatGPT Business
    # personal plans: training on by default
    training: off, by plan
    second_switch: >
      Codex Settings > training on full environments = off
    retention: >
      per Enterprise Privacy page, version of 2026-09-13
    evidence: https://help.openai.com/en/articles/5722486
    # help article showed "Updated: 2 days ago" on 2026-09-13
  - product: Claude Code
    account: Team
    # Free/Pro/Max: switch, 5 years of retention when on
    training: off, commercial terms
    retention: 30 days; Zero Data Retention requested
    evidence: https://code.claude.com/docs/en/data-usage
priority_trail:
  before_each_upload: >
    git commit, signed tag, external timestamp
    (e.g. OpenTimestamps)
  purpose: >
    proves that the draft existed at time T,
    independently of any vendor log
review:
  when: >
    on every change to the vendor's terms;
    the recorded version date is the trigger

Three lines carry the file. The account line, because it decides the row of the table and is the one thing no investigation can change afterwards. The line with the second switch, because the Codex setting for full environments is documented as independent of the ChatGPT switch, and a team that has flipped one switch has flipped exactly one switch. And the priority trail, because a signed, externally timestamped commit is the only provenance evidence that does not live in the vendor's infrastructure. Alpöge and Buckmaster's Lean check of 22 August is exactly this kind of evidence, and that is why the priority question, unlike the data question, has a documented answer.

What does not help

  • "The vendor denied it." A denial is a statement by the party that holds the logs, and the Navier-Stokes wordings show that such a statement can change scope and strength within 48 hours while the facts stay the same. From outside it can be neither confirmed nor refuted.
  • "We use the API, so nothing gets trained." For API, Business and Enterprise that is true by default. But Codex, signed in with a personal ChatGPT account, is the product for individuals, and the switch for full environments is separate from the ChatGPT switch. The row is decided by the account the CLI is signed in with, not by the product name.
  • "We opted out, so the old sessions are safe." The opt-out only works forward: "After you opt out, we won't train our models on your new conversations." And a thumbs-up under a response sends "the entire conversation associated with that feedback" into training, even after the opt-out.
  • "A Lean certificate settles who was first." Lean settles that the theorem is a theorem; a repository timestamp settles that the file existed at that time; neither settles whether two derivations were independent. Only a reading of both proofs settles that, the task Clay's two years are there for.

A Lean certificate is the structural inspection of a proof. It confirms that the construction carries the load. It does not say who drew the plans, and it does not say whose plans were on the table while the drawing was done.

Verdict

"Navier-Stokes solved" is true by the text Clay wrote and not yet recognized by the procedure Clay enforces: (C) and (D) are theorems in Lean, (A) and (B) are open, and the prize needs a journal and two years. The correctness question cost 17 hours of compute and will cost a referee a few weeks. The other two questions have no price at which they could be bought afterwards. Whoever puts unpublished work into a vendor's agent has already decided which row of the table they are in, whether they looked or not. AI governance, in the plain sense this Regulation & Governance dossier means, turns that into a decision with a date and a document instead of a discovery in a Sunday call. Correctness can be bought afterwards. Provenance is fixed before the first prompt, or never.