OpenAI says an unreleased 'Astra' model cracked ten long-open math problems

OpenAI published ten new results to problems in pure mathematics and theoretical computer science that had seen no progress on their main result for a decade or more — in several cases far longer. The company credits an internal version of Astra, described as its next major model. The problems span high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography, and extremal combinatorics.

Among the named results: a construction of a non-sofic group (settling whether every group admits finite permutation approximations), a claimed counterexample to Connes’ Rigidity Conjecture on group von Neumann algebras, improved asymptotic upper bounds for sphere packing approaching the Cohn–Elkies threshold, exponentially stronger upper bounds for binary and spherical codes, and new bounds for monochromatic triangles in multicolored graphs. Critically, each proof ships with a machine-checkable Lean certificate plus a chain-of-thought walkthrough, released openly in the openai/ten-proofs repository. Sébastien Bubeck promoted the work, and Greg Brockman put the compute cost at roughly $2,000 in API pricing.

The Lean certificates are the load-bearing claim here: if the proofs formally check, the correctness of the results is independently verifiable regardless of how much anyone trusts the model that produced them. That shifts the interesting debate away from hallucination and toward provenance — whether Astra genuinely originated these ideas or heavily assisted human framing — a distinction OpenAI’s blog post and CoT walkthroughs are pitched to address. Reaction on Hacker News was predictably split between excitement and skepticism, but formally verified solutions to problems open for decades, at trivial compute cost, would be a notable marker for AI-assisted research if they withstand scrutiny.