OpenAI says a system more capable than GPT-6 Astra solved a Millennium Prize problem. The internet gasped. Mathematicians squinted. I read the paper, the repo, and the Lean formalization so you don't have to.
Here is the uncomfortable version in 90 seconds:
1. The numbers are real and they are absurd.
10,000 agents. 130 billion output tokens. One candidate singularity proof out the other end. Nobody in the history of mathematics has ever searched a proof space at this scale. That part is genuinely new, and dismissing it because you dislike the company is cope.
2. The Lean certificate proves less than you think.
Lean verified that the formalized steps follow from the stated axioms. Read that again. It checked the logic, not the physics. Whether the assumptions match the actual Millennium problem is a human judgment call — and that judgment hasn't happened yet. Your CI pipeline going green doesn't mean your code is correct either. Same energy — just with $500 billion more market cap behind it. A compiler passing is not peer review passing.
3. The code is public. The acceptance is not.
The proof lives in the navierstokesandeuler repo. Anyone can read it. But there is no Clay Institute acceptance, no published referee report, nothing that turns a candidate proof into a solved prize. "Solved" is doing a lot of commercial lifting in that headline.
4. Ask when, not just what.
A model family ships. A proof drops. An IPO looms. I am not saying the math was scheduled, I am saying billion-dollar announcements deserve billion-dollar skepticism. The footnote is where the body is buried.
My full audit: the vortex math, the fault line in the proof, the token-bill breakdown, and what has to happen next — is here:
👉 Full postmortem with receipts: https://mukul-kumar-mishra.github.io/system-design/navier-stokes-astra-postmortem.html
Now fight me in the comments: does a machine-checked proof count as "solved" before any human referee signs off? Yes or no, defend it. 👇
Top comments (0)