OpenAI's Astra solves 10 long-open math problems and publishes proofs

Aug 2, 2026

OpenAI's unreleased Astra AI model has solved 10 long-open problems in mathematics, publishing machine-checkable proofs for each. The breakthroughs, including disproving Connes’s rigidity conjecture, are seen as "big news" by experts, contrasting with a prior false claim by OpenAI in 2025. The results arrive amid growing concern in the math community over AI's role and lack of peer review.

Astra mathematical breakthroughs

▪Astra disproved Connes’s rigidity conjecture, posed in 1980, and proved Ehrhart’s volume conjecture.
▪One major result is the construction of a non-sofic group, a problem open since Mikhail Gromov introduced the concept in 1999.
▪An internal version of OpenAI's Astra model produced new results for 10 long-open problems in mathematics and theoretical computer science.
▪The model also solved three problems from Paul Erdős’s catalog, including problem 183 on multicolor Ramsey numbers.

Lean proof verification

▪The results have not yet been through peer review, and mathematicians must still verify that the formal statements match the problems.
▪OpenAI published machine-checkable proofs for all 10 results, including a 249-page manuscript and Lean 4 certificates.
▪The Lean 4 certificates are available on GitHub under an Apache 2.0 license and have a "sorry" count of zero, indicating no steps were left unproven.

Previous GPT-5 controversy

▪In October 2025, OpenAI's then vice president of science, Kevin Weil, falsely claimed GPT-5 had solved 10 unsolved Erdős problems.
▪Thomas Bloom described the new Astra results as "big news," rating them higher than a previous OpenAI counterexample he helped verify.
▪Following the 2025 incident, Kevin Weil deleted his post, and Google DeepMind CEO Demis Hassabis called it embarrassing.
▪Erdős problem database maintainer Thomas Bloom called the 2025 claim a "dramatic misrepresentation," as the model had only found existing papers.

Computational cost efficiency

▪While the mathematical arguments came from Astra, human researchers turned the model's output into publishable papers.
▪OpenAI estimated the total token cost for solving all 10 problems at approximately $2,000, based on GPT-5.6 Sol API rates.

Mathematical community backlash

▪The Leiden Declaration warns that AI companies are "using published research without consent, bypassing peer review, and threatening the integrity of proof and attribution."
▪In June, the International Mathematical Union endorsed the Leiden Declaration, which criticizes AI companies' use of published research.
▪Software engineer Fernando Borretti argued that AI will push the frontier of mathematics beyond human comprehension.

Astra release timeline uncertainty

▪OpenAI research scientist Noam Brown called the results "a major step for scientific reasoning."
▪Astra is described as an unreleased model family designed to coordinate multiple agents for long tasks.
▪OpenAI has not announced a release date, pricing, or final name for the Astra model family.
▪Any launch of Astra must undergo the federal AI safety review process that previously delayed the GPT-5.6 rollout.