OpenAI says its next model, Astra, has solved ten open problems in mathematics

OpenAI says an internal version of its next major model, called Astra, has produced ten new results in mathematics and theoretical computer science. Each of the problems had been open for at least a decade. The company published a 249-page manuscript alongside machine-checkable Lean 4 certificates for every result on GitHub.

The headline result is the first-ever explicit construction of a non-sofic group, resolving a central question in group theory that has stood since Mikhail Gromov introduced the concept of soficity in 1999. No mathematician had managed to prove or disprove whether non-sofic groups exist in the 27 years since.

The other results span several fields. Astra disproved Connes’s rigidity conjecture on von Neumann algebras, proved Ehrhart’s volume conjecture, and resolved three problems from Paul Erdos’s famous catalogue, including problem number 183 on multicoloured Ramsey numbers. It also produced the first improvement to the general upper bound on high-dimensional sphere-packing density since 1978, proved a parallel repetition theorem for two-player quantum games, and established new lower bounds on the circuit complexity of computing the permanent.

OpenAI’s head of mathematics research, Sebastien Bubeck, confirmed the results on X, calling them “beautiful” and noting that each ships with a Lean certificate and a chain-of-thought walkthrough. The total compute cost for all ten solutions was roughly $2,000 at Sol API rates, according to OpenAI.

The announcement lands against a backdrop of escalating tension between AI companies and the mathematics community. In June, mathematicians issued the Leiden Declaration, endorsed by the International Mathematical Union, warning that AI companies are using published research without consent, bypassing peer review, and threatening the integrity of proof and attribution. The Declaration specifically cited companies that announce results through press releases rather than peer-reviewed journals.

OpenAI has form on this front. In May it announced that the same long-horizon model family disproved the Erdos unit distance conjecture, an 80-year-old problem in discrete geometry. Fields Medalist Tim Gowers said at the time that he would recommend that proof for publication in Annals of Mathematics without hesitation.

Thomas Bloom, who runs the erdosproblems website, called the latest ten results “big news” on X, saying they are more significant than the unit distance counterexample.

OpenAI has not said when Astra will be released publicly, describing it only as its “next major model.” Some observers, including investor Mark Kretschmann, have speculated that Astra is the GPT-6 series. The company is also giving 100,000 academic researchers free access to its frontier models through 2027, a move that deepens its ties to the scientific community while concentrating research infrastructure on its own platform.

The Lean certificates address a key objection that the mathematical community has raised about AI-generated proofs: that they are difficult to verify independently. Machine-checkable proofs can be validated by anyone with the Lean compiler, without trusting the model or its operators. Whether the broader mathematical community will accept results announced through a blog post rather than a peer-reviewed journal remains an open question, one the Leiden Declaration was written to answer.