OpenAI says unreleased Astra model cracked ten decades-old math problems

OpenAI said on August 1 that an unreleased build of its next model family, codenamed Astra, produced ten solutions to open problems in mathematics, quantum complexity and theoretical computer science. Each problem had gone at least a decade without meaningful progress, the company said in a research post.

The claimed results are unusually specific. They include the first explicit construction of a non-sofic group, a counterexample disproving Connes’s rigidity conjecture, an improved general sphere-packing bound — the first since 1978 — and new circuit-complexity lower bounds for computing the permanent. OpenAI also listed a resolution of Ehrhart’s volume conjecture and improved bounds on multicolor triangle Ramsey numbers.

What separates this from earlier AI math claims is verification. Every result was formalized in Lean 4, the proof-checking language, with machine-checkable certificates published alongside a 249-page manuscript and chain-of-thought walkthroughs in a companion GitHub repository. OpenAI said generating all ten proofs cost roughly $2,000 in API token spend.

The release doubles as a preview. Astra is OpenAI’s next model family, and the company has not shipped it or said when it will. The results come from an internal build whose weights, full method and independent reviews OpenAI has not published. None of the ten proofs has cleared peer review, and mathematicians will need time to check whether the Lean formalizations match the informal claims and whether the problems were genuinely open. A formal Lean certificate confirms a proof is logically valid; it does not confirm the stated theorem is the one that matters.

Still, machine-checked output lowers the usual risk with AI math claims — that a plausible-looking argument hides an error. Expect number theorists and complexity researchers to start pulling apart the openai/ten-proofs repository line by line.