AI Brief, 9 September 2026: a Millennium Prize problem, claimed and unchecked

OpenAI published On the Navier-Stokes Millennium Prize Problem at 10:00 UTC on 8 September, claiming that an internal model produced a proof that three-dimensional incompressible Navier-Stokes solutions can break down in finite time. That is a claim on one of the seven Clay Millennium Prize problems, and it resolves it in the negative direction: not that fluid flows stay smooth forever, but that at least one of them does not. The company says it does not intend to claim the prize.

Unusually for a claim of this size, the artifact arrived with it. Fifty-seven minutes after the announcement, a 616,276-line Lean 4 formalization went up under Apache-2.0, alongside a 166-page paper, and the formalization contains no unfinished steps in either of its proof directories. What has not arrived is a reader. No mathematician outside OpenAI has reported checking the argument, the papers are self-hosted PDFs rather than preprints or journal submissions, and the repository's own metadata records its review status as self-assessed. This is the second frontier lab in five days to publish a machine-checked proof: the 5 September issue covered Anthropic's Lean formalization of Fermat's Last Theorem, where Kevin Buzzard compiled the repository himself within a day and said it checked out. Nothing equivalent has yet been said about this one.

Six hours before OpenAI's post went live, Tristan Buckmaster of NYU's Courant Institute published a signed four-page statement describing two private calls with OpenAI two days earlier, in which he says he was asked to remove his co-author, an Anthropic employee, from a paper. OpenAI's Sébastien Bubeck disputes that characterisation under his own name. Both accounts are on the record, neither is corroborated, and Buckmaster is careful to say he is not accusing anyone of anything.

Separately, the NSA, CISA and FBI issued a joint advisory naming six Chinese AI companies over what it calls industrial-scale distillation of US models. The document is more interesting than the coverage of it, mostly because of what it declines to allege.

• OpenAI claims alternatives (C) and (D) of Fefferman's official problem statement: finite-time breakdown on both ${\mathbb{R}}^3$ and the torus, for every viscosity, with a smooth compactly supported forcing term. Forcing is permitted in (C) and (D); only (A) and (B) require it to vanish.
• The Lean repository is 2,486 files and 616,276 lines, with zero sorry placeholders in the Navier-Stokes and Euler proof directories and an axiom whitelist that excludes sorryAx.
• OpenAI does not name the model, describing it only as significantly more capable than GPT-6 Astra, with training begun on 28 August and still running. Formalization took a further 17 hours under GPT-6 Astra.
• Clay's rules require publication in a qualifying outlet, two years elapsed, and general acceptance. A CDN-hosted PDF starts none of that clock.
• Joint advisory AA26-251A names DeepSeek, Moonshot AI, Alibaba, MiniMax, StepFun and Z.AI. The words "theft", "trade secret", "steal" and "weights" appear in it zero times.
• Mistral raised €3 billion at a post-money valuation of more than €21 billion, led by Samsung.

What the proof claims, and what the machine actually checked #

The Clay problem is not a single question. Charles Fefferman's official problem statement offers four alternatives, any one of which a solver may take. (A) and (B) ask for global existence and smoothness, on ${\mathbb{R}}^3$ and on the torus respectively, and both require the external force to be identically zero. (C) and (D) ask for the opposite, and permit a force, provided it is smooth and satisfies the stated decay bounds. Fefferman describes the four options as giving "reasonable lee-way to solvers while retaining the heart of the problem."

That matters, because a forced construction sounds like a weaker result and is not. The equations are

$${\partial }_{t}u+(u\cdot \mathrm{\nabla })u=\nu \mathrm{\Delta }u-\mathrm{\nabla }p+f,\mathrm{\nabla }\cdot u=0$$

where $u(x,t)$ is the velocity field, $p$ the pressure, $\nu >0$ the viscosity, and $f$ the external force. OpenAI's Theorem 1.1 starts the fluid from rest, $u(\cdot ,0)=0$ , and produces an $f$ that is smooth and compactly supported for which

$$\underset{0\le t<1}{sup}\Vert u(t){\Vert }_{L^2}<\mathrm{\infty },\underset{t\to 1}{lim sup}\Vert u(t){\Vert }_{L^{\mathrm{\infty }}}=\mathrm{\infty }$$

The energy stays bounded while the velocity itself blows up at time 1. The hard part has never been finding a force that breaks a fluid, it has been finding one that is genuinely smooth. Diego Córdoba and Luis Martínez-Zoroa opened this route earlier, and as Quanta explains, their cascade construction fell short of the prize criteria because stacking the layers could give the combined forcing function undesirable properties. Smoothness of $f$ is the bar.

The repository is the strongest part of the release. It builds against Lean 4.34.0-rc2 and Mathlib, and its checking harness borrows the challenge statements from Google DeepMind's Formal Conjectures project so that the goal is stated independently of the solution. The axiom discipline is what makes the file count mean anything:

// ComparatorChallenges/NavierStokes.json
"permitted_axioms": ["propext", "Quot.sound", "Classical.choice"]

