OpenAI says an internal model found new proofs for ten open math problems
OpenAI reports that an internal version of its next major model, Astra, produced new results on ten long-standing open problems in geometry, coding theory, complexity, and cryptography, with humans formalizing the arguments in Lean. Here's what shipped and what it means for how we assign credit to AI-generated mathematics.
OpenAI announced on August 1, 2026 that an internal version of Astra, its next major model, produced new results on ten open problems spanning high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography, and extremal combinatorics. Every problem had seen no progress on its main result for at least a decade, and in most cases much longer.
This follows OpenAI's May disclosure of an AI-generated disproof of the Erdős unit-distance conjecture, found while evaluating an unreleased model. That result has already drawn follow-on work from independent mathematicians and computer scientists, cited in the announcement's footnotes, which is the detail worth sitting with: the community engaged with a machine-generated result on its mathematical merits, not as a curiosity.
The ten results
Stated plainly, the results are: new upper bounds on sphere-packing density approaching the Cohn–Elkies threshold; exponentially improved bounds on binary and spherical code sizes at a given minimum distance; a construction proving non-sofic groups exist, closing a central question in group theory; a disproof of Connes's rigidity conjecture, which held that certain groups are uniquely determined by their von Neumann algebras; new lower bounds for computing the permanent with arithmetic circuits, including a formula-size bound of order n⁴/log n; an exponential parallel repetition theorem for two-player quantum games; polynomial-factor hardness of approximation for the closest vector problem, a lattice question that underpins post-quantum cryptography; a full resolution, in every dimension, of Ehrhart's volume conjecture; a superexponential lower bound on multicolor triangle Ramsey numbers, resolving Erdős problem 183; and results on the compactness and degeneracy conjectures in extremal graph theory, resolving Erdős problems 146 and 180.
That's three of Erdős's open-problem list closed in one release, plus a disproof of a conjecture that had stood in operator algebras for decades. Regardless of how the results were produced, the list would be a strong year for a research group.
How the results were produced
OpenAI's account of the pipeline is specific: Astra generated the mathematical arguments, at a total token cost the company puts at roughly $2,000 at Sol API rates. Humans then worked with the same model to prepare the arguments into manuscripts. After that, the model formalized each argument as a Lean certificate — a machine-checkable proof object, not a natural-language sketch a reviewer has to take on faith. OpenAI also released the model's narration of its own reasoning for each result, alongside the reasoning walkthroughs and the underlying paper.
The Lean step is the load-bearing one. A natural-language proof from a language model is a claim; a Lean certificate is a checkable object that either type-checks against the formal statement or doesn't. That's what lets OpenAI say, as it does in the announcement, that it takes responsibility for the correctness of the results while attributing the mathematical arguments themselves to the system.
Who gets credit for a proof a model wrote
OpenAI is explicit that it won't claim human authorship for arguments a model generated, and it points to the Leiden declaration on AI and Mathematics as a marker of how contested this is inside the field. That's the right instinct. Attribution that quietly folds a model's contribution into human authorship erodes the record faster than it protects anyone's ego, and it's a bad precedent for a field that runs on precise credit.
What I'd watch next is independent replication and, more interesting to me, what mathematicians do with the reasoning walkthroughs rather than just the certificates. A Lean proof tells you a result is true; it doesn't tell you why the approach worked or what else it generalizes to. The May Erdős result already produced five or six papers extending the idea in directions the original disproof didn't take. If that pattern holds for these ten, the actual value of this release won't be the theorems — it'll be the reasoning traces treated as research leads, which is a different and, I think, more durable way for a model to contribute to a field than either "tool" or "author" quite captures.
The production lesson generalizes past mathematics: pair a generative model with a verifier that doesn't grade on a curve — Lean here, tests and formal specs in software — and separate "who proposed this" from "who is accountable for it being correct." That split is doing more work in this announcement than the ten results themselves.