On the night of September 8, two posts topped Hacker News at once: NYU professor Tristan Buckmaster's public statement (1,200+ points) and OpenAI's official blog post *On the Navier–Stokes Millennium Prize Problem* (1,088 points, 900+ comments). The most famous of the seven Millennium Prize Problems was, overnight, announced as breached by two groups at once — one human, one a fleet of AI agents.
The counterintuitive headline
Neither side claims to have proven that "water doesn't blow up." Both teams attacked the other side of the fortress.
In 2000, the Clay Mathematics Institute offered $1M for Navier-Stokes existence and smoothness. The official rules open two doors:
- Front door (A)(B): prove that smooth solutions to 3D incompressible Navier-Stokes with smooth initial data (and zero external forcing) stay smooth forever. Still unclaimed — and this is the door most headlines assumed was solved.
- Side door (C)(D): find a counterexample — smooth data plus smooth forcing making the solution lose smoothness in finite time. You are allowed to design the external force yourself, like drawing your own auxiliary lines on the exam. OpenAI walked through this door.
- 167-page paper, sole author: OpenAI.
- A companion 58-page result in the same repo: unforced 3D Euler blows up in finite time from smooth compactly supported data.
- Both results fully formalized in Lean 4 + Mathlib; the repo
openai/NavierStokesAndEulerwent live September 8, hit 800+ stars within hours, and includes an independent re-checker called Comparator. Anyone can clone it and runlean. - Internal model described as "significantly stronger than GPT-6 Astra"
- ~10,000 concurrent agents; launched September 5, ran 88 hours; Lean formalization took another 17 hours
- 4.9 million messages, ~300 billion output tokens
- One HN user's estimate at Astra API prices: ~$15 million of inference
- Total output: 225 pages of rigorous proof plus machine-checkable code
What OpenAI's proof says
Per the blog and paper: for every positive viscosity, there exists a smooth external force such that the solution from rest develops unbounded velocity in finite time — while kinetic energy stays bounded. Both venues of condition (C) — 3D space and the 3D torus (D) — are covered.
The physical picture: an inward-spiraling vortex repeatedly stretched into ever-thinner "spaghetti," with the model pushing high-frequency corrections into unstable directions of the linearized operator, until the system collapses into an unstable modulated ODE — the fluid throws itself out in finite time.
Key facts:
The 88-hour bill
Humans got there half a step first
Buckmaster (NYU Courant) and Alpoge (now at Anthropic) obtained Boussinesq and Euler blowup constructions in mid-August, completed Lean verification on August 22, and posted three papers totaling ~248 pages — same "smooth-forcing blowup" route, building on Córdoba and Martínez-Zoroa (whom Buckmaster says deserves a Fields Medal). A superdiffusive-viscosity NS blowup awaits Lean verification.
Notably, this human team also leaned heavily on AI: Claude and Codex did the heavy lifting; GPT-6 Astra only for writing and auditing. Buckmaster called his own Euler manuscript "AI slop" and apologized for the prose.
The timeline dispute
OpenAI says its project started September 1. Buckmaster released a September 3 email; OpenAI later admitted to them the first prompt was sent only after the B&A news reached the company. Buckmaster alleges that on September 6, over three calls, Bubeck shifted from "minimal human intervention" to admitting the whole team, multiple attempts, and even the prompts were written with Codex; he further alleges two requests to remove Alpoge from the author list and a comment of "why do you want to ruin your career." Bubeck publicly called the accusations "false and inflammatory." On data: OpenAI conceded it "cannot rule out that de-identified usage data helped improve our models"; OpenAI states it does not intend to claim the Millennium Prize. So far only one side has documents — the September 3 email.
The mathematical community's verdict
Terence Tao (September 7 blog) called it a "remarkable achievement" and endorsed the technical core: pushing high-frequency corrections into unstable directions and reducing to an unstable modulated ODE. On unforced NS: "not yet," but feasible and not far. Clay president Bridson stopped at "an exciting day."
Skepticism has precedent: in December 2025, a claimed end-to-end Lean proof proved invalid and a bet paid out in January. This time the repo is public and compiler-verifiable. HN's sharpest test, from user nairboon: have the model independently solve a Millennium problem that doesn't collide with prior human work — e.g., Yang-Mills. Nobody has taken that bet.
The prize is probably still on the table
Clay rules: publication in a top journal, two years of community acceptance, unanimous committee vote — earliest resolution ~2028. Buckmaster called the night a "Deep Blue vs. Kasparov moment": chess thrived for thirty years after. What was proven: fluids can blow up in finite time when external forcing is allowed — a side-door victory. The front door remains open on both tracks, now at full speed.
Two watchpoints: when B&A's unforced-direction construction passes Lean, and whether OpenAI dares take Yang-Mills.
Sources: OpenAI's blog post and papers, the Lean repo openai/NavierStokesAndEuler; Tristan Buckmaster's statement (cims.nyu.edu/~tristanb/statement.pdf) and the B&A preprints; Terence Tao's September 7 post; the Clay Mathematics Institute problem statement PDF; the Hacker News threads.