OpenAI has published 10 new results for problems in mathematics and theoretical computer science that had seen no progress on their main results for more than a decade[1]. The work came from an internal version of Astra, which the company describes as its next major model. Every argument was formalized as a Lean certificate, and the model's own narration of how it worked through each problem has been released alongside the results.

Ten problems that had not moved in over a decade

The results cover problems that have been open, with no progress on the main result, for at least 10 years and in most cases far longer[1]. They span high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography and extremal combinatorics. OpenAI says all of them are of substantial interest to their respective mathematical communities, and that several matter across mathematics as a whole.

Here is the full list[1]:

  • High-dimensional sphere packing. New upper bounds on sphere-packing density down to the Cohn–Elkies threshold.
  • Binary and spherical codes. Exponentially improved bounds on the maximum size of binary codes at any prescribed minimum distance, with analogous results for high-dimensional spherical codes.
  • Non-sofic groups. A construction establishing the existence of non-sofic groups, a central open question in group theory.
  • Connes's rigidity conjecture. A disproof of the longstanding conjecture that certain groups are uniquely determined by their von Neumann algebras.
  • Arithmetic circuit complexity. New lower bounds for computing the permanent with arithmetic circuits and formulas, including an arithmetic-formula lower bound on the order of n to the fourth power divided by log n.
  • Quantum parallel repetition. An exponential parallel repetition theorem for general two-player quantum games, extending a foundational principle from classical complexity theory.
  • Closest vector problem. Polynomial-factor hardness of approximation for the closest vector problem, a foundational lattice question tied to post-quantum cryptography.
  • Ehrhart's volume conjecture. Determining, in every dimension, the maximum possible volume of a convex body whose centroid is its only interior lattice point.
  • Multicolor Ramsey numbers. A superexponential lower bound for multicolor triangle Ramsey numbers, resolving Erdős problem 183.
  • Extremal number conjectures. Results on the compactness and degeneracy conjectures in extremal graph theory, resolving Erdős problems 146 and 180.

The list runs from areas close to practical application, such as sphere packing and lattice cryptography, to deeply theoretical territory such as operator algebras. The central claim is not that a specialized solver cracked one problem in its own niche, but that a single model produced results across all of these fields.

The work came from an internal version of Astra

The results were produced by an internal version of Astra, the model OpenAI calls its next major release[1]. According to the company, the total number of tokens needed to find the solutions would cost roughly 2,000 USD (about 320,000 yen) at GPT-5.6 Sol API rates. That is a small figure next to problems the mathematical community has been stuck on for decades.

※1 USD = 158 JPY (as of August 1, 2026)

The model's output was not the end of the process. Humans, working with the same model, turned the arguments into manuscripts. The model then formalized each argument as a Lean certificate, putting the proofs through a proof assistant[1]. That gives the results a machine-checkable backing separate from human peer review. OpenAI is also releasing, for each solution, the model's narration of its own reasoning process.

A follow-on from the May Erdős disproof

This announcement did not arrive out of nowhere. In May 2026, OpenAI shared an AI-generated disproof of the Erdős unit-distance conjecture, found while evaluating an unreleased model[1][2]. The starting point was a question Erdős posed in 1946: place n points on a plane, and count how many pairs sit exactly one unit apart[2].

For decades, mathematicians expected the best configurations to look roughly like square grids. The model instead used algebraic integers to build a more intricate lattice, producing an infinite family of examples that substantially beat the grid-based constructions[2]. What drew attention at the time was that the proof came from a general-purpose reasoning model rather than a system trained specifically for mathematics or scaffolded to search proof strategies. External mathematicians who checked the work validated the approach, though the broader planar unit distance problem itself remains open[3]. OpenAI says the May result has already inspired further work in mathematics and theoretical computer science, citing follow-on papers including one showing that the sum-product conjecture is false for real numbers[1].

How to describe who did the work

OpenAI is as explicit about attribution as it is about the technical content. The company states that the questions raised by systems capable of contributing to mathematical research cannot be answered by a technology company alone[1]. It expresses deep respect and understanding for those concerned about AI's impact on the field, including the signers of the Leiden Declaration on AI and Mathematics.

That declaration is a statement published in June 2026 by an international group of mathematicians responding to rapid AI progress in research-level mathematics, endorsed by the International Mathematical Union[4]. It raises the reliability of automatically generated results, the attribution of results produced with proprietary models, and the effect on publication and peer review. Its recommendations ask researchers to disclose their use of AI tools, take responsibility for the correctness of results, and cite prior work appropriately[4]. It does not call for banning AI from mathematics; it asks for clear community norms.

OpenAI's own position follows the same line. 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 argues[1]. In this case, humans helped prepare the manuscripts and formalize the proofs in Lean and take responsibility for their correctness, while the mathematical arguments themselves were generated by the system. OpenAI is asking the mathematical community to engage with the results, place them in context, and carry the underlying ideas into new research.

Ahead of this announcement, the company also launched ChatGPT for Academic Researchers, giving 100,000 scientists and mathematicians free access to its best ChatGPT models[1]. Its framing is that widespread access is a prerequisite for researchers to define the future of their own disciplines.

Summary

OpenAI has released 10 results for mathematics and theoretical computer science problems that had gone more than a decade without progress, produced by an internal version of its next major model, Astra. The proofs were formalized in Lean and the model's reasoning narration was published with them. Two things landed at once: the fact that roughly 320,000 yen worth of tokens reached problems that had resisted for decades, and the question of whose name belongs on the result.

Source[1]: https://openai.com/index/ten-advances-in-mathematics/

Source[2]: https://openai.com/index/model-disproves-discrete-geometry-conjecture/

Source[3]: https://www.understandingai.org/p/openais-milestone-math-breakthrough

Source[4]: https://www.lms.ac.uk/news/leiden-declaration-on-ai-and-mathematics