On the night of September 8, Hacker News hosted two explosive posts at once: one linking to a statement by NYU mathematician Tristan Buckmaster (1,200+ points), the other to OpenAI's official post "On the Navier–Stokes Millennium Prize Problem" (1,088 points, 900+ comments). The most famous of the seven Millennium Prize Problems was claimed to have been breached the same night—by human mathematicians on one side, and by roughly 100,000 AI instances on the other.
The most counterintuitive conclusion first: neither team claims to have proven that "water blows up" in the unforced setting. Both attacked the other side of the fortress.
The fine print of the Millennium Problem
In 2000, the Clay Mathematics Institute put a $1M bounty on existence and smoothness of Navier-Stokes solutions. The official rules open two doors:
- The front door (Criteria A, B): prove that smooth solutions of the 3D incompressible Navier-Stokes equations remain smooth forever for smooth initial data, with zero external force.
- The side door (Criteria C, D): produce a counterexample—smooth data plus a smooth external force you are allowed to design—making the solution lose smoothness in finite time.
- Dec 2025 — Budden claims a Lean end-to-end proof; invalid, bet settles in January
- Aug 15 — Buckmaster & Alpoge secure two blowup constructions
- Aug 22 — Lean verification of the human team's papers completed
- Sep 3 — Buckmaster emails OpenAI about his team's progress
- Sep 5 — OpenAI's 10,000-agent sprint starts; runs 88 hours
- Sep 6 — Three Bubeck calls; the Rashomon begins
- Sep 7 — Tao's post delivers the technical verdict
- Sep 8 — OpenAI paper and Lean repo go public; Buckmaster's statement posted
The side door's fine print—that the forcing is yours to design—is like being allowed to draw your own auxiliary lines on the exam. Most headlines omitted it; OpenAI went precisely through this door.
What OpenAI's proof says
Per the official blog and accompanying paper: for every positive viscosity coefficient, there exists a smooth forcing under which the solution starting from rest develops unbounded velocity in finite time, while kinetic energy remains bounded throughout. Both Criterion (C) in R³ and (D) on the 3D torus are settled.
The physical picture: an inward-spiraling vortex repeatedly stretched into ever-thinner "spaghetti" filaments; the model pushes high-frequency corrections into unstable directions of the linearized operator, until the whole system collapses into an unstable modulation ODE—the fluid throws itself out in finite time.
The 167-page paper's author field contains one word: OpenAI. The same repository holds a 58-page result proving finite-time blowup for the unforced 3D Euler equations from smooth compactly supported data—arguably the cleaner headline, yet buried in the announcement's second paragraph. Both results are fully formalized in Lean 4 with Mathlib. The repository, NavierStokesAndEuler, went live September 8, gathered 800+ stars within hours, and ships an independent re-checker called Comparator. Anyone can clone it, type lean, and watch the compiler verify this century-scale claim line by line.
The 88-hour bill
The process numbers are the most surreal part of the announcement. The internal model is officially described as "significantly stronger than GPT-6 Astra"; ~10,000 agents ran concurrently; the run started September 5 and finished in 88 hours, with Lean formalization taking another 17 hours. Total traffic: 4.9 million messages, roughly 300 billion output tokens. Someone on HN priced this at Astra's API rates: around $15 million. The cheapest Millennium Problem solution in history—and the most expensive inference bill.
For scale: a prolific mathematician producing a thousand pages over a lifetime is rare. One night yielded 225 pages of rigorous proof, plus machine-checkable code that compiles.
| Item | Number | |---|---| | NS paper | 167 pages, signed OpenAI | | Unforced Euler blowup | 58 pages | | Concurrent agents | ~10,000 | | Main runs | 88 hours + 17 hours Lean verification | | Messages / output tokens | 4.9M / ~300B | | Estimated inference cost | ~$15M |
Humans got there half a step first
On the other track: Buckmaster (NYU Courant, longtime attacker of fluid singularity problems) and Alpoge (now an Anthropic researcher). In mid-August they obtained blowup constructions for the Boussinesq and Euler equations, completing Lean verification on August 22—three papers totaling ~248 pages, via the same "smooth-forcing blowup" route. The theoretical skeleton draws on work by Córdoba and Martínez-Zoroa; Buckmaster said Martínez-Zoroa's work deserves a Fields Medal. They also hold a blowup construction for hyperdiffusive NS awaiting Lean verification, not yet released.
An easily missed fact: this human team itself used AI heavily—Claude and Codex did the heavy lifting; GPT-6 Astra was used only for writing and auditing. Buckmaster even called his own Euler manuscript "AI slop" and publicly apologized for its writing quality.
Rashomon
The real drama is the timeline. OpenAI says the project started September 1. Buckmaster's statement produced a September 3 email: OpenAI later admitted the first prompt was sent only after news of the B&A work reached them.
On September 6, OpenAI's Bubeck and Buckmaster spoke three times. Per Buckmaster, he was first told there was "minimal human intervention," then the story changed mid-call: the whole team, multiple attempts, and the prompt itself were written with Codex, with "absurd amounts of compute." He also alleges two requests to remove Alpoge from the author list, and the line "why would you ruin your career." Bubeck's public response: the allegations are "false and inflammatory."
The data question is murkier. OpenAI conceded it "cannot rule out that de-identified usage data helped improve our models"; Buckmaster's question about whether Codex sessions entered the training set went unanswered. OpenAI also stated it does not intend to claim the Millennium Prize. So far, only one side has produced documents—the September 3 email, fully available.
The math community's verdict
Terence Tao, in a September 7 blog post, called it a "remarkable achievement" and endorsed the technical core: pushing high-frequency corrections into unstable directions and reducing to an unstable modulation ODE system is real. As for unforced NS, "not yet"—but feasible, and not far off. Clay Institute president Bridson stopped at "an exciting day."
Skepticism has precedent: in December 2025, former DeepMind director Budden claimed an end-to-end Lean proof that later proved invalid, settling a bet in January. The difference this time: the repository is public and independently verifiable—the compiler takes no side in disputes.
The sharpest test on HN came 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 dared take that bet.
The prize money likely stays on the table
Clay rules: publication in an authoritative journal, two years of community acceptance, unanimous committee vote. The earliest verdict is 2028; the $1M most likely stays put. Buckmaster called this night "the Deep Blue vs. Kasparov moment." Deep Blue won that game, and chess flourished for thirty more years. What this night proved: when external forces may be designed, fluids can blow up in finite time—a victory at the side door. The front door remains open, and both tracks are now running at full speed.
The eight-day interleaving of the two tracks deserves a look:
---
Sources: OpenAI, "On the Navier–Stokes Millennium Prize Problem," accompanying paper, and the Lean repository 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's official problem statement PDF; the Hacker News discussion thread.