Inside the Dispute Over A Landmark Agent-Driven Mathematical Proof: OpenAI agents solved a version of the Navier-Stokes fluid equations problem

OpenAI agents solved a longstanding mathematical problem that carries a $1 million prize, but many obervers question whether the agents drew on unpublished work by two mathematicians. 

What's new: On September 8, OpenAI announced that an unreleased model had produced a proof addressing an unsolved problem in fluid dynamics: Whether the equations known as Navier-Stokes have solutions that are, in fact, physically impossible. The proof, which took 10,000 agents 88 hours to produce, shows the answer is yes: Under the right conditions, the equations break down. However, mathematicians Tristan Buckmaster and Levent Alpöge had been using OpenAI Codex to solve the same problem and Buckmaster had discussed the project with OpenAI personnel. OpenAI published its proof only one day after they had published proofs of related equations, raising suspicions that OpenAI’s agents had seen their work, perhaps via models that had been trained on their data.

What the agents proved: The Navier-Stokes equations describe how fluids move, from water in pipes to air over a wing. For decades, mathematicians have tried to determine whether these equations always produce “smooth” solutions — no sudden jumps or infinite speeds — or whether they can predict an infinite speed, which no real fluid can reach. Either answer would settle the problem, a problem selected for a $1 million Millennium Prize funded by Clay Mathematics Institute. OpenAI’s proof demonstrates that under a smooth external force, a fluid's speed can increase beyond finite limits even as its energy remains finite. Clay”s official problem statement allows this result. (The harder version that most mathematicians have in mind, an infinite speed or sudden jump with no outside force at all, remains an open problem.)

Prize pursuits: OpenAI published a 166-page paper as well as the agent-written code in Lean, a programming language that lets computers check mathematical proofs line by line. The underlying model’s name, size, and training data are undisclosed. OpenAI says only that it is “significantly more capable than GPT-6 Astra” and was built by “large-scale reinforcement learning on top of a previously pretrained model.”

• On September 1, after hearing rumors that agents elsewhere were solving Millennium problems, OpenAI launched groups of agents tasked with solving the open problems. Each agent could read a cached snapshot of the web, run code, and message others in its group.
• A group of nearly 100 agents solved a related question about Euler equations — simplified cases of the Navier-Stokes equations — in about 50 hours. OpenAI then shifted agents from the other problems to Navier-Stokes. That group, which grew to 10,000 concurrent agents, reached its conclusion 88 hours after launch, on September 5. Formalizing the steps in Lean took another 17 hours.
• Altogether the agents exchanged 4.9 million messages and generated about 300 billion output tokens. OpenAI did not disclose the cost. Estimates range between $2 million and $22.5 million based on GPT-6 Astra’s list price.
• So far, no independent review of OpenAI’s proof has been completed. Clay's rules require publication, a two-year wait, and general acceptance and review by expert mathematicians before it will consider a solution. OpenAI says it isn't seeking the prize.

The controversy: Hours before OpenAI’s announcement, NYU mathematician Tristan Buckmaster posted a statement that accused OpenAI researcher Sébastien Bubeck of pressuring him over credit for related work he had done with Levent Alpöge, who works at Anthropic. Buckmaster said he and Alpöge had spent most of a year using OpenAI Codex and Anthropic Claude to chase the same kind of proof, building on an approach opened years earlier by mathematicians Diego Córdoba and Luis Martínez-Zoroa, whom Buckmaster credits with “the basic idea of this program.” Buckmaster and Alpöge had posted Lean-verified proofs of three simpler fluid equations, including Navier-Stokes variations, on September 7.

• Buckmaster said his collaboration with Alpöge is personal, not institutional, and that he paid for it out of his own research funds, “including footing a large bill to OpenAI.” He spoke twice by phone with OpenAI’s Bubeck on September 6 and asked whether OpenAI's model had been trained on, or had access to, the Codex sessions where he and Alpöge had been putting drafts. He says he was told the model didn’t look up user data, but his question about training went unanswered. He also says Bubeck proposed that Buckmaster himself write up OpenAI’s result without naming Alpöge because Alpöge works at Anthropic. Bubeck posted on the X social network that he never sought to omit Alpöge’s name.
• On September 8, OpenAI said that neither its researchers nor its agents saw the pair’s work before publication and that no specific user data was accessed — but it could not determine whether the company had used their activities to improve its models. On September 10, OpenAI replaced that sentence: Following an investigation, it said, Buckmaster's Codex prompts over the two months prior to the announcement “could not have influenced the system in any way, including through training.” However, OpenAI did not address whether earlier Codex prompts may have influenced the system.

Behind the news: The race to build math-savvy AI has entered an especially intense phase. Four days before OpenAI's announcement, Anthropic announced that a Claude model had produced the first complete Lean proof of Fermat’s Last Theorem. A research model roughly comparable to Claude Fable 5.1 worked on its own for 11 days and used about 6 billion output tokens — 2 percent of OpenAI’s tally. This proof drew no dispute. It contained no new mathematical inventions. Anthropic built on, credited, and had the result endorsed by Kevin Buzzard, whose Imperial College team has been formalizing the theorem since 2024.

Why it matters: Buckmaster called OpenAI’s Navier-Stokes proof a “Deep Blue-Kasparov moment,” referring to the pivotal series of chess matches in 1996 and 1997 in which IBM’s Deep Blue computer defeated world champion Gary Kasparov. Some pundits question whether mathematician might be an endangered job title. However, Buckmaster noted that the important thing is the sheer speed with which mathematicians and LLMs working together can make progress. Nonetheless, a formally correct proof doesn’t tell you why it works, whether the problem statement is correct, or what meanings can be drawn from it. While automated verification has become relatively inexpensive, human-readable understanding remains costly.

We're thinking: The questions around whether OpenAI used the mathematicians’ work is an important reminder to check the privacy settings of your LLM provider, and to consider zero data-retention options if you’re processing sensitive data that you don’t want a provider to use.