OpenAI says it solved Navier–Stokes. Verdict: NEEDS REVIEW.
OpenAI says an internal model, run as about 10,000 concurrent agents for 88 hours, produced a Lean-verified proof that the Navier–Stokes equations blow up in finite time — a Millennium Prize problem open since 1934.
OpenAI says an internal model, run as about 10,000 concurrent agents for 88 hours, produced a Lean-verified proof that the Navier–Stokes equations blow up in finite time — a Millennium Prize problem open since 1934. Twelve hours earlier, NYU's Tristan Buckmaster published a four-page statement about how the Sunday phone call with OpenAI went ("Why would you ruin your career?"), Terence Tao wrote that open problems are now being mined like a non-renewable resource, and an Anthropic pretraining researcher resigned over the race. Also: Meta ships Muse, a personal agent with its own VM. Verdict: NEEDS REVIEW.
Read the written edition (English) ↗
What this video covers
- OpenAI: Navier–Stokes blow-up, ~10,000 agents, 88 hours, 130B output tokens, Lean-verified
- Buckmaster and Alpöge: a year on the same approach, a rumor, and a Sunday call with two offers
- Terence Tao: "even the rumor of someone working on a problem can trigger a massive amount of AI-powered effort to flatten it"
- Jacob Coxon resigns from Anthropic: both labs are "racing straight to self-improving superintelligence"
- Meta ships Muse: a personal agent on its own cloud VM, in WhatsApp, US only
Transcript
0:00 Yesterday, OpenAI announced its AI solved a Millennium Prize problem, ninety years open, one million dollars, in eighty-eight hours, and the two mathematicians who spent a year on the same problem learned about it on a Sunday phone call that, per one of them, included: why would you ruin your career? It was a long Monday. At dawn an NYU professor posted a four-page statement; sixteen hundred points on Hacker News. In the afternoon OpenAI posted the proof.
0:26 In the evening Terence Tao said open problems are now mined like a non-renewable resource, and overnight an Anthropic researcher resigned on X, forty-four million views, because both labs are, quote, gambling with our lives. Also, Meta shipped a personal agent that lives in WhatsApp and has its own computer. In this video: the proof, the phone call, the footnote, and the sentence Terence Tao wants the labs to hear.
0:49 It's Wednesday, September 9th, and this is The Daily Diff. The math first. Navier–Stokes describes how fluids move, and since 1934 nobody knew whether a smooth 3D fluid can hit a singularity: velocity going infinite in finite time. OpenAI's system says yes. Start at rest, apply a smooth force, keep the energy finite, and a vortex spirals inward like spaghetti until the speed blows up. Statements C and D of the Clay formulation, in Lean,
1:16 seventeen hours of Astra to verify. So fluids can explode, which anyone who spilled coffee on a MacBook knew, but now it's in Lean. How: OpenAI has a new internal model it calls significantly more capable than Astra, and on September 1st they heard a rumor that two Millennium problems had been solved, so they pointed it at every open one. The Navier–Stokes group: about ten thousand concurrent agents, a hundred and thirty billion output tokens; three hundred billion across all
1:42 problems. At Astra list prices, fifteen million dollars of tokens for a one-million-dollar prize OpenAI says it won't claim, and at that margin, who would. The other side. Tristan Buckmaster at NYU and Levent Alpöge, who works at Anthropic, spent a year pushing an approach by Córdoba and Martínez-Zoroa with Claude and Codex, paying OpenAI from Buckmaster's own research funds. On August 15th they got blow-up for the Euler equations; Buckmaster calls the first LLM proof the most horrendous he has ever read,
2:10 and it verified in Lean on August 22nd. Then a rumor spread, and September 3rd he emailed OpenAI: it's us, it's personal, we'll post soon. On Sunday at 12:45 OpenAI asked to meet at any point today, and Sébastien Bubeck joined. Buckmaster was told the model had proved forced Navier–Stokes with very little human input, which over the call became an entire team, easier problems first, a prompt written by Codex, and an insane amount of
2:36 compute. He asked when the first prompt was sent. Eventually: in the past few days, after information about our work had reached OpenAI. Two offers followed. One: you post Euler, we post Navier–Stokes the next day. Two: Buckmaster alone writes up the OpenAI proof, and, he says, Bubeck twice wanted Alpöge off the paper because he works at Anthropic. He declined and said he'd go public. The reply, per the statement: why would you ruin your career,
3:00 then: if you don't want me to be nice, I don't have to be nice. Normally the line right before a horse's head turns up in a bed. OpenAI's version: nobody saw their work, no user data was accessed, and, footnote, they cannot rule out that de-identified data from the professors' use of their products helped improve the model. Alpöge's review: props to them for straight coming clean. Sam Altman says everyone acted with integrity and generosity and the other team
3:25 threatened unfounded accusations of plagiarism, spelled with one i. So the official position: we did not copy your homework, we heard you were doing homework. Terence Tao called the professors' result remarkable and noted Buckmaster explained it to him over the phone, a refreshing change from AI-based communication modalities. Then, four posts: good open problems are now mined like a non-renewable resource, even a rumor of someone working on one triggers a massive AI effort to flatten it, so the incentive is to stop sharing research
3:55 directions, reversing centuries of open science. Three groups posted fluid blow-up in one weekend; the next paper may be an NDA. Which is the mood Jacob Coxon resigned into: three years of pretraining at OpenAI, then Anthropic; neither company is acting responsibly, he says, both are racing to self-improving superintelligence, and the endgame should not be launched from a private company's Slack. Forty-four million views, on the day one lab put ten thousand agents on a rumor,
4:21 so the thread shipped with a live demo. Meanwhile, Meta shipped Muse: a personal agent on its own cloud VM with its own browser, and you talk to it in WhatsApp. US only, free for most things. Meta promises a version not even Meta can read, later this year, a very specific way of describing this year. Top Hacker News comment: I don't want to share my life with Meta like this. Second: it keeps trying to sell me a stroller.
4:45 If you'd rather read this than hear me say it, the diff lands in your inbox every morning — free at the daily diff dot dev, link below. So — today's verdict: needs review. The proof compiles; the story doesn't. Ten thousand agents closing a ninety-year-old problem in a weekend is the capability result of the year; announcing it with a Sunday phone call to the two people you heard about it from is not.
5:07 And that's the diff for today. I'm Niko from Axrisi. Merge responsibly.
Sources
- OpenAI: On the Navier–Stokes Millennium Prize Problemopenai.com
- OpenAI Lean formalizationgithub.com
- Tristan Buckmaster, statement (PDF)cims.nyu.edu
- HN: Buckmaster statementnews.ycombinator.com
- HN: OpenAI postnews.ycombinator.com
- Terence Tao on the Alpöge–Buckmaster resultmathstodon.xyz
- Terence Tao: open problems mined non-renewablymathstodon.xyz
- HN: Tao threadnews.ycombinator.com
- Clay Mathematics Institute: Navier–Stokes problem statementwww.claymath.org
- GPT-6 Astra pricing (used for the token-bill arithmetic)openai.com
- Jacob Coxon's resignation threadx.com
- HN: I resigned from Anthropic todaynews.ycombinator.com
- Meta: Introducing Museabout.fb.com
- Museai.meta.com
- HN: Musenews.ycombinator.com
