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

UPDATED 18:21 EDT / AUGUST 02 2026 AI OpenAI’s Astra solves 10 long-open math problems and publishes the proofs by Duncan Riley OpenAI Group PBC revealed Saturday that an internal version of Astra, the model family it calls its next major release, produced new results for 10 problems in mathematics and theoretical computer science that had been open for at least a decade, and it published machine-checkable proofs alongside the claim. The company posted a 249-page manuscript collection, model-written reasoning walkthroughs and Lean 4 certificates for all 10 results. The certificates sit on GitHub under an Apache 2.0 license, and the repository reports a “sorry” count of zero, meaning no step in any of the formalized proofs has been left unproven. The headline result is an explicit construction of a non-sofic group, a question left open since Mikhail Gromov introduced soficity in 1999. Astra also disproved Connes’s rigidity conjecture, constructing infinitely many non-isomorphic groups with property (T) that share the same von Neumann algebra, and it proved Ehrhart’s volume conjecture. Three problems from Paul Erdős’s catalog fell as well, including problem 183 on multicolor Ramsey numbers. Stripped of the terminology, a group is the mathematical description of a set of symmetries, and a sofic group is one whose structure can be approximated by shuffling a finite deck of cards. Every group anyone had examined turned out to be sofic, and no one could prove that all of them are. Astra built the exception. Connes’s conjecture, posed in 1980, held that for one rigid class of groups, a related algebraic object acts as a unique fingerprint, pinning down the group it came from. Astra produced infinitely many distinct groups sharing a single fingerprint. Erdős problem 183 is about Ramsey numbers. Color the links in a network with a fixed number of colors and past a certain size you cannot avoid a triangle whose three links match. The Ramsey number is the size at which that becomes true. The remainder of the list runs across high-dimensional sphere packing, binary and spherical codes, arithmetic circuit complexity, quantum parallel repetition and the hardness of the closest vector problem, the last of which bears on lattice cryptography. Astra also produced counterexamples in extremal graph theory, resolving two more Erdős problems. The Lean certificates are what give the announcement its weight. Lean’s kernel returns a binary verdict, either the proof compiles or it does not, which takes trust in the model out of the equation. What it does not take out is the need for a mathematician to confirm that each formal statement says what the open problem actually asks and to judge whether the result matters. None of the 10 has been through peer review. OpenAI has been here before. The company’s then vice president of science, Kevin Weil, claimed in October 2025 that GPT-5 had solved 10 previously unsolved Erdős problems. Thomas Bloom, who maintains the erdosproblems.com database, called that “a dramatic misrepresentation.” The model had found papers in the literature that Bloom was personally unaware of. Weil deleted the post, and Google DeepMind Chief Executive Demis Hassabis called the episode embarrassing. Bloom called the Astra results “big news” and rated them ahead of the Erdős unit distance counterexample an internal OpenAI model produced in May, a paper he helped verify. Astra itself remains unreleased. OpenAI describes it as a model family built to run long tasks by coordinating multiple agents over extended periods, an extension of the test-time reasoning work associated with research scientist Noam Brown, who called the results “a ma