OpenAI Claims an Internal AI Solved Navier-Stokes (One of the $1M Millennium Problems) — The Math Is Stunning, the Ethics Are a Mess
OpenAI announced that an internal model solved the Navier–Stokes existence and smoothness problem, one of the seven Millennium Prize Problems carrying a $1M bounty from the Clay Mathematics Institute. The proof demonstrates that the Navier-Stokes equations, which govern fluid motion, can develop a singularity in finite time — a result mathematicians have pursued for 26 years.
The achievement is extraordinary. An AI model trained for under two weeks is reportedly "more than twice as capable in mathematics as GPT-6 Astra," which OpenAI released just a week prior. The proof was formalized in Lean, a proof assistant, making it machine-verifiable.
But the story has two layers. The math layer is landmark. The ethics layer — involving threatened academics, stolen credit, and a researcher whose ChatGPT sessions may have seeded OpenAI's solution — is the kind of controversy that will define how academia and AI labs collaborate going forward.
Here's what happened, what the proof actually says, and why you should care about both halves of this story.
What Actually Happened
According to HN commenters who read OpenAI's announcement (the page is JavaScript-rendered, but key excerpts were quoted in the thread):
"We're sharing a solution to the Navier–Stokes existence and smoothness problem, one of the Millennium Prize Problems. This proof, produced by an internal OpenAI system, shows that the dynamics of the Navier-Stokes equations for fluid motion can develop a singularity in finite time."
The timeline, reconstructed from HN comments and the concurrent Buckmaster statement:
Shotgun on all six. OpenAI's internal model (more capable than GPT-6 Astra) was first pointed at the six open Millennium Prize Problems simultaneously. The approach was brute-force — use massive agent parallelism and see what sticks.
Unforced Euler falls first. With 100 agents working in parallel, the model solved the unforced 3D Euler blowup problem. This is a related but non-Millennium fluid dynamics problem.
10,000 agents on Navier-Stokes. With the Euler result as a starting point, OpenAI scaled to 10,000 agents and targeted the full Navier-Stokes existence and smoothness problem. The model produced a proof showing finite-time singularity formation.
Formalized in Lean. The proof was written in the Lean proof assistant, which means it's mechanically verifiable — not a hand-wavy "trust me" mathematical argument.
One HN commenter summarized the model progression:
"There are at least two versions of a model more powerful than Astra at OpenAI at the moment. The less capable version was used to solve the unforced Euler problem with 100 agents. The more improved version was used to solve Navier-Stokes with 10,000 agents."
The Mathematics: Finite-Time Singularity in Navier-Stokes
The Millennium Prize Problem asks whether solutions to the Navier-Stokes equations, which model how fluids like air and water move, can develop singularities (points where the velocity becomes infinite) in finite time, or whether they remain smooth forever given reasonable initial conditions.
OpenAI's proof answers: singularities can form in finite time.
This is significant because it resolves a fundamental question about whether the Navier-Stokes equations — which we use every day to model weather, aerodynamics, blood flow, and ocean currents — are mathematically "well-posed" in the sense of always having smooth solutions. If singularities can form, there's a limit to how far these equations can predict fluid behavior without breaking down.
The approach used by OpenAI's model is reportedly similar to recent work by mathematicians Tristan Buckmaster (NYU) and Levent Alpöge (Anthropic) , who had been making progress on related problems. Buckmaster and Alpöge had proven finite-time blowup for incompressible porous media, Boussinesq, and 3D incompressible Euler — close variants of the Navier-Stokes problem, but not the Millennium version itself.
The Controversy: "Why Would You Ruin Your Career?"
Here's where the story stops being about math and starts being about ethics.
Tristan Buckmaster, a professor at NYU's Courant Institute, published a personal statement on September 8 detailing interactions with OpenAI. The sequence of events, per his account:
Early September: A rumor spread inside OpenAI that "Anthropic solved a major math problem" — referring to Alpöge, who works at Anthropic, and his collaborator Buckmaster. The work was independent of Anthropic's AI efforts.
Buckmaster clarifies. Buckmaster emailed OpenAI to correct the rumor, without revealing the specific problem or his methodology.
OpenAI pivots to Navier-Stokes. After learning the rumor, OpenAI started directing its internal model at Navier-Stokes. Within days, senior researcher Sebastien Bubeck told Buckmaster they'd solved the $1M Millennium Prize problem — using an approach "very similar" to Buckmaster and Alpöge's work on the non-Millennium variant.
Credit conditional on removing Alpöge. OpenAI offered to credit Buckmaster for the discovery — but only if Buckmaster removed Alpöge as a co-author, since Alpöge works for Anthropic.
The threat. When Buckmaster declined, he says OpenAI's representative told him: "If you don't want me to be nice, then I don't have to be nice." And: "Why would you ruin your career?"
Rushed independent publication. Buckmaster and Alpöge rushed to publish their own results independently on September 8 — two days before OpenAI's announcement — establishing priority and demonstrating their independent approach.
OpenAI's own announcement hedges: "While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models."
This is the crux. Buckmaster and Alpöge used AI tools (including ChatGPT and Claude) in their research. If those sessions contributed to OpenAI's training data, then OpenAI's model may have been informed by the very researchers it's now racing to publish over — a feedback loop that's hard to distinguish from data theft.
Terence Tao Weighs In
Fields Medalist Terence Tao, the world's most famous living mathematician, commented on Mathstodon:
"The point remains 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."
Tao's point is subtle but important. Even if the solution is correct, the way it was produced and announced — as a PR event rather than a peer-reviewed mathematical contribution — changes the incentives for how mathematical research gets done.
What This Means for the AI Industry
Ignore the drama for a moment. The technical claims are extraordinary:
- A model trained for under two weeks outperforms GPT-6 Astra (released the previous week) by 2x on mathematics.
- 10,000 AI agents collaborating solved a problem that resisted 26 years of human effort.
- The proof is machine-verifiable via Lean, reducing the risk of subtle human errors that plague long mathematical proofs.
If true, this means AI has crossed a threshold in mathematical research. The claim that "LLMs can't do novel mathematics" is dead. The remaining question is whether the output is truth or just an exceptionally well-optimized hallucination.
Several HN commenters raised the Lean angle: "With these massive Lean proofs how do we know the model didn't just find some bug in Lean and exploit it?" It's a fair question — automated theorem provers have been gamed before. But a Lean proof that compiles is, by definition, logically sound within Lean's axioms. If the translation from mathematical reasoning to Lean is correct, the proof holds.
The Questions That Remain
For mathematicians: Is the proof correct? Has it been independently verified? The Clay Institute's $1M prize isn't awarded for a press release — there's a formal verification process.
For AI researchers: How does OpenAI's internal model achieve 2x math improvement over Astra in two weeks? What architecture allows 10,000 agents to converge on a coherent proof? These are the technical details that matter more than the drama.
For engineers using AI tools: If your API conversations can be used to train models that then compete with you, you need to understand what "opting out" actually means. OpenAI's candid admission that they "cannot rule out" training on user data should give you pause.
For anyone evaluating AI progress: The Navier-Stokes result — if verified — is the single strongest piece of evidence yet that LLMs can produce novel, high-value mathematical results. The fact that it comes wrapped in a controversy over credit and data rights doesn't diminish the technical achievement. It does, however, tell you everything you need to know about how AI labs view their relationship with the broader research community.
Sources: HN discussion — OpenAI announcement (1127 pts), HN discussion — Buckmaster statement (1270 pts), Tristan Buckmaster personal statement (PDF), Terence Tao on Mathstodon, OpenAI announcement page. Key quotes from HN comments cited inline. Coworker model capability claims and shotgunning timeline per HN commenters. Timeline of Buckmaster's interactions reconstructed from his statement and cross-referenced to HN thread.
Top comments (0)