Those are the three standard Mathlib axioms. sorryAx, the axiom Lean introduces when a proof is left unfinished, is absent from the list, so a proof leaning on an unfinished step is rejected rather than quietly accepted. The solution module ends by printing its own axiom dependencies:

#print axioms NavierStokes.Comparator.navier_stokes_breakdown_R3

Anyone with a large enough machine can run that and see the three axioms and nothing else. Four sorry tokens do exist, all in the challenge files, and they are the upstream project's deliberate placeholders rather than gaps in the argument.

What Lean establishes is narrower than it looks, and the gap is the whole story.

Lean verifies that a formal statement follows from the axioms. It does not verify that the formal statement is the one Fefferman wrote down, and it does not read the 166 pages the formalization was derived from. Quanta puts the same caveat plainly: the crucial remaining human job is guaranteeing that the statement shown true in Lean is logically equivalent to what mathematicians set out to prove. That is exactly the job Buzzard performed for the Fermat artifact, and restated in his own comments on 8 September, writing that someone has to read the statement to check it corresponds to the right theorem, and that he did that. Nobody has done it here.

Three states are worth keeping apart. The announcement is dated 8 September. The artifact is public, licensed and machine-checkable. The verification is absent. OpenAI credits no human author on either paper, both of which carry the byline "OpenAI", and does not name the model that found the proof, saying only that it is significantly more capable than GPT-6 Astra and that its training began on 28 August and continues. Clay's rules require publication in a qualifying outlet, two years elapsed, and general acceptance by the mathematical community. A self-hosted PDF is not a qualifying outlet, so the clock has not started, which is presumably part of why OpenAI says it will not claim the prize.

The credit dispute, as far as it is sourced #

At 03:58 UTC on 8 September, roughly six hours before OpenAI's post, Buckmaster published a statement on his university page. He and Levent Alpöge, a mathematician employed by Anthropic, had that morning released finite-time blowup results with smooth forcing for the incompressible porous media, Boussinesq and 3D Euler equations, together with their own Lean repository. Those are related to the Millennium problem and are not a solution of it; Terence Tao, writing the previous day, called the work a breakthrough while noting the authors do not quite achieve those goals yet.

Buckmaster writes that in two calls on 6 September, Bubeck "twice asserted that he wanted Levent removed from authorship", with Alpöge's employment at Anthropic given as the reason, and that he declined the proposals put to him. He quotes a reply of "Why would you ruin your career?" when he said he would go public. Bubeck, on the record under his own name, says he never asked for Alpöge to be removed from authorship of his own work, that the remark about Alpöge's employer arose while discussing a hypothetical rewrite of OpenAI's paper which he felt a rival lab's employee should not author, and that the career remark was poorly chosen, made in frustration and retracted on the call. Neither call was recorded, Alpöge was not on either of them, and no third party has corroborated either version.

The most important sentence in Buckmaster's statement is the one the coverage has mostly dropped. He writes that he has not seen OpenAI's proof, does not know what its model did, does not know whether their data was used, and is "not accusing anyone of anything." What he does report is a question that went unanswered: he says he asked whether the model had been trained on their Codex sessions, was told it did not look up user data, asked again about training, and got no answer. OpenAI's own answer is narrow in both directions. It says no specific user data was accessed, and concedes in the same post that it cannot rule out that de-identified data derived from their use of its products helped improve its models. Both halves belong in any honest summary. The two sides also disagree about who contacted whom first.

This is not an institutional fight, whatever its shape suggests. Buckmaster describes the collaboration as purely personal, free of institutional agreements or official involvement by either employer, and says he paid for tools out of his own research funds. Anthropic as a company has said nothing. OpenAI's post credits the pair's priority on forced Euler explicitly, and Buckmaster uses his statement to push credit further away from himself, writing that the underlying idea belongs to Córdoba and Martínez-Zoroa. Córdoba told Scientific American that he was "a little bit in shock", and attached the conditional that has not been discharged: if it is done, it will be a big surprise. The American Mathematical Society issued a statement the same day calling the progress a milestone advance in human knowledge, in a lineage ending with "the final steps taken by OpenAI mathematicians". It is a statement about credit, and says nothing about whether the proof has been checked.

Tao published a four-part thread ten and a half hours after OpenAI's post, arguing that the stock of good open problems is being mined non-renewably, that "it is now the identification of a promising problem which is the scarce and precious resource", and that "even the rumor of someone working on a problem can trigger a massive amount of AI-powered effort to flatten it". It reads as a response and is not one: the thread names no company, no lab and no result, and extends an argument he began the previous day about his own Equational Theories Project. His one grievance directed at labs is about disclosure, namely their refusal to publish negative results or reveal how solutions were reached. Three days earlier he had proposed a different competition: rather than racing to announce solutions to unsolved problems, race to announce a new mathematical insight.

An advisory that stops short of the word it is being reported with #

The NSA, CISA and FBI published joint advisory AA26-251A on 8 September, naming DeepSeek, Moonshot AI, Alibaba, MiniMax, StepFun and Z.AI, with corporate legal names, and describing what it calls aggressive, malicious and targeted distillation campaigns against US models. Coverage has widely rendered this as theft. The document does not. "Theft", "trade secret", "steal", "stolen", "weights", "hack", "intrusion" and "espionage" appear in it zero times. It states directly that distillation is "recognized as a legitimate and useful technique in AI research", and locates the wrongdoing in the manner of access: terms-of-use violations, fraudulent accounts, gray-market API proxies it calls "transfer stations" used to evade regional restrictions, and jailbreaking aimed at surfacing hidden chain-of-thought. That is a different allegation from weight exfiltration, and no criminal charge, sanction or Entity List designation accompanies it. Treasury Secretary Scott Bessent's public framing is looser than the document he is describing.

The evidentiary base is thin in ways worth stating. There is no indicators-of-compromise section at all, unusual for a joint advisory: no addresses, no domains, no account identifiers, no incident dates. The quantitative claims, billions of tokens across millions of requests, are asserted without methodology. The only nearby figures with a stated method are Anthropic's own, published in February from its own request logs, describing over 16 million exchanges through roughly 24,000 fraudulent accounts. Those are an interested party's unaudited measurements of its own traffic, and the advisory does not restate them, it lists the blog post among its references. The claim that this happened "likely with the knowledge of the Chinese government" rests on that adverb and nothing else.

The advisory's sharpest line is that DeepSeek's quoted $5.6M training cost is misleading. That figure is checkable. DeepSeek's own V3 technical report gives 2,664K + 119K + 5K = 2,788K H800 GPU-hours at an assumed $2 per GPU-hour, which is $5,576,000 exactly. But it is a V3 number rather than an R1 number, and the same paragraph of the same paper already says it excludes prior research and ablations. The gotcha is thinner than it reads. The model lists are worse: the narrative and Table 1 disagree for all six companies, several named US models were never shipped under those names, gpt-oss-20b is OpenAI's own open-weight release where distillation is expressly permitted, and the DeepSeek timeline is chronologically impossible, listing GPT-5 and Claude Sonnet 4.5, from August and September 2025, among models distilled to train R1 and V3, which shipped in January 2025 and December 2024.

The least-covered part of the document is its most consequential. Among the mitigations, the advisory recommends that US providers "avoid informing China-based AI company users suspected of distillation campaigns of a switch to a downgraded model." That is the federal government advising commercial firms to silently degrade paying customers' service on suspicion. None of the six named companies had responded at the time of writing, roughly nine hours after publication and across a Chinese-timezone night, which is neither a denial nor yet a story.

Also notable #

• Mistral raised €3 billion in a Series D at a post-money valuation of more than €21 billion, announced 8 September, led by Samsung Electronics with the EQT-managed Scaleup Europe Fund and PSG Equity as co-leads. Mistral calls it the largest equity round ever completed by a European technology company, which is its own claim.
• ChatGPT Images 2.5 shipped the same day with two API models, GPT-Image-2.5 Flare and Sunburst. Latency is reported as "up to 50%" better than Images 2.0 in the consumer section and a flat 50% against GPT-Image-2 in the API section: two baselines and two strengths of claim for one change. The "more than 3 billion images" weekly figure is a floor, spans ChatGPT and the API together, and predates this model. All self-reported.
• AlphaGenome Atlas covers predicted effects for 9 billion single-nucleotide variants, the right order for roughly 3.1 billion bases times three substitutions each. Access is free for non-commercial use through a Google portal, with commercial access on Google Cloud later, so it is gated rather than open, and the accompanying document is a self-hosted PDF with no DOI.
• Unsloth Desktop v0.1.807-beta switched AMD systems without ROCm to a Vulkan llama.cpp backend by default. The project claims 20% for prefill and decode, while its own detail section says 23% prefill and 8% decode; all self-reported. The backend is chosen at install time via UNSLOTH_LLAMA_CPP_BACKEND=vulkan|cpu|cuda|rocm|auto, so reverting means re-running the installer.
• vLLM tagged v0.29.0, 607 commits ahead of v0.28.0, but published no release and no wheel. The newest installable version remains 0.28.0 from 26 August.

What to watch #

• Whether any mathematician outside OpenAI reads the 166 pages. The Fermat artifact took about a day to attract Buzzard, a point the 5, 6 and 7 September issues tracked. The checkable half here is already checkable by anyone; the half that matters is whether the Lean statement is Fefferman's, and that needs a named expert to say so.
• Whether the two constructions get compared by a neutral party. OpenAI says the proofs differ significantly and that the Euler results are not even the same theorem; Buckmaster says the route is one almost nobody was taking. Both are interested parties, and nobody has looked at both.
• Whether AA26-251A is corrected. The impossible DeepSeek chronology and the inclusion of an open-weight model in a list of illicit extraction are the kind of errors that get quietly amended, and the signed PDF may not match the web edition. Whether any named company responds is separate.
• Artificial Analysis has still stated no comparability position, a fifth consecutive issue, and its changelog added nothing in this window. Independent numbers for Tencent's Hy4 preview remain absent for a seventh.