AI + Mathematics
OpenAI, Navier-Stokes, and the million-dollar question.
01 / What is the prize?
Can the equations make water do something impossible?
Start with a fluid moving smoothly. Let the equations run. Can they drive its motion beyond every limit, in a finite amount of time?
The Navier-Stokes equations treat water or air as a continuous substance. Viscosity, the fluid's internal friction, tends to smooth its motion. The question is whether the equations can nevertheless produce an infinite runaway from smooth conditions. Mathematicians call that a singularity. [4]
Real water cannot move infinitely fast. A valid example would reveal where the continuous-fluid description stops making physical sense. It would leave the equations' many useful engineering applications intact. The prize asks whether smooth solutions always persist, or whether a permitted counterexample exists. [2][4]
Clay selected seven Millennium Prize Problems in 2000, with $1 million attached to each. Its Navier-Stokes statement permits a counterexample driven by a smooth external force. That condition matters here. [4][5]
02 / The claim
A vortex, a proof, and a very large computation.
The proposed answer is a vortex that tightens, stretches, and spins ever faster.
The fast-moving region shrinks as its speed grows. That is how the construction can have unbounded speed while keeping total energy finite: ever less fluid carries the extreme motion. A carefully constructed, smooth external force drives the flow. The argument claims alternatives C and D of Clay's problem. [2]
Those figures are OpenAI's account. Discovery used a stronger, unreleased model; Astra handled a further 17 hours of formalization and verification. [1]
What Lean adds
The public repository contains formal theorem statements and build instructions. A proof assistant checks derivations against formal definitions and assumptions. Reviewers still need to inspect that translation, reproduce the checks, and assess the argument. We have not independently audited this proof. [3]
What the result would mean
A valid construction would settle an allowed form of the prize problem. Its use of a designed smooth force matters: conclusions about unforced Navier-Stokes or ordinary turbulence require further arguments. The theorem's assumptions determine its reach. [4]
03 / Before the announcement
The human research already underway.
Tristan Buckmaster and Levent Alpoge built on a program developed by Diego Cordoba and Luis Martinez-Zoroa. Their work used Claude and Codex; Buckmaster describes it as a personal collaboration, independent of either employer. [6]
Buckmaster dates their forced Boussinesq and Euler breakthroughs to this day, followed by Lean verification on August 22. [6]
OpenAI says rumors of solved prize problems prompted its own multiagent effort. [1]
Tao discusses the researchers' three forced-flow results and their potential extension to Navier-Stokes. He credits the underlying Cordoba and Martinez-Zoroa strategy. [7]
OpenAI publishes its proposed proof. The debate expands to authorship, research privacy, and what a proof should teach. [1][6][8]
A separate team, Ganeshram, Duruisseaux, and Anandkumar, is pursuing unforced Euler using physics-informed neural networks and stability analysis. Their candidate construction illustrates another route through AI-assisted mathematics. Tao describes a remaining stability challenge before a full rigorous blowup result. [10][7]
04 / The controversy
Credit. Access. Trust.
Did the lab borrow the researchers' direction, or benefit from private work they entrusted to its tools?
Buckmaster's account
He says the unusual smooth-force route matched their unpublished direction, which made OpenAI's timing suspicious. Their drafts had been going into Codex. He describes pressure to publish and an offer excluding Alpoge from a proposed Navier-Stokes writeup. He explicitly says he does not know whether their data was used. [6]
Alpoge's response
Alpoge treats OpenAI's training caveat as a significant admission. His initial reading suggested similarities to another Euler blowup proof they had developed. This adds a specific mathematical concern to the allegations of borrowed or stolen work; establishing provenance requires evidence beyond resemblance. [11]
OpenAI's response
The company denies accessing specific user data and says the proofs differ. It cannot entirely rule out de-identified usage data improving its models. Bubeck disputes the authorship account: he says the concern involved an Anthropic employee rewriting OpenAI's proof. He also apologizes for his career-related wording. [1][9]
The public record establishes conflicting accounts. It does not establish data theft. The timing and the competing role of a research platform still warrant scrutiny.
05 / Terence Tao's perspective
What did we learn from solving it?
Tao welcomes the mathematical advances. He also argues that understanding and reusable ideas give a solution its lasting value. [7]
His September 8 thread asks what happens when labs can rapidly finish promising problems after hearing that someone is working on them. Choosing a fruitful question takes expertise. Researchers may stop sharing directions if disclosure invites a better-funded competitor to finish first. [8]
He also wants access to failed attempts and the process behind successful solutions. Those reveal where methods work, where they fail, and what to try next. This is an argument about sustaining open mathematics, alongside the excitement of a new result. [8]
Questions people are asking
The short answers.
Has OpenAI won the Millennium Prize?
No prize award is established by the September 8 announcement. Clay requires publication in a qualifying outlet, at least two years, and general mathematical acceptance before considering a solution. OpenAI says it will not claim the prize.
Did GPT-6 Astra solve Navier-Stokes?
OpenAI attributes the proof discovery to an unreleased model stronger than Astra. It reports using Astra for another 17 hours of Lean formalization and verification.
What does the proposed proof establish?
OpenAI claims finite-time blowup for three-dimensional incompressible Navier-Stokes with smooth external forcing, covering the official problem's alternatives C and D. The exact assumptions and formalization require independent review.