The $1 Million Navier-Stokes AI Proof Controversy: OpenAI, Anthropic, and the Battle for Mathematical Supremacy

Advanced AI and theoretical mathematics just collided in public, and it got ugly fast. A quiet, independent collaboration between an NYU mathematics professor and an Anthropic researcher turned into an institutional fight involving OpenAI, accusations of scooped research, and the most coveted bounty in mathematics: the Clay Mathematics Institute’s $1 million Millennium Prize.

NYU professor Tristan Buckmaster and Anthropic’s Levent Alpöge recently announced breakthroughs on finite-time blowups in fluid dynamics equations. Then OpenAI said its internal model had solved the actual Navier-Stokes Millennium Prize problem, and the accusations started flying: intellectual property theft, academic pressure tactics, questions about what the model was trained on.

Here’s what the math means, how the AI work actually happened, how the dispute unfolded, and what it says about where AI-assisted research is headed.

The Mathematical Holy Grail: Understanding Navier-Stokes and Finite-Time Blowups

The Navier-Stokes equations are the partial differential equations that describe how viscous fluids move. They govern aircraft aerodynamics, blood flow, and ocean currents.

They were formulated in the 19th century, and mathematicians still don’t have a rigorous proof of whether smooth, globally defined solutions always exist in three dimensions. In 2000, the Clay Mathematics Institute put a $1 million bounty on proving or disproving that existence, one of seven Millennium Prize Problems.

Charles Fefferman’s Formulation and “Options C and D”

Charles Fefferman wrote the official statement of the problem, laying out several conditions, labeled as options, under which a solution counts.

Buckmaster and Alpöge went after one of the hardest pathways: finite-time blowup with smooth forcing. A “blowup” happens when a solution develops a singularity, a point where fluid velocity or vorticity becomes infinite in finite time.

Getting a blowup is easy if you apply a chaotic or discontinuous external force. Fefferman’s options C and D specifically require the force to be infinitely differentiable (smooth) and either compactly supported or periodic. For years, nobody found a way for a smooth force to trigger a genuine, infinite-energy singularity.

The Mechanics of a Fluid Singularity

In turbulent flow, energy usually cascades from large scales down to small ones, where viscosity turns it into heat. A blowup happens when that cascade reverses or accelerates without limit, concentrating infinite kinetic energy at a single point in finite time.

If you use a rough or discontinuous force, you’re basically injecting infinite energy from the start, so forcing a blowup is trivial and doesn’t tell you much. The real challenge in Fefferman’s options C and D is showing that the equations’ own nonlinear term, the $(u \cdot \nabla)u$ piece, can build up infinite energy density on its own, even with a perfectly smooth, bounded, physically realistic force behind it. That takes constructing delicate, nearly self-similar structures, and it’s the kind of problem where AI models can help by holding large systems of inequalities in view at once.

The Stepping Stones: Euler, Boussinesq, and the SQG Connection

Mathematicians usually study simplified variants before tackling the full, viscous Navier-Stokes equations:

1. The 3D Incompressible Euler equations — zero-viscosity fluids, isolating the nonlinear transport of vorticity.
2. The Boussinesq equations — small density variations, used to model buoyancy-driven flows in the atmosphere and ocean.
3. The Surface Quasi-Geostrophic (SQG) equation — models atmospheric and oceanic surface temperature dynamics, and shares deep mathematical structure with 3D Euler.

In August 2026, Buckmaster and Alpöge proved finite-time blowup with smooth forcing for the incompressible porous media equation, the Boussinesq equations, and the 3D incompressible Euler equations.

None of these is the Navier-Stokes equation that carries the prize, but they’re the stepping stones that validate the smooth-forcing approach originally developed by Diego Córdoba and Luis Martínez-Zoroa. Córdoba and Martínez-Zoroa had made major progress proving stable, nearly self-similar blowup for the 2D Boussinesq and 3D Euler equations with smooth data.

Buckmaster has said in private circles that Martínez-Zoroa deserves a Fields Medal for this line of work. He and Alpöge took Córdoba and Martínez-Zoroa’s rough-forcing results and, with AI assistance, extended them into the far harder smooth-forcing regime.

The AI Revolution: How LLMs and Lean 4 Formalization Cracked the Code

This wasn’t a pen-and-paper derivation. Buckmaster and Alpöge ran a heavily AI-augmented workflow using Anthropic’s Claude, OpenAI’s Codex (an internal iteration called GPT-5.6 Sol), and a newer model referred to as Astra.

Frontier Models: GPT-5.6 Sol, Astra, and the Autoformalization Gap

Claude handled high-level conceptual brainstorming and literature review. The heavy lifting in logical deduction went to GPT-5.6 Sol, a Codex iteration built for extended chain-of-thought reasoning and symbolic manipulation, well suited to the dense algebraic topology involved in PDE blowups.

Astra, deployed later, mainly audited arguments and helped with the LaTeX write-up. Even so, autoformalization has a real gap. An LLM can produce a logically sound sequence of deductions in plain language, but turning that into code that matches the exact syntax and definitions of a formal math library is a separate problem. A theorem that’s obviously true in prose can still need hundreds of lines of boilerplate to satisfy a type checker. Buckmaster has said the initial LLM outputs were rough: the AI got the math right but not the rigor, and getting from one to the other took heavy human guidance.

Lean 4 and Mathlib: The Ultimate Mathematical Auditor

Lean 4 is an open-source theorem prover and programming language for formally verifying proofs, and it was central to this breakthrough.

Traditional proofs are written in LaTeX and reviewed by human experts, which can take years and still lets errors slip through. Lean forces the author to translate a proof into strict, machine-checkable code, built on Mathlib, Lean’s community-maintained library of more than 2 million lines of code and 350,000 verified theorems. If the code compiles against Mathlib, the proof holds.

Autoformalization, turning natural-language math arguments into Lean 4 proofs a computer can check, has improved a lot recently, and that’s what let AI agents bridge informal reasoning and rigorous code here.

By August 22, Buckmaster and Alpöge had verified their Euler blowup proof in Lean 4 and posted the code on GitHub. They had also been storing their drafts and sessions inside OpenAI’s Codex environment, a choice that would matter a lot once the dispute broke out.

The Controversy: The Rumor, The Call, and The Alleged Scoop

In early September, rumors started spreading that Anthropic had solved a major open problem. Because Alpöge works at Anthropic, people assumed the company was behind it, even though the research was an independent collaboration funded by Buckmaster’s own research grants and had nothing to do with his employer.

Tristan Buckmaster Reaches Out to OpenAI

On Thursday, September 3, worried about the misinformation spreading, Buckmaster emailed a mathematician at OpenAI to set the record straight. He said the collaboration was independent, that they’d verified results for related equations, and that they’d deliberately held off on releasing a Lean certificate alongside an unpolished preprint. He wanted OpenAI to have the facts.

OpenAI’s initial reply was polite, offering compute and enthusiasm about the progress. The tone changed over the weekend.

The September 6th Call with Sebastien Bubeck

On Sunday, September 6, Buckmaster ended up on a series of calls with Sebastien Bubeck, a research lead at OpenAI and former Microsoft AI VP. Alpöge wasn’t included.

Bubeck told him an internal OpenAI model had produced a roughly 100-page proof of finite-time blowup for the forced Navier-Stokes equations, the actual Millennium Prize problem, using options C and D from Fefferman’s statement with what OpenAI described as very little human input.

That raised immediate red flags for Buckmaster. The smooth-force route through Fefferman’s options C and D was the specific niche pathway Córdoba and Martínez-Zoroa had pioneered, and it was the exact path he and Alpöge had been quietly working on for months. Almost no one else was pursuing that angle.

As the call went on, OpenAI’s account started shifting. It turned out a large human research team had been working on the problem, that they’d primed the model on easier cases like Euler first, and that they’d thrown an enormous amount of compute at it. When Buckmaster asked whether the model had been trained on or had access to his private Codex sessions, where he’d stored a year’s worth of drafts, OpenAI didn’t give him a straight answer.

The Ultimatum: Remove the Anthropic Employee

The most serious allegation concerns how OpenAI framed the credit-sharing. Buckmaster says OpenAI offered two options: either Buckmaster and Alpöge would post their Euler result and OpenAI would post its Navier-Stokes result the next day, or Buckmaster alone would write up OpenAI’s result.

Both versions, according to Buckmaster, required dropping Levent Alpöge from authorship. He says Bubeck was frustrated that Alpöge worked for Anthropic and suggested the situation would be simpler without him involved. When Buckmaster said he’d go public with the details of the call, he says the response was: “If you don’t want me to be nice, then I don’t have to be nice.”

Buckmaster turned down both offers and published his and Alpöge’s verified results on his own, which brought a wave of support from the math community.

The Fallout: “AI Slop” and the Ethics of Training Data

The dispute has exposed real gaps in how AI companies handle academic users’ data and intellectual property.

The Ethical Dilemma of Codex Sessions

OpenAI has said that starting August 28, it began training a new internal model that showed unusually strong math performance.

That timeline raised eyebrows. Buckmaster and Alpöge got their breakthroughs on August 15 and had been feeding drafts, prompts, and reasoning into OpenAI’s Codex for months. OpenAI says its models don’t pull from live user data, but it hasn’t said whether aggregated Codex interactions were folded into the training runs for its new frontier models. If a company trains on a customer’s unpublished research prompts and then that customer gets scooped, that’s a serious breach of trust. In an autoformalization workflow, a researcher’s prompt history is effectively their unpublished IP.

The “AI Slop” Problem in Mathematics

Because of the pressure and the fear of being scooped, Buckmaster and Alpöge published before their work was fully polished. Buckmaster has called the Euler write-up “AI slop.”

In mathematics, how a proof is presented matters almost as much as the logic. A good write-up walks the reader through the intuition, the geometry, the physical meaning behind the equations. LLMs can produce logically sound Lean code, but the prose that comes out tends to read like dense machine output. Buckmaster has said the community deserved weeks of careful human translation to turn the raw AI output into something readable, but the competitive pressure didn’t leave time for that.

Community Reaction and the “Deep Blue-Kasparov” Moment

The math community is still processing this. Fields Medalist Terence Tao has acknowledged how far autoformalization agents have come. Buckmaster has called this a “Deep Blue-Kasparov moment,” a comparison Quanta Magazine and Scientific American have both picked up.

When Deep Blue beat Garry Kasparov in 1997, chess didn’t end, but how the game was studied and played changed for good. A mathematician and an LLM solving multi-year fluid dynamics problems in about a month raises similar questions for research generally: how do you assign credit when an AI generates the core logic? How do journals referee papers co-authored by a model? How do researchers protect work they built using a proprietary AI tool?

Hacker News and X have been arguing over the ethics of AI labs since the story broke. Some critics have pointed out that Sebastien Bubeck’s own earlier claims about models proving “new interesting mathematics” look different next to allegations that a lab used a customer’s own data against them in a race for a million-dollar prize. There’s growing pressure on AI labs to run contamination audits so paying customers’ private work doesn’t end up training the models that compete with them.

The Verdict: Where Do We Go From Here?

The Clay Mathematics Institute hasn’t awarded the prize yet. OpenAI has published its claimed proof and Lean formalization; Buckmaster and Alpöge have published their verified proofs for Euler, Boussinesq, and porous media.

Now the math community has to work through hundreds of pages of AI-generated Lean code to figure out whether OpenAI’s model actually solved Navier-Stokes or produced something that looks right but doesn’t hold up under scrutiny.

Whoever ends up with the $1 million, this dispute has already changed things. Frontier AI models aren’t just coding and writing tools anymore, they’re doing real work in the highest levels of theoretical mathematics. But it’s also a warning: without clear rules on training data, credit, and transparency, the competition between AI labs risks damaging the collaboration that research depends on.

The equations may finally be giving up their secrets. The dispute over who found them first shows that trust and credit are still the harder problem.