OpenAI says its Astra model solved 10 long-open math problems for $2,000

OpenAI revealed on Saturday that its internal model Astra produced new results for 10 problems in mathematics and theoretical computer science that had remained open for at least a decade, publishing machine-checkable proofs alongside each claim. The company reported a token cost of roughly $2,000 at current API rates for all 10 solutions.forbes+1

Verified Proofs Across Multiple Fields

The results span high-dimensional sphere packing, coding theory, cryptography, extremal combinatorics, and quantum game theory. The headline result is an explicit construction of a non-sofic group, a question open since 1999, which disproves the conjecture that all countable groups are sofic. Astra also disproved Connes's rigidity conjecture from 1980 and resolved three problems from Paul Erdős's catalog, including problem 183 on multicolor Ramsey numbers.newscientist+1

OpenAI published a 249-page manuscript along with Lean 4 proof certificates on GitHub under an Apache 2.0 license, reporting a "sorry" count of zero — meaning no step in any formalized proof was left unproven. The Lean kernel returns a binary verdict: either the proof compiles or it does not, removing the need to trust the model's output on faith.siliconangle+1

Thomas Bloom, who maintains the Erdős problem catalogue, called the results "big news" and rated them ahead of the Erdős unit distance counterexample that an earlier OpenAI model produced in May. Abhishek Saha at Queen Mary University of London said any one of the 10 solutions "would be a significant and impressive achievement".newscientist+1

Skeptics Urge Caution

The announcement drew pointed criticism. Gary Marcus, a prominent AI skeptic, described the release as "amazing — but vastly oversold," arguing that success in formally verifiable mathematics does not generalize to domains where verification is harder. He noted that the $2,000 figure covers only successful attempts and excludes the salaries of mathematicians and computer scientists who helped prepare the papers.garymarcus.substack

Francesco Fournier-Facio at the University of Cambridge questioned the transparency of the work, arguing that the soficity solution relies heavily on prior papers by Andreas Thom and Gábor Kun from 2016 and 2019. OpenAI's initial claim that all 10 problems "have seen no progress on the main result for at least a decade" was amended after Fournier-Facio complained it was incorrect.newscientist

Broader Implications

Astra itself remains unreleased. OpenAI describes it as a model family built to coordinate multiple agents over extended tasks. CEO Sam Altman has demonstrated the model to policymakers in Washington, but the company has not announced a release date or whether it will ship as GPT-6 or another variant.siliconangle

The timing arrives as the mathematics community pushes back against AI companies. In June, the International Mathematical Union endorsed the Leiden Declaration, warning that AI firms are "using published research without consent, bypassing peer review, and threatening the integrity of proof and attribution".siliconangle