OpenAI's Astra Cracks 10 Math Problems That Stumped Humans for Decades
OpenAI's unreleased Astra model solved 10 decade-old open problems in math and CS, verified in Lean 4, for roughly $2,000 in compute
- OpenAI's unreleased Astra model solved 10 long-standing open problems in math and CS, each open for at least a decade.
- Headline results include the first-ever non-sofic group construction (open since 1999) and a disproof of Connes's rigidity conjecture (posed in 1980).
- All 10 proofs are machine-verified in Lean 4 with zero unproven gaps, published on GitHub under Apache 2.0.
- Total inference cost for all 10 solutions was roughly $2,000 at GPT-5.6 Sol API rates.
- Astra is built for long-horizon multi-agent reasoning; no public release date or pricing has been announced.
- OpenAI explicitly stated AI authorship should be credited as such, putting pressure on journals and universities to update attribution policies.
OpenAI just quietly announced its next major model by doing something unusual: dropping a batch of solved mathematical problems that had stumped the world's best mathematicians for decades. OpenAI revealed Astra, an unreleased model designed to tackle complex, long-running tasks, after an internal version produced ten significant advances in mathematics and theoretical computer science. This is not a benchmark score or a leaderboard climb. These are new mathematical results.
What Astra actually produced
The results are not benchmark scores. They are new mathematical results: constructions, counterexamples, and bounds that professional mathematicians had not been able to produce, now released with machine-checkable proofs in the Lean theorem prover. The company published a 249-page manuscript alongside machine-checkable Lean 4 certificates for every result on GitHub.
Here are the ten results, spanning eight fields:
- High-dimensional sphere packing -- the first improvement to the general upper bound on high-dimensional sphere-packing density since 1978.
- Binary and spherical codes -- exponentially improved bounds on the maximum size of binary codes at any prescribed minimum distance.
- Non-sofic groups -- the first-ever explicit construction of a non-sofic group, resolving a central question in group theory that has stood since Mikhail Gromov introduced the concept of soficity in 1999. No mathematician had managed to prove or disprove whether non-sofic groups exist in the 27 years since.
- Connes's rigidity conjecture -- a disproof, constructing infinitely many non-isomorphic groups with property (T) that share the same von Neumann algebra.
- Arithmetic circuit complexity -- new lower bounds for computing the permanent, including an arithmetic-formula lower bound of order n
4/log n. - Quantum parallel repetition -- an exponential parallel repetition theorem for general two-player quantum games.
- Closest vector problem -- a polynomial-factor hardness of approximation result for the closest vector problem, a foundational question with connections to post-quantum cryptography.
- Ehrhart's volume conjecture -- determining the maximum possible volume of a convex body whose centroid is its only interior lattice point, in every dimension.