OpenAI's Navier-Stokes Win Cost ~$15M in Output Tokens

OpenAI claims its agents solved a Millennium Prize problem — Navier–Stokes, Lean-formalized, verified Sunday morning. The announcement is real. The receipt is the story. Buried in OpenAI's own writeup: the run sent 4.9 million messages and ~300 billion output tokens. At the published Astra rate of $50 per million output tokens, that output side alone is ~$15,000,000 — and OpenAI's head of research Mark Chen confirmed the compute cost "in the millions of dollars." That number isn't an estimate of their internal bill; it's what the same workload would cost you at list price.

What shipped

Per the press briefing: OpenAI started training a math-heavy internal model on August 28, read rumors that Anthropic-affiliated researchers were closing in on Navier–Stokes, then pointed 1,000+ agents at the problem for 50+ hours until one produced a proof that formalized in Lean. HN put the announcement at 535 points within hours. The math itself hasn't been independently published yet — "Lean-formalized" is the strongest verification claim on the table today.

The other receipt

Now the counter-fact. The "concurrent work" OpenAI's post footnotes is by two people — NYU's Tristan Buckmaster and Anthropic researcher Levent Alpöge — who posted their advance before OpenAI's announcement, using off-the-shelf Claude and Codex. Retail subscriptions, no agent swarm. So the same mathematical frontier was reached from two directions: a ~$15M token firehose, and two researchers with consumer coding agents.

The two-tier game

And it's already bitter. Buckmaster's statement alleges OpenAI learned of his work last week, mobilized, couldn't answer whether it accessed his Codex logs, and floated credit proposals that excluded his collaborator. Bubeck denies the name-removal claim; Altman waded in. Whatever the truth, note the structure: the people who did the prior work with cheap agents are now negotiating with the people who spent $15M to arrive second-adjacent. Frontier math is a two-tier game now — and the bottom tier just proved it can play.