OpenAI Says Unreleased Astra Model Cracked Ten Long-Open Math and Complexity Problems

OpenAI published ten results it says resolve or advance problems that have seen no progress for at least a decade, spanning high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography, and extremal combinatorics. The company attributes the work to an internal version of Astra, described as its next major model.

The claimed advances include the first explicit construction of a non-sofic group, a disproof of Connes's rigidity conjecture, a proof of quantum parallel repetition for general two-player entangled games, a proof of Ehrhart's volume conjecture, and the first improved general sphere-packing exponent since 1978. What separates this from prior lab claims of mathematical ability is verification. OpenAI says the model formalized its arguments in Lean 4, producing machine-checkable certificates on GitHub alongside a 249-page manuscript and per-result reasoning walkthroughs. The company states the successful runs cost roughly $2,000 in tokens at its Sol API rates.

A careful assessment separates two claims. The Lean certificates make the correctness of the formalized proofs independently checkable, which is far stronger evidence than a natural-language argument a reviewer must trust. What remains asserted rather than verified is the process: how many failed attempts, how much human scaffolding shaped the problem setups, and whether the novelty is the model's or comes from expert prompts. Mathematicians will now read the manuscript and audit the Lean files, and their verdict, not the announcement, settles whether these are genuine open-problem resolutions.