OpenAI’s Astra tackles 10 long-standing maths and computer science problems

OpenAI has published ten AI-generated research results that it says resolve or significantly advance long-standing problems across mathematics and theoretical computer science.

The results span high-dimensional geometry, coding theory, group theory, circuit and quantum complexity, lattice cryptography, operator algebras and extremal combinatorics. OpenAI said they were produced using an internal version of Astra, its next major model, before being prepared as manuscripts and formalised in the Lean proof assistant.

The ten results

The company reported advances in the following areas:

• High-dimensional sphere packing: Tighter upper bounds on packing density extending to the Cohn–Elkies threshold.
• Binary and spherical codes: Exponentially stronger bounds on the maximum size of codes with a specified minimum distance.
• Non-sofic groups: A construction demonstrating the existence of non-sofic groups.
• Connes’s rigidity conjecture: A disproof of the conjecture that certain groups are uniquely characterised by their von Neumann algebras.
• Arithmetic circuit complexity: New lower bounds for computing the permanent, including an arithmetic-formula bound of order (n^4/\log n).
• Quantum parallel repetition: An exponential parallel repetition theorem covering general two-player quantum games.
• Closest vector problem: Polynomial-factor hardness-of-approximation results for a lattice problem relevant to post-quantum cryptography.
• Ehrhart’s volume conjecture: A determination of the maximum volume, across all dimensions, of a convex body whose centroid is its sole interior lattice point.
• Multicolour Ramsey numbers: A superexponential lower bound for multicolour triangle Ramsey numbers, resolving Erdős problem 183.
• Extremal graph theory: Results resolving the compactness and degeneracy conjectures associated with Erdős problems 146 and 180.

OpenAI estimated that generating the solutions required a volume of model usage equivalent to roughly $2,000 at Sol API rates. It also released model-generated reasoning walkthroughs and Lean certificates for the arguments.

Significance and scrutiny

The work indicates that advanced AI systems may be moving beyond established benchmark problems toward producing original arguments on unresolved research questions. Several results also concern foundational areas with wider implications, including quantum computation, cryptographic security and computational complexity.

Formalisation in Lean provides a machine-checkable representation of each argument, but it does not remove the need for independent expert scrutiny. The mathematical community will need to examine the assumptions, novelty and broader significance of the results before their standing is fully established.

OpenAI said the mathematical arguments were generated by its system, while people helped prepare the manuscripts and formalise the proofs. The company argued that attribution should clearly distinguish AI-generated reasoning from human-authored research.

The announcement follows OpenAI’s earlier publication of an AI-generated disproof of the Erdős unit-distance conjecture in May. The company is also expanding access to its research models through an initiative offering 100,000 scientists and mathematicians free access to its leading ChatGPT systems, according to the August 1 announcement.