OpenAI's 10,000-agent Navier–Stokes proof claim ignites scooping dispute

OpenAI announces a Millennium Prize result

OpenAI announced on September 8 that an internal, unreleased AI system has produced a proof addressing the Navier–Stokes existence and smoothness problem, one of the seven Millennium Prize Problems. The work was done by a coordinated swarm of roughly 10,000 AI agents, and The Verge reports the company described it as a milestone. Yet within a day the achievement was overshadowed by allegations that OpenAI rushed to beat two human researchers after learning of their progress, and by questions it cannot fully answer about whose data shaped its model.

What OpenAI says it achieved

The Navier–Stokes equations describe how fluids move, and they sit behind weather forecasting, aircraft design and blood-flow modelling. What has been unsettled since the 1930s is whether a smooth three-dimensional flow can spontaneously develop a singularity, where a quantity such as velocity shoots to infinity in finite time. The Clay Mathematics Institute put a $1 million prize on the question in 2000, and it has resisted near a century of attack.

According to dev.to's technical breakdown, OpenAI's paper claims a proof that such a singularity can in fact form from a smooth, physically reasonable starting state, and that the argument has been formalised and checked in Lean, a proof-verification language. The Verge adds that OpenAI says it will not claim the bounty, which the Clay Institute has not awarded; the company frames its goal as reporting on the substantial progress of its models. The effort reportedly cost millions of dollars.

Inside the agent swarm

The dev.to writeup sketches an unusual workflow. Starting in late August, OpenAI trained a new internal model that outperformed its released flagship on mathematics benchmarks. After hearing rumours that a rival lab was close to a Millennium problem, it pointed the model at all the unsolved prize problems at once. Agents ran in large groups, each group given a different framing of the same question, some trying to prove the statement and others to disprove it. The Navier–Stokes group grew to about 10,000 concurrent agents, while a smaller group of under 100 solved a related Euler-equations blow-up question that helped steer the main effort. Periodically, a coding-focused model extracted the most promising partial results and fed them back to other groups as fresh prompts.

The totals are striking: about 88 hours of agent work plus 17 hours of Lean formalisation, close to 5 million inter-agent messages, and on the order of 300 billion output tokens.

The race that preceded it

One day before OpenAI's announcement, New York University mathematician Tristan Buckmaster published findings on a related problem with Levent Alpöge, a researcher at Anthropic who was not working for his employer on this. According to The Verge, Buckmaster contacted OpenAI after learning it was aware of their progress, asking when it had started and what data its model had been trained on. He says the exchange turned hostile, with an OpenAI researcher asking why he would ruin his career, and later saying that if he did not want them to be nice, they did not have to be. Buckmaster says OpenAI urged him to publish while crediting its internal model and dropping Alpöge as co-author. OpenAI researcher Sébastien Bubeck, whom Buckmaster named, disputes parts of this account and denies asking for Alpöge's removal.

On the central data question, OpenAI has flatly denied accessing specific user data, including Buckmaster's Codex sessions, but conceded it cannot rule out that de-identified data derived from product usage helped improve its models, while stressing the two proofs differ significantly. Bubeck told a press briefing reported by Science that the rumours which triggered the effort were found on Twitter, and that OpenAI only later realised they concerned Alpöge and Buckmaster.

A discipline on edge

Mathematicians quoted by The Verge are blunt. Abhishek Saha of Queen Mary University of London says OpenAI did the kind of things mathematicians generally do not do, noting that scooping is rare because frontier problems demand rare expertise. Matthew Ballard of the University of South Carolina argues mathematics runs on an informal norm of trust, with researchers sharing half-formed ideas expecting no competition. Jeremy Avigad of Carnegie Mellon says the mere thought that AI systems might lift ideas from queries is chilling, since the slightest hint could now unleash a well-resourced swarm. Brown University's Brendan Hassett says labs must be able to demonstrate that chat logs will not be used to improve models, and Yang-Hui He worries mathematics could drift back toward Medici-style secrecy.

Why it matters

Two things are true at once. Technically, this is the most visible demonstration yet that massive parallel agent search plus mechanical proof verification can operate at the very top of mathematics, and dev.to draws practical lessons for agentic system builders: diverse framings beat single deep attempts, cross-pollination of partial results matters, and the Lean step is what separates a proof from plausible text. Institutionally, the result is not independently certified, review is ongoing, and OpenAI's inability to conclusively rule out indirect data influence means the trust questions cannot be closed. If famous open problems become marketing opportunities pursued with corporate resources and opaque provenance, the open culture that makes mathematics work is what gets spent first.