OpenAI publishes 10 research advances generated by unreleased Astra model

5 Aug

The results span mathematics and theoretical computer science, with manuscripts, Lean certificates and reconstructed reasoning walkthroughs released for expert scrutiny

Mathematical notation and diagrams appear across a digital grid. The image accompanies OpenAI’s release of research generated by its internal Astra model. — ***OpenAI says an internal version of its Astra AI model generated ten results across mathematics and theoretical computer science***

OpenAI has published ten results in mathematics and theoretical computer science that it says were generated by an internal version of Astra, its next major AI model. The work includes proposed resolutions of open conjectures alongside new bounds and substantial progress on other long-standing problems.

A 249-page collection sets out the arguments across high-dimensional geometry, coding theory, group theory, operator algebras, arithmetic circuit complexity, quantum complexity, lattice cryptography and extremal combinatorics.

Colin Fleming, Chief Marketing Officer, Business at OpenAI, presented the results more categorically on LinkedIn: “Not benchmark questions. Problems that had yet to be solved.”

OpenAI’s technical account is more qualified. It states that each result either resolves or makes substantial progress on an open problem, rather than claiming that all ten problems have been fully solved.

From sphere packing to quantum complexity

Among the results, the Astra model produced new upper bounds for high-dimensional sphere-packing density. The accompanying paper describes this as the first improvement to the general sphere-packing exponent since 1978.

For binary and spherical codes, OpenAI reports exponentially improved bounds on the maximum code size at prescribed minimum distances. The collection also presents a construction intended to establish the existence of non-sofic groups and a proposed disproof of Connes’s rigidity conjecture.

Further results cover new lower bounds for calculating the permanent using arithmetic circuits and formulas, including a formula lower bound of order n⁴/log n. In quantum complexity, the model generated an exponential parallel repetition theorem for general two-player quantum games.

A direct reduction from 3SAT produced polynomial-factor hardness of approximation for the closest vector problem, which OpenAI identifies as a lattice problem connected to post-quantum cryptography.

The remaining work includes a proposed proof of Ehrhart’s volume conjecture in every dimension, a superexponential lower bound for multicolor triangle Ramsey numbers and findings addressing compactness and degeneracy conjectures in extremal graph theory. The Ramsey and graph theory work covers Erdős problems 183, 146 and 180.

Human preparation and formalization in Lean

OpenAI says Astra generated the mathematical arguments before humans prepared them as manuscripts using the same model. Astra then formalized each argument in a Lean certificate.

The company estimates that the tokens required to find the solutions would have cost approximately $2,000 at Sol API rates. This figure covers the model’s solution-finding process, according to OpenAI, rather than the subsequent human preparation or wider research costs.

Responsibility for the published work remains with the company. OpenAI states: “We helped prepare the manuscripts and formalize the proofs in Lean, and we take responsibility for their correctness, while the mathematical arguments themselves were generated by our system.”

It argues that attributing an entirely AI-generated proof to human authors would misrepresent both the model’s contribution and human intellectual work. OpenAI also acknowledges concerns about the role of AI in mathematics, including those expressed by signatories to the Leiden declaration on AI and Mathematics.

Alongside the manuscripts and Lean certificates, OpenAI has released narrated walkthroughs for each result. The accompanying notes describe these as reconstructions produced by an AI model after reading the original reasoning chains and completed papers. They cover successful ideas, obstacles and changes in approach, rather than serving only as summaries of the finished proofs.

The results follow an AI-generated disproof of the Erdős unit-distance conjecture shared by OpenAI in May. The company says that earlier finding has already prompted further work in mathematics and theoretical computer science.

OpenAI is also providing 100,000 scientists and mathematicians with free access to its best ChatGPT models through ChatGPT for Academic Researchers. The manuscripts, Lean certificates and reasoning walkthroughs for the Astra results have now been released for examination by the mathematical community.