OpenAI says an internal version of its next major artificial intelligence model has produced new results on 10 longstanding problems in mathematics and theoretical computer science, highlighting the growing role of AI systems in advanced scientific research.
The company said the results were generated by an internal version of Astra, described as its next major model. The issues had remained open with no progress on the main result for at least a decade in each case, and in many instances much longer..
The research spans areas including high-dimensional geometry, coding theory, group theory, operator algebras, quantum complexity, lattice cryptography and extremal combinatorics.
OpenAI said the model produced results for issues of substantial interest to their respective mathematical communities, with several also having broader relevance across mathematics.
Among the results, the system produced new upper bounds for high-dimensional sphere packing that reach down to the Cohn-Elkies threshold. It also generated improved bounds for the maximum size of binary codes at prescribed minimum distances, alongside related results for high-dimensional spherical codes.
In group theory, OpenAI said the work included a construction establishing the existence of non-sofic groups, addressing a longstanding open question. The system also produced a disproof of Connes’s rigidity conjecture, which concerns whether certain groups are uniquely determined by their von Neumann algebras.
Other results involved arithmetic circuit complexity, including new lower bounds for computing the permanent using arithmetic circuits and formulas. OpenAI said the work included an arithmetic-formula lower bound of order n⁴/log n.
READ: AI just got cheaper: OpenAI slashes prices by up to 80% (July 31, 2026)
The model also produced an exponential parallel repetition theorem for general two-player quantum games, extending a foundational principle from classical complexity theory. In lattice-based mathematics, the research produced a polynomial-factor hardness of approximation result for the closest vector problem, a foundational question with connections to post-quantum cryptography.
The remaining results covered Ehrhart’s volume conjecture, multicolor Ramsey numbers and extremal graph theory. OpenAI said the work on multicolor Ramsey numbers produced a superexponential lower bound for multicolor triangle Ramsey numbers and resolved Erdős concern 183.
The company also said results concerning compactness and degeneracy conjectures in extremal graph theory resolved Erdős problems 146 and 180. OpenAI said the total number of tokens required to find solutions to the concerns would cost approximately $2,000 at Sol API rates.
The mathematical arguments were subsequently prepared into manuscripts by humans working with the same model, according to OpenAI. The company said the model’s arguments were then formalized into Lean certificates, a process intended to provide machine-checkable verification of the proofs.
OpenAI is also releasing narrations of the model’s reasoning for each solution, according to the company. The announcement comes as AI companies increasingly position their models as tools for scientific discovery rather than systems limited to conventional tasks such as writing, coding and information retrieval.
OpenAI said its goal is to empower scientists and mathematicians with tools that can accelerate discovery. The company recently announced an initiative offering free access to its best ChatGPT models to 100,000 scientists and mathematicians. The company also acknowledged that the use of AI in mathematical research raises questions about authorship, attribution and the role of human researchers.
READ: Altman meets US lawmakers, discusses new models and security breach incident (July 30, 2026)
OpenAI said attribution should accurately reflect how a result was produced and argued that claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system’s contribution and the nature of human intellectual work.
The company said humans helped prepare the manuscripts and formalize the proofs in Lean, while the mathematical arguments themselves were generated by its AI system. OpenAI also said it takes responsibility for the correctness of the work.
The announcement is likely to intensify discussion about how AI-generated mathematical discoveries should be evaluated and credited. OpenAI said it hopes the mathematical community will examine the results, place them in context and build on the ideas through further research.
The results also raise broader questions about the potential role of increasingly capable AI systems as research collaborators. While the company presented the work as a significant step, the mathematical community will ultimately need to assess the underlying arguments and their implications independently.
For OpenAI, the results represent another attempt to demonstrate that advanced AI models can contribute to difficult problems that have challenged researchers for years.
The company’s announcement suggests that the next phase of AI development could increasingly involve collaboration between mathematical researchers and AI systems capable of generating, testing and formalizing complex arguments.


