[DigitalToday reporter Seung-a Yoo] OpenAI’s unreleased internal model "Astra", introduced as a next-generation model family, has presented new results on 10 problems in mathematics and theoretical computer science that had remained unsolved for at least 10 years. It also released proofs that can be machine-verified.

On Aug. 2 (local time), foreign media outlets including SiliconANGLE reported that OpenAI released on GitHub a 249-page manuscript, the model’s generated reasoning process and Lean 4-based proof certificates under the Apache 2.0 licence. The released certificate repository showed a "sorry" count of 0. OpenAI explained this means there are no unfinished steps left in the formalised proofs.

A leading result is an explicit construction problem for non-sofic groups that had remained unsolved since Mikhail Gromov (미하일 그로모프) introduced the concept of soficity in 1999. Astra also presented a counterexample to the rigidity conjecture raised by Alain Connes (알랭 콘) in 1980, and said it constructed infinitely many different property (T) groups that share the same von Neumann algebra. It also proved the Ehrhard volume conjecture and claimed to have solved 3 problems from Paul Erdos (폴 에르되시)’s list. These included Problem 183 related to multicolour Ramsey numbers.

Sofic groups refer to groups with a structure that can be approximated by finite permutations. All groups studied so far have been confirmed as sofic groups, but it has not yet been proven that all groups are sofic. Astra claimed it presented an exception that departs from this conventional view. It also said it infinitely constructed different groups that share one fingerprint, unlike the Connes conjecture’s view that, within a certain set of rigid groups, the related algebraic object can uniquely identify the original group.

The remaining results span fields including high-dimensional sphere packing, binary and spherical codes, arithmetic circuit complexity, quantum parallel repetition and the hardness of the closest vector problem. The closest vector problem is also linked to lattice cryptography, and Astra claimed it also presented a counterexample in extremal graph theory to solve 2 additional Erdos problems.

The key to the announcement is the Lean certificates. The Lean kernel determines whether a proof compiles as a binary value, so the model’s claims do not need to be taken on trust at the formal verification stage. Still, mathematicians need to verify whether each formal statement accurately reflects what the original open problems require, and the academic meaning of the results. The 10 results also have not yet undergone peer review.

OpenAI has faced similar controversy in the past. Kevin Weil (케빈 와일), then vice president for science, claimed in 2025 that GPT-5 solved 10 Erdos problems, but Thomas Bloom (토머스 블룸), who runs the Erdos problems database, criticised it as a "dramatic distortion". At the time, the model merely found existing papers, and Weil later deleted the post. Demis Hassabis (데미스 허사비스), chief executive of Google DeepMind, also called it an embarrassing case.

This time, the assessment differed. Bloom called Astra’s results "big news" and said it was a step ahead of a May Erdos unit-distance counterexample produced by an OpenAI internal model that he helped verify.

Astra has not been released. OpenAI said the model family is designed for multiple agents to collaborate over long periods to carry out complex tasks, and is an extension of test-time reasoning research led by research scientist Noam Brown (노엄 브라운). Brown wrote in a post on X, formerly Twitter, that the results were "an important advance in scientific reasoning". OpenAI said a person organised the model’s output into a paper format, but Astra generated the mathematical arguments themselves. The token cost for the 10 solutions was put at about $2,000, based on GPT-5.6 Sol application programming interface rates.

Sam Altman (샘 알트먼) recently demonstrated Astra to policymakers in Washington. OpenAI has not yet decided the release timing, pricing or whether to apply it to GPT-6. Even if it is released, it would have to undergo a federal AI safety review, the same procedure that previously delayed the launch of GPT-5.6.

Separately, the International Mathematical Union backed the Leiden Manifesto and warned that AI companies "use public research without consent, bypass peer review, and threaten the integrity of proof and attribution". Software engineer Fernando Borretti (페르난도 보레티) argued that existing lines of defence by human mathematicians may no longer hold and that AI could change the front line of mathematical research.

OpenAI’s announcement is triggering fresh debate over how academia should verify and accept mathematical results produced by AI, and how to establish copyright and research ethics, beyond the technical achievement itself.

An internal version of Astra, @OpenAI’s next major model family, solved 10 major open problems in mathematics, quantum complexity, and theoretical computer science. We believe it will be a major step for scientific reasoning. https://t.co/iP6cyheZ7i https://t.co/DfBOvi5O8F pic.twitter.com/jHuulDwV46