On 8 September 2026, OpenAI announced that an internal multi-agent system had produced a claimed proof of the Navier–Stokes existence and smoothness problem — one of the seven Clay Millennium Prize Problems. The system reportedly ran for 88 hours, dispatched on the order of 10,000 cooperating agents, exchanged roughly three million messages, and emitted on the order of 130 billion output tokens. A Lean formalization of the proof was published alongside the claim. Critically, the result resolves only two of the four statements the Millennium Prize statement asks for; the remaining two remain open. The company stated it would not seek the $1M Millennium Prize.
The same week, NYU's Tristan Buckmaster and Anthropic researcher Levent Alpöge released preprints on closely related equations — the incompressible porous medium, two-dimensional Boussinesq, and three-dimensional incompressible Euler — produced with AI assistance, formalized in Lean, and described by Buckmaster as the result of roughly a year of work. Terence Tao, who had spent several days reading the Buckmaster–Alpöge arguments, summarized them on his own blog and concluded that the full Navier–Stokes result "looks very feasible" in the near future — but had not, at the time of writing, been completed by any independent group.
Two facts sit underneath the headlines and deserve to be kept apart.
First, the mathematical fact. A Millennium Prize problem is one of the deepest open questions in mathematics. A claimed proof, even accompanied by a Lean formalization, is not a solution until it has been independently checked by the working community and the standing institutions (in this case, the Clay Mathematics Institute) have weighed in. That process is now under way. The Lean artifact matters here: it makes verification possible without trust in the producing system. But Lean checks the proof as written, not the search that produced the proof. The gap between "the proof checks" and "the proof was found the way you think it was" is, as the events below show, not academic.
Second, the structure of the search. OpenAI's own account describes a two-stage process. First, a small team — on the order of 100 agents, working for roughly 50 hours — used the new internal model to produce an unforced 3D Euler regularity disproof: a singularity construction for a closely related, slightly easier equation. That result, not the Navier–Stokes one, was the demonstrative proof of capability. After it checked, OpenAI redirected resources and launched the much larger Navier–Stokes effort: 10,000 agents, 88 hours, 3 million messages, 130 billion output tokens. The Euler disproof was the staircase; the headline result was the building. We will return to this when discussing what kind of work was actually done — and by whom, and to what end.
Third, the sociological fact. OpenAI stated that its effort began on 1 September "after hearing what it called a rumor of another Millennium Prize problem being resolved." Buckmaster and Alpöge had been working on the problem, in some form, for nearly a year, and had used OpenAI's own products (including Codex) in the process. Buckmaster's public statement was scrupulous and worth quoting in full:
"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."
OpenAI's response was equally careful, and equally revealing:
"We cannot rule out that de-identified data derived from their usage of our products helped improve our models."
This is the first sentence in this story that any reader at Rizoma Lab should commit to memory. It is not a denial. It is a structural admission. It says, in plain language: the substrate on which the proof was generated could itself have been shaped by the work it then appeared to recapitulate. A reasoning system without a sovereign evidence model cannot separate the two.
What Terence Tao Actually Said
Tao's reaction has been widely paraphrased. The words that matter are his own:
"It's a little like going to watch a movie and jumping straight from the first ten minutes to the last ten minutes; technically, all the plot lines are resolved, but most of the value of the experience was lost."
And, in the same exchange:
"The indiscriminate use of AI is turning the subject into a meaningless production quota 'game' that ultimately is of very little benefit, either to mathematics or to the world."
This is not a complaint about AI. It is a complaint about unearned compression. Tao is identifying the failure mode we have spent years describing in other vocabularies: a process that produces an answer without producing the chain of understanding that makes the answer durable, teachable, or transferable. The Lean file is real. The proof may well be real. The mathematical insight, in the sense the working community uses the word, is what gets compressed away when 10,000 agents race for 88 hours and the human reading the result has to ask an AI to summarize the proof to them.
Why This Matters to Rizoma
Our work on the G-model — the General Theory of Stupidity — formalizes a specific claim: that the dominant failure mode of large generative systems is not hallucination in the everyday sense, but cognitive collapse under information entropy. The system produces fluent output, the output happens to score well on local metrics, the boundary conditions that would have made the output correct in a meaningful sense are nowhere represented in the system's evidence model. The Navier–Stokes episode is, to us, a near-perfect demonstration of the syndrome — including the part where the result is, on the surface, impressive.
The NARI architecture we are building is designed around the inverse priority. In our world:
Evidence precedes generation. A reasoning step that cannot point to its evidence, its memory, and its justification does not run. We do not "rule out" the use of data we cannot trace — we make the data architecturally inaccessible until it has been admitted through a defined gate.
The search is part of the artifact. A proof produced by a long agentic search is not equivalent to the same proof reconstructed by a deterministic walk through the same evidence. The first is a black box with a certificate; the second is a belief structure. Mathematics, like engineering, like policy, runs on the second.
Sovereignty is not a metaphor. The model that solved Navier–Stokes in 88 hours is internal, undisclosed, and cannot be audited by anyone outside OpenAI. That is a research result; it is not a piece of public infrastructure. A research result is something to be replicated and believed. A piece of public infrastructure is something to be depended on. The conflation of the two is, in our view, the central architectural error of the present decade.
A second observation, specific to this week: OpenAI's own account shows that the useful work was done by the small team, not the large swarm. The 100-agent, 50-hour Euler disproof was the result that pointed the larger effort at a tractable sub-problem. The 10,000-agent, 88-hour Navier–Stokes run was, by OpenAI's own description, a scale-up after a smaller, targeted proof of capability. In our vocabulary: the G-factor of the small run was lower than the G-factor of the large one. The interesting question is not "how do you scale to 10,000 agents" — it is "how do you keep the G-factor low when you do." That is a design problem, not a compute problem.
The Question We Are Left With
If a multi-agent system can compress a year of mathematical work into three days and produce a checkable Lean artifact, what is the future of human-led mathematical research?
Our answer is not "stop." Our answer is narrow the surface area where compression is allowed and widen the surface area where it is forbidden.
A Millennium Prize proof is, almost by definition, a place where compression is allowed: the verification of a Lean file is a defined, finite, mechanical task. Lean will tell you, with certainty, whether the proof checks. This is exactly the kind of problem on which brute-force search plus formalization should be expected to win, and it is not surprising that it has.
The 90% of mathematics that is not a formal proof — the selection of the right definition, the right conjecture, the right counterexample, the right analogy to a different field — is the part where the Tao critique lands. There is no Lean file for "this is the question worth asking." No amount of agent-hours compresses that step. A field that replaces the asking with the answering, even if every answer checks, has not accelerated. It has hollowed out.
The lesson of this week, for us, is not that AI will solve mathematics. The lesson is that the boundary between solving and producing the appearance of having solved is exactly the boundary we have been building sovereign architectures to defend. We expect the next year of this story to be a working demonstration of whether the field takes that boundary seriously.