The company published machine-checkable Lean 4 proofs on GitHub for all 10 results, including the first explicit construction of a non-sofic group
Cheng Xin / Getty Images
OpenAI announced Saturday that Astra, its next major model still awaiting public release, had generated solutions to 10 longstanding problems across mathematics and theoretical computer science, each unsolved for ten or more years. Alongside the announcement, OpenAI released a 249-page manuscript and Lean 4 proof certificates on GitHub under an Apache 2.0 license; the repository's "sorry" count stands at zero, indicating that every step across all ten formalized proofs is fully verified.
Chief among the findings is an explicit construction of a non-sofic group, settling a question that has gone unanswered since Mikhail Gromov laid out the concept of soficity in 1999. Astra also disproved Connes's rigidity conjecture on von Neumann algebras, proved Ehrhart's volume conjecture, and resolved three problems from Paul Erdős's catalog, including problem 183 on multicolor Ramsey numbers, according to SiliconAngle. Additional results span high-dimensional sphere packing, binary and spherical codes, arithmetic circuit complexity, quantum parallel repetition, and the hardness of the closest vector problem.
OpenAI put the total compute cost for all 10 solutions at roughly $2,000 at GPT-5.6 Sol API rates. The company's head of mathematics research, Sebastien Bubeck, confirmed the results on X $TWTR, calling them "beautiful," according to The Next Web. Research scientist Noam Brown called the results "a major step for scientific reasoning" in a post on X. OpenAI credited Astra with the underlying mathematical reasoning, while human researchers worked the model's output into papers suitable for publication.
Thomas Bloom, who curates the erdosproblems.com database, described the ten results as "big news" on X, placing their significance above the unit distance counterexample that an internal OpenAI model generated in May, according to The Next Web.
Because Lean's kernel either accepts or rejects a proof outright, independent verification requires nothing more than running the certificates through the compiler. However, none of the 10 results has been through peer review, according to SiliconAngle.
The announcement comes against a backdrop of friction between AI companies and the mathematics community. The International Mathematical Union's June endorsement of the Leiden Declaration formalized the community's concerns, with the declaration charging that AI companies exploit published research without permission, sidestep peer review, and erode standards around proof and credit.
OpenAI has not given a release date for Astra. OpenAI recently cut prices on two models in its GPT-5.6 family after efficiency improvements during internal development, while Sol pricing — the rate used to calculate the $2,000 Astra compute cost — remained unchanged.
OpenAI has yet to clarify whether Astra will carry a GPT-6 designation or slot into the existing GPT-5 line, and the model will need to clear the federal AI safety review before it can reach users.
Join 500,000+ readers who start their day with Quartz.
By subscribing, you agree to our Terms of Service and Privacy Policy.
