OpenAI introduced its next major model family on August 1, 2026, not with a benchmark chart but with ten solved research problems. An internal, unreleased version of the model — named Astra — generated original solutions to ten open questions in mathematics and theoretical computer science, none of which had seen progress on the main result in at least a decade. Each solution was published alongside a Lean 4 formalization on GitHub and a walkthrough of the model's reasoning.
The headline result is the first explicit construction of a non-sofic group, settling a question Mikhail Gromov raised in 1999 about whether every countable group can be approximated by finite permutations. "Yes, nonsofic groups exist," wrote OpenAI researcher Sébastien Bubeck in announcing the release on X, calling it "one of many new beautiful results proved by Astra, our next major model."
Key Highlights
- Ten results, spanning group theory, operator algebras, high-dimensional geometry, coding theory, arithmetic circuit complexity, quantum complexity, lattice cryptography and extremal combinatorics.
- Every proof formalized in Lean 4 and published on GitHub, so each logical step can be checked by a program rather than trusted on the author's word.
- Roughly $2,000 in total token cost at OpenAI's Sol API rates — about $200 per decade-open problem.
- A 249-page manuscript plus per-result chain-of-thought walkthroughs accompanies the release.
- Astra is not available. No pricing, no benchmarks, no release date, and no final decision on whether it ships as GPT-6 or a point release.
Details
The ten results are unusually varied for a single announcement. Beyond the non-sofic group, Astra produced a disproof of Connes's rigidity conjecture in von Neumann algebra theory, a proof of Ehrhart's volume conjecture in every dimension, and the first improvement to the general upper bound on high-dimensional sphere packing since 1978 — a bound that now matches the Cohn-Elkies threshold.
The rest lean toward complexity and combinatorics: exponentially improved bounds on binary and spherical code sizes, new arithmetic circuit lower bounds for computing the permanent, an exponential parallel repetition theorem for every finite two-player entangled game, and polynomial-factor hardness of approximation for the closest vector problem. Three Erdős problems fell as well — numbers 146, 180 and 183, the last a superexponential lower bound on multicolour triangle Ramsey numbers.
OpenAI is explicit about the division of labour. Astra generated the core mathematical arguments and formalized them; human researchers prepared the manuscripts for publication. The company states that claiming human authorship of the arguments would misrepresent how they were produced — a notable stance given the ongoing dispute over attribution in AI-assisted mathematics.
Impact
The Lean certificates are what separate this from previous AI-mathematics announcements. The standard failure mode of such claims is a plausible chain of reasoning that quietly hand-waves past the one step that actually mattered; a Lean kernel does not accept hand-waving. Anyone can clone the repository and re-verify the proofs without trusting OpenAI's characterization of them.
The price figure is doing heavy lifting in the coverage, and it deserves scrutiny. The roughly $2,000 covers the successful runs. OpenAI researcher Noam Brown acknowledged that the team attempted other major problems and came up empty: "Sadly, no Millennium Prize Problems (yet)." He also noted that per-problem spend was low, implying more test-time compute could push results further. What the announcement does not disclose is the denominator — how many problems were attempted, how many runs failed, and what the full experimental bill came to.
For working researchers, the shift is less about the ten theorems than about where the bottleneck now sits. Ramsey numbers do not feed anyone, though the closest-vector-problem hardness result touches the foundations of lattice-based post-quantum cryptography. The more consequential change is that generating a candidate proof of a decade-open problem has a printed price, and verifying it has become the scarcer skill.
Background
The announcement lands in an already tense period. In July, Anthropic's Claude Fable 5 helped produce a counterexample to the Jacobian conjecture, an 87-year-old problem, in dimensions three and higher — a result mathematician Levent Alpöge posted to X and that Kevin Buzzard's community subsequently formalized in Lean. Thomas Bloom, the Manchester mathematician who maintains the Erdős problems database, called the Astra release "big news," and bigger than earlier results this year.
Bloom has also pushed back on the framing that AI is replacing mathematicians, noting that these systems draw on more than a century of theory built by mathematicians and were trained on everything mathematicians have written. In June 2026, an international group published the Leiden Declaration on Artificial Intelligence and Mathematics, endorsed by the International Mathematical Union and signed within a day by more than a thousand researchers, including Terence Tao, Peter Scholze, Kevin Buzzard and Scott Aaronson. Its objection is not to AI but to training without consent, bypassing verification, and failing to attribute — and it warns specifically that evaluation suffers when results are communicated through press releases and blog posts rather than papers.
What's Next
Astra remains unreleased, and OpenAI has published no benchmarks or launch window. The open questions are whether the ten results survive peer review, what the undisclosed failure rate looks like, and whether the same approach generalizes beyond problems that can be checked mechanically. Formal verification works cleanly for theorems; most scientific claims do not come with a kernel that can reject them.
Source: OpenAI