On September 1st, a rumour spread on Twitter X that Anthropic had solved two Millennium Prize Problems. This was proven wrong, but shortly after, OpenAI deployed 10,000 agents anyway.
88 hours later, those agents had a Lean-verified proof of finite-time blowup for the Navier-Stokes equations. A vortex tightens and spins faster while the fluid’s energy stays bounded. "Ten years ago, nobody believed there was a singularity for Navier-Stokes," said Diego Córdoba of the Institute for Mathematical Sciences in Madrid.
The night before the OpenAI announcement, Tristan Buckmaster from NYU published his own statement and competing results. He and his collaborator, Levent Alpoge of Harvard, had been working on the same problem for most of the past year. One of the three papers they released under pressure, he wrote, "can only be described as AI slop. I am sorry for this."
The intellectual foundations of both results belong to Córdoba and Luis Martinez-Zoroa of CUNEF University in Madrid. Their technique, building an infinite sequence of non-singular solutions and combining them in what Martinez-Zoroa calls an “infinite cascade” to produce a singularity, was the most notable insight that everyone else built on. Charles Fefferman from Princeton, who wrote the Clay Institute’s official description of the problem, said the heroes of the story are Córdoba and Martinez-Zoroa. Buckmaster wrote in his statement after:
Let me make plain what I have said to colleagues in private: in view of this body of work, I believe Luis Martinez-Zorao deserves a Fields Medal.
Córdoba on his own AI usage:
I don’t use AI: I have Luis
The remaining mathematical hurdle was producing the infinite cascade with a smoothing forcing function, the version that the Millennium Prize actually requires. Both groups did clear that hurdle, though they dispute who cleared it first and for which version of the problem. Buckmaster and Alpoge claim priority for the Euler result, while OpenAI claims priority for the full Navier-Stokes.
The result has been formally checked in Lean. However, what Lean cannot check is whether the formal statement correctly manages to capture the Mathematical claim - that still requires human scrutiny. The Clay Mathematics Institute hasn’t awarded anything: under its rules, a proposed solution must be published in a qualifying journal, at least two years must pass, and finally it must gain general acceptance. OpenAI announced that it doesn’t intend to actually claim the prize, with Altman joking on X that researchers knew the problem was “only worth $1 million,” while the commute cost was several million.
I don’t have the mathematical background to fully assess the proof’s depth, but I found Terrence Tao’s response to be the most useful framing of what the moment actually represents for the field, beyond the headline and rumours.
Before OpenAI’s announcement, responding to earlier rumours on Mathstodon, Tao wrote that:
There is a substantial opportunity cost in converting a historically productive and motivating problem such as Navier-Stokes regularity into a mere viral social media post advertising some benchmark progress, rather than actually advancing the field and developing the next generation of both problems to ask, and people to work on them.
After September 8th, he put it differently to CNN:
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.
His concern is that the insights generated on the way to a proof (understanding why an approach works, what connections it reveals, and what problems it opens next), often matter more to mathematical progress than the proof itself. AI proofs, inherently, tend to produce answers without those insights. His September 8th essay made the structural point explicitly: AI labs can now mass-deploy compute against a research problem the moment they hear a rumour that someone is close. The dynamics of mathematical research have changed, regardless of whether any particular specific results turn out to be valid. The next generation of problems to ask, and the people who learn to ask them, are the things Tao thinks are now at risk.
Buckmaster and Alpoge spent most of the past year working on fluid equations using AI tools, including Claude and, from his own research funds, OpenAI’s Codex. By August 15th, they had proved finite-time blowup for Euler with smooth forcing, and by August 22nd, they had a Lean-verified proof.
On September 1st, Twitter rumours claimed Anthropic had resolved two Millennium Prize Problems. The rumours were connected to Buckmaster and Alpoge’s work, though the work wasn’t really Anthropic’s. It was a personal collaboration between two mathematicians, one of whom happened to work at Anthropic. Sebastien Bubeck of OpenAI later confirmed the chain of causation directly on X:
We began working on the Millennium problems due to viral Twitter rumours that Anthropic had resolved 2 Millennium problems.
OpenAI set nearly 100 agents to work on the Euler problem (50 hours), then redirected approximately 10,000 agents towards Navier-Stokes. The agents exchanged 2.7 million messages on the Navier-Stokes problem alone and generated roughly 130 billion output tokens. At retail pricing, this would cost approximately $6.5 million in output; Bubeck described the actual expenditure as “several million dollars.” The internal model used, per VentureBeat, is “significantly more capable than GPT-6 Astra. Astra itself was then used for the subsequent 17-hour Lean formalization.
On September 6th, OpenAI contacted Alpoge to reveal what it had. The text exchange that followed has since been posted publicly by Bubeck.
Buckmaster later wrote that hearing the word “forced” was “a bright red flag.” It was precisely the approach that he and Alpoge had been pursuing.
What happened next is mostly disputed. Buckmaster’s account: Bubeck proposed Buckmaster could write up OpenAI’s result without Alpoge as co-author, citing Alpoge’s Anthropic employment as a complication. Bubeck’s account: he was discussing whether Buckmaster could lead to a rewrite of OpenAI’s separate proof, and he felt it would be inappropriate for an Anthropic employee themselves to author work created by an OpenAI system. Bubeck also acknowledged making a remark about Buckmaster “risking his career” and called it “an extremely poor choice of words.” He later said that he retracted this immediately: “I never asked for Levent to be removed from authorship of his own work,” he wrote on X.
Buckmaster published his own statement just before midnight on September 7th, pre-empting OpenAI’s announcement. The statement also raised a question he was careful not to frame as an accusation: that he and Alpoge had been using OpenAI’s Codex on what appeared to be a consumer-tier account. For consumer Codex users, OpenAI’s policy permits use of content for model training unless the user has opted out. Buckmaster wrote: “I do not know whether our data was used. I am not accusing anyone of anything.
OpenAI’s response was the following: “No specific user data was accessed in order to solve this problem.” But: “We cannot rule out that de-identified data derived from their usage of our products helped improve our models.”
The markets are pricing several intangibles.
This is pricing whether Alpoge and Buckmaster’s work gets framed as Anthropic’s result. At its current probability, traders are saying it won’t, which seems like the right chain of thought. The work was personal, with Alpoge’s employer being almost incidental, except insofar as it’s creating the credit complications.
"Does a smooth Navier-Stokes solution always exist?" stands at 7%.
"Will ANOTHER Millennium Prize Problem be solved in 2026?" has moved from 20% to 64% since the announcement. I'd still price the individual problems conservatively given how different they are from Navier-Stokes in terms of existing mathematical scaffolding, but the direction of the move makes sense.
"Will Artificial Intelligence solve a Millennium Prize Problem before 2030?" is now at 97%, with traders saying it’s essentially guaranteed. “In what year will artificial intelligence solve a Millennium Prize Problem?” is trading with a median answer of 2027, implying that they think a second problem falls next year.
We covered AI in mathematics in May, when OpenAI announced the Erdos result, and the market on AI solving an important conjecture before 2030 sat at 76%.
It has gone up to 99% since. The question we asked then, on whether AI will solve a Millennium Prize problem before 2030, now essentially has its answer.
Martínez-Zoroa, when reached for comment, said: "It would have been nice to do this ourselves, but I'm very happy for him."
Happy Forecasting!
- Above the Fold
> “AI solves Millennium Prize Problem in September 2026” is at 95%, the gap most likely just a reflection of the uncertainty about whether OpenAI’s result is fully accepted as a solution to the Millennium Prize version specifically, or a closely related variant.
No, it's pretty obvious that the problem solved is the Millennium Prize problem. The uncertainty was most likely either in whether OpenAI's result is correct at all or if it is considered solved by AI or by humans. However, this has since been resolved YES.
> “In what year will artificial intelligence solve a Millennium Prize Problem?” is trading with a median answer of 2027, implying that they think a second problem falls next year.
No, the question refers to Navier Stokes. It just has 5-year long buckets (2025-2029 is at 98%)