OpenAI's unreleased 'Astra' model claims ten advances in maths and theoretical CS, with Lean proofs
On 1 Aug 2026 OpenAI published 'Ten advances in mathematics and theoretical computer science' by an internal model, Astra (released as GPT-6 Astra on 3 Sep). It came with a 249-page manuscript and Lean 4 proofs. The claims include the first explicit non-sofic group, a disproof of Connes's rigidity conjecture, the first improvement to the sphere-packing upper-bound exponent since 1978, and solutions to Erdős problems #146, #180 and #183.
Key facts
- Claims: explicit non-sofic group (Gromov's question, ~1999); disproof of Connes's rigidity conjecture; quantum parallel repetition for general two-player entangled games
- Also: Ehrhart volume conjecture (partial per some sources); polynomial-factor NP-hardness of approximating the Closest Vector Problem; permanent circuit lower bound ~n⁴/log n
- Superexponential lower bound for multicolour Ramsey numbers (Erdős #183); Erdős #146 and #180; improved binary and spherical codes
- Sphere-packing upper-bound exponent ~0.5990558 → ~0.6044005, first improvement since Kabatiansky–Levenshtein (1978)
- Evidence: 249-page PDF, Lean 4 proofs (openai/ten-proofs); < $2,000 of tokens per solution at GPT-5.6 Sol prices; prompts not released
- Attribution dispute: Andreas Thom (11 Sep, guest post on Tao's blog) says the non-sofic proof relies crucially on his 2019 work with Gábor Kun (Prop. 2.3 of OpenAI's PDF) despite OpenAI's 'decade without progress' framing, and asks whether his own ChatGPT conversations about these techniques reached the model; Mark Sellke replied 'that did not happen'. Kun and Thom posted a follow-up, arXiv 2608.06222 (6 Aug)
- Independent audit (arXiv 2608.14673): 'No confirmed substantive mathematical error in a principal result remains'; one chapter needs major revisions, and some stronger results were not reproduced
Science result
- Field
- mathematics / group theory, operator algebras, combinatorics, complexity theory, coding theory
- Problem
- Ten open problems incl. existence of explicit non-sofic groups, Connes rigidity, Erdős #146/#180/#183, sphere-packing bounds
- Result
- Claimed resolutions or improvements on ten open problems, most with Lean-formalised proofs.
- AI system
- Astra (GPT-6 Astra)
- Human role
- Largely autonomous per OpenAI; humans selected problems and checked
- Verification
- Formal proofs in Lean for most results; independent human audit found no remaining substantive error in principal results
- Status
- confirmed
- Why surprising
- A single unreleased model produced in one batch results that specialists would count as career highlights, including a question Gromov asked about 25 years earlier.
What happened
OpenAI released, in one announcement, ten research results produced by an internal model a month before its launch. Most came with machine-checked proofs.
Why it matters
It moved the frontier from individual AI-assisted results to a lab producing batches of significant theorems. An independent audit largely upheld them.
Changelog
- 2026-09-29: added Andreas Thom's attribution critique of the non-sofic result, Kun–Thom follow-up paper, MathOverflow thread
- 2026-09-29: created
Related posts (2)
- On the existence of non-sofic groups Andreas Thom (guest post on Terence Tao's blog) · blog · 2026-09-11
A group theorist whose 2019 work underpins OpenAI's 'first explicit non-sofic group' publicly disputes OpenAI's framing and asks whether users' private ChatGPT conversations fed the model that raced them to publication. - Returning from OpenAI's summit on the future of mathematics: 'The End of Mathematics' talk Daniel Litt @littmath · x · 2026-08-11
A leading AI-sceptical mathematician's account of OpenAI's closed-door 'future of mathematics' summit, where Bubeck asked him to describe the future to avoid, in which humans are mathematically disempowered.
Related events
- OpenAI releases GPT-6 Astra, its first GPT-6 model ★★★★★
- OpenAI says an internal model resolved 100+ long-standing open problems in 24 days of training; no list released ★★★
- GPT-5.6 Sol Ultra proves the 50-year-old cycle double cover conjecture ★★★★★
- GPT-6 Astra lowers the bounded prime gaps record from 246 to 186 ★★★★
- Pre-release GPT-6 Astra disproves the Köthe conjecture (1930) with a Lean-verified counterexample ★★★★
Sources (8)
- officialOpenAI: Ten advances in mathematics and theoretical computer science
- paperOpenAI: ten proofs manuscript (PDF)
- discussionA Human Audit of OpenAI's AI-Generated Mathematical Proofs (arXiv 2608.14673)
- discussionSimon Willison on the ten advances
- discussionAndreas Thom (guest post on Tao's blog): On the existence of non-sofic groups (attribution concerns)
- paperKun & Thom: Nonsofic wreath products of residually finite groups (arXiv 2608.06222)
- discussionMathOverflow: key new ideas in the non-soficity proof
- pressQuanta: Why the legendary Erdős problems are falling to AI
id: 2026-08-01-openai-astra-ten-advances · updated 2026-09-29 · open in the interactive timeline