OpenAI's Astra Solves Ten Decade-Old Math Problems with Machine-Checkable Lean Proofs

OpenAI's Astra Solves Ten Decade-Old Math Problems with Machine-Checkable Lean Proofs

OpenAI has officially confirmed the name of its next major AI model family, Astra, by announcing a historic mathematical breakthrough achieved by an unreleased internal version of the model. On August 1, 2026, OpenAI revealed that Astra solved ten long-standing open problems in mathematics and theoretical computer science that had seen no progress on their main results for at least a decade. To guarantee the mathematical community of their validity, OpenAI released machine-checkable Lean certificates for each proof on GitHub.

According to OpenAI's official announcement, the unreleased model operates as a multi-agent system coordinating over extended periods:

"The results were achieved by an internal version of Astra, our next major model. The total number of tokens needed to find solutions to these problems would cost roughly $2,000 at Sol API rates.¹ These arguments were then prepared into manuscripts by humans with the same model. Afterward, the model formalized each argument in a Lean certificate." — OpenAI: Ten advances in mathematics and theoretical computer science

The ten solved problems span high-dimensional geometry, cryptography, quantum complexity, and extremal combinatorics, including:

1. High-dimensional sphere packing: New upper bounds on sphere-packing density down to the Cohn–Elkies threshold.
2. Binary and spherical codes: Exponentially improved bounds on the maximum size of binary codes at any prescribed minimum distance.
3. Non-sofic groups: A construction establishing the existence of non-sofic groups, addressing a central open question in group theory.
4. Connes’s rigidity conjecture: Disproof of a longstanding von Neumann algebra conjecture.
5. Arithmetic circuit complexity: New lower bounds for computing the permanent using arithmetic circuits and formulas.
6. Quantum parallel repetition: An exponential parallel repetition theorem for general two-player quantum games.
7. Closest vector problem: Polynomial-factor hardness of approximation for the closest vector problem, a foundational lattice question related to post-quantum cryptography.
8. Ehrhart’s volume conjecture: Determining, in every dimension, the maximum possible volume of a convex body whose centroid is its only interior lattice point.
9. Multicolor Ramsey numbers: A superexponential lower bound for multicolor triangle Ramsey numbers, resolving Erdős problem 183.
10. Extremal number conjectures: Results on the compactness and degeneracy conjectures in extremal graph theory, resolving Erdős problems 146 and 180.

Human-AI Collaboration and the Leiden Declaration

OpenAI acknowledged the delicate ethical and academic questions surrounding AI-generated scientific discoveries, specifically citing the Leiden declaration on AI and Mathematics:

"The emergence of systems capable of contributing to mathematical research raises questions that cannot be answered by a technology company alone... 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." — OpenAI: Ten advances in mathematics and theoretical computer science

This milestone highlights a transition from traditional pattern-matching LLMs to deep, long-horizon reasoning systems. While the model remains internal and unreleased, the demonstration of formalizing complex mathematical reasoning via automated theorem provers (like Lean) signals a major leap toward AI as a genuine collaborator in scientific discovery.