Credit

The other papers of 8 September

❓ What did human mathematicians actually release the same day?

Tristan Buckmaster (NYU Courant) and Levent Alpöge (a mathematician at Anthropic) posted three results: finite-time blowup with smooth forcing for incompressible porous media, Boussinesq, and 3D incompressible Euler, following the program of Diego Córdoba and Luis Martínez-Zoroa, with “a great deal of help from LLMs” (Anthropic and OpenAI models, including Codex). Lean verification is claimed for released pieces. They did not claim full Navier–Stokes. Buckmaster wrote that they believe they have hypo-dissipative Navier–Stokes but were not releasing it without Lean and a presentable writeup.

Tao called the Buckmaster–Alpöge work a remarkable achievement and said there did not seem to be anything in principle preventing extension all the way to Navier–Stokes, given enough compute and AI.

A third, independent Euler line appeared around 7 September: Ganeshram, Duruisseaux, and Anandkumar, using a physics-informed neural network to locate a blowup ansatz for 3D Euler without forcing. Tao flagged it as more “mainstream” numerically and relatively AI-light (literature review and Lean as secondary tasks).

OpenAI’s account of overlap

❓ What does OpenAI say it knew, and when?

The company dates its effort to 1 September, after a rumor later connected to Alpöge and Buckmaster. After finishing Lean verification on 6 September, believing the rumor was a Navier–Stokes solution, OpenAI says it reached out to offer a concurrent release and to recognize their priority. It then learned they had forced Euler, not Navier–Stokes. OpenAI says it offered visibility into prompts and later the proof, recognizes priority on forced Euler, and congratulates them.

On data: researchers and agents “did not see any of their work through any means until they released it publicly”; “no specific user data was accessed.” “While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models.” The Euler theorems, OpenAI notes, differ: forced versus unforced.

Mark Chen, on a reporter call, said no people or AI systems searched user data to solve the problem, and that he was disappointed by the allegations.

Buckmaster’s account of the calls

❓ What does Buckmaster allege that OpenAI does not?

In a public statement accompanying the preprints, Buckmaster describes 6 September calls with Sébastien Bubeck (and another OpenAI mathematician), without Alpöge on the line. He says he was told an internal model had produced a roughly 100-page proof of forced Navier–Stokes blowup on \(\mathbb{R}^3\) and the torus — “the route Luis and Diego opened and the one Levent and I had quietly chosen,” a route “almost nobody else I know of was working on.” He says the first prompt was sent after word of their work reached OpenAI. He asked whether the model had been trained on or had access to Codex sessions containing their drafts; he was told the model did not look up user data, and did not get an answer on training. He alleges pressure to drop Alpöge as coauthor because Alpöge works at Anthropic, and an offer of sole authorship on a paper that would credit OpenAI’s model.

Those are allegations. They are specific, dated, and from a named specialist. They are not court findings. This package does not adjudicate intent.

Why the dispute is load-bearing for AI science

❓ Even if the theorem is true, what institutional fact is being tested?

If unpublished research cannot safely live inside a lab’s coding agent, then the labs that own the best agents become unavoidable coauthors — or adversaries — of the fields they serve. That is a trust problem orthogonal to Lean.

If, instead, OpenAI’s isolation claims hold and the swarm rediscovered a rare route from rumor-level hints plus general training, then the story is “compute finishes the last mile,” which is the story Tao already considered likely.

Diego Córdoba’s reaction, to Scientific American, sits in the middle: shock, and surprise “if it’s done,” because the forcing approach was theirs.

The right reader posture on 8 September is: keep the theorem and the process in separate columns. A correct proof can still have an ugly priority story. An ugly priority story does not, by itself, put a sorry in Lean.

DeepMind 2025 as background, not this result

❓ Had AI already “found singularities” in fluids?

In September 2025 Google DeepMind, with academic collaborators, reported systematic discovery of new families of unstable singularities in related fluid equations (including IPM and Boussinesq) using machine-learning optimizers. That was a numerical-discovery milestone aimed at the same mountain. It was not a Lean Clay (C)/(D) theorem. It belongs on the tech tree as an earlier rung.