OpenAI claims Navier–Stokes Millennium solve; Claude formalizes Fermat's Last Theorem in 11 days

OpenAI has announced that its AI agents solved the Navier–Stokes existence and smoothness problem, one of the seven Millennium Prize Problems set by the Clay Mathematics Institute in 2000, each carrying a $1 million prize. According to MIT Technology Review, only one other Millennium Problem had been solved before this, and OpenAI says it will not claim the prize.

The announcement was quickly overshadowed by a dispute over credit. According to MIT Technology Review, NYU mathematician Tristan Buckmaster and Anthropic employee Levent Alpöge had spent nearly a year on the problem using publicly available models from both OpenAI and Anthropic. On Monday, Buckmaster posted a proof on Mastodon showing that a simplified version of the Navier–Stokes equations can break down. OpenAI followed with a proof that the full equations can break down as well, produced with an internal model said to outperform the recently released Astra model.

A dispute over where the idea came from

Buckmaster also published a document describing his exchanges with OpenAI employees. As MIT Technology Review reports, he says they offered two options: either he and Alpöge post their work and OpenAI posts its own solution the following day, or he co-authors a paper with OpenAI that excludes Alpöge because of his job at rival Anthropic. Buckmaster says employees denied that any agent or person accessed the transcripts of his sessions with OpenAI models, but gave no answer when asked whether those transcripts were used for training. OpenAI chief research officer Mark Chen repeated the denial, while technical staff member Sébastien Bubeck said the team took up the problem after hearing a rumor about Buckmaster and Alpöge's efforts.

Both proofs rely on an approach pioneered by Diego Córdoba and Luis Martínez-Zoroa. Brown University professor Javier Gómez-Serrano notes that independent discovery is plausible, since this was one of several promising lines of attack, but that influence cannot be ruled out.

The price of a proof

In a press briefing, Bubeck and Chen said the team cracked the problem only by running about 10,000 agents concurrently, at a cost of millions of dollars. Buckmaster and Alpöge, working with public models, did not reach a full solution in almost a year.

Claude and Fermat's Last Theorem

The same week produced a second landmark. A dev.to write-up — itself AI-assisted — drawing on Anthropic research posts and a blog by Imperial College London's Kevin Buzzard, reports that Claude produced the first complete machine-checked Lean formalization of Fermat's Last Theorem between August 7 and 17. Buzzard holds a five-year grant (2024–2029) to do precisely that, and titled his post "Anthropic has beaten me to it."

The reported figures are striking: roughly 13 million lines of Lean, some 30,300 sub-theorems proved (29,500 used in the final proof), and about six billion output tokens, generated by dozens of agents coordinating on the Prove2Me platform with an internal research model. Human guidance was limited to occasional high-level hints from an Anthropic researcher. A first attempt reportedly failed because agents worked at cross purposes; the successful run made them share a dependency graph of the theorem.

Buzzard compiled the code himself and confirmed it checks out, but he also flagged limits: the proof follows the 1990s-era Darmon–Diamond–Taylor and Ribet route rather than a modern one, covers only primes p ≥ 17, and, in his view, adds nothing mathematically. Anthropic's own write-up lists further caveats: no explanatory comments, non-standard naming, roughly a fifth of all lines duplicated (a single lemma declared in over 300 files), and a build that needs 96 cores, 512 GiB of RAM and nearly six hours. The code will not enter Mathlib in its current form.

Why it matters

Taken together, the two results suggest that the hardest problems in mathematics may increasingly be settled by a handful of frontier labs with internal models and budgets in the millions — resources almost no academic mathematician has. MIT Technology Review reports hearing from several researchers that mathematicians are becoming depressed, and quotes UCLA's Terence Tao warning that solving problems "prematurely" with "purely AI-powered methods" and without transparency could become "a net negative for the progress of mathematics as a whole."

There are upsides. Machine-checked proofs remove dependence on fallible human referees, and Buzzard predicts that fresh research could soon be formalized almost as fast as it is written. But the OpenAI credit fight points to a governance gap: when agents may have seen, or been trained on, someone's private prior work, the attribution norms underpinning mathematical collaboration no longer obviously apply — and, as this episode shows, nobody may be able to prove what the machines actually used.