OpenAI has revealed that an internal version of Astra, its next major AI model family, has produced new results on 10 longstanding open problems spanning mathematics, quantum complexity, and theoretical computer science.
The company said each problem had remained unresolved for at least a decade, with machine-checkable proofs published alongside the announcement for independent verification.
According to OpenAI, Astra generated advances across multiple research areas, including high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, lattice cryptography, extremal combinatorics and quantum complexity.
Rather than releasing only benchmark scores, the company published formal proofs and supporting research documents to allow mathematicians to evaluate the results.
In a research post, OpenAI described Astra as “next major model” and said the results were generated using an internal version of Astra. The model is not yet available to the public.
The company published machine-checkable proofs for each result, saying the work resolves or makes substantial progress on 10 longstanding open problems in mathematics and theoretical computer science.
“The total number of tokens needed to find solutions to these problems would cost roughly $2,000 at Sol API rates,” it said.
The company said the AI-generated arguments were later prepared into research manuscripts by humans using the same model. It added that the proofs were then formalised as Lean certificates, while also releasing the model’s narration of its reasoning process for each result.
The results span several areas of mathematics and computer science. They include new bounds for high-dimensional sphere packing and binary codes, a construction proving the existence of non-sofic groups, a disproof of Connes’ rigidity conjecture, new lower bounds in arithmetic circuit complexity, and progress on quantum complexity, lattice cryptography and graph theory.
Alongside the research announcement, OpenAI also said it recently launched ChatGPT for Academic Researchers, an initiative that will provide 1,00,000 scientists and mathematicians with free access to its most capable ChatGPT models.
OpenAI acknowledged that AI-generated mathematical research raises broader questions about authorship and attribution.
“We believe attribution should honestly reflect how a result was produced: claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system’s contribution and the nature of genuine human intellectual work,” the company said.
It added that while it helped prepare the manuscripts and formalise the proofs in Lean, “the mathematical arguments themselves were generated by our system”. OpenAI said it hopes the mathematical community will evaluate the results, build on them and define how AI should be used in future mathematical research.
In May, OpenAI disclosed that one of its internal reasoning models had autonomously disproved a long-standing conjecture in discrete geometry that had remained unsolved for nearly 80 years. At the time, external mathematicians described the result as a milestone for AI-assisted mathematical research.
OpenAI argued that mathematics provides a rigorous environment for evaluating advanced reasoning because proofs can be formally verified.
Shortly after OpenAI’s announcement, Anthropic researcher Levent Alpöge said in a post on X that the company’s Claude Fable model had independently solved five of the same problems in under 24 hours. Anthropic has not published a paper verifying the results.
Your reaction
Discussion
What's your take on this story?
No comments yet — be the first to share your view.