OpenAI's Astra Solved 10 Open Math Problems. I Checked the Proofs.
On August 1, 2026, OpenAI said an internal version of its next model, Astra, solved ten open problems in mathematics and theoretical computer science. The tokens used to find the solutions would cost about $2,000 at API rates. Claims like this are usually impossible to check. This one is different. OpenAI published every proof as a Lean 4 certificate on GitHub. So I downloaded them and looked. ...