OpenAI's Astra solved 10 open math problems — and published the proofs
OpenAI says an internal build of its next model family, Astra, solved ten previously open problems spanning group theory, high-dimensional geometry, coding theory, quantum complexity, lattice cryptography, and extremal combinatorics — including the first explicit construction of a "non-sofic group," a question that had been open since 1999.
The part that actually matters
Plenty of "AI solves hard math problem" claims are difficult to verify independently. This one isn't: OpenAI published a 249-page manuscript alongside machine-checkable proof files written in Lean 4 on GitHub, under an Apache 2.0 license. The repository's "sorry" count — Lean's marker for an unproven placeholder step — is zero across all ten proofs. Anyone with the Lean toolchain can check the work themselves without trusting OpenAI's word for it.
A model claiming to solve open problems is a marketing line. A model producing proofs a third-party verifier can mechanically check is a different, much stronger claim — the difference between "trust us" and "here, run it yourself."
What it cost, and what it doesn't prove
OpenAI put the total compute cost for finding all ten proofs at roughly $2,000 — startlingly cheap next to the years some of these problems had been open. That's a real result. It's not, on its own, evidence of general mathematical reasoning: formally verifiable domains like Lean-checked proofs are a narrow, unusually well-suited benchmark for a system that can search and check its own work automatically. Ten hard, formally verified results are still ten data points, not a claim about what Astra can do outside proof assistants.
Worth watching regardless of where you land on that question: publishing the verification artifact alongside the claim, rather than instead of it, is the kind of move that's likely to become the expected bar for capability announcements generally — not just in math.
Source: siliconangle.com