Ten advances in mathematics and theoretical computer science
OpenAI Blog · 2026-08-01
OpenAI's internal Astra model generates new results on ten long-standing open problems in mathematics and theoretical computer science — including disproving Connes's rigidity conjecture and constructing non-sofic groups — with each proof formally verified in Lean.
Extraction
Topics: ai-mathematical-researchformal-verificationllm-capabilitiestheorem-provingextremal-combinatorics
Claims
- An internal version of OpenAI's Astra model produced new mathematical results on ten problems that had been open for at least a decade, spanning geometry, coding theory, group theory, and quantum complexity.
- The total compute cost to find all ten solutions was approximately $2,000 at Sol API rates.
- Each proof was formalized in a Lean certificate after human-assisted manuscript preparation using the same model.
- OpenAI argues that claiming human authorship for AI-generated proofs misrepresents both the AI's contribution and the nature of human intellectual work, and that attribution must honestly reflect how results were produced.
- The earlier AI-disproof of the Erdős unit-distance conjecture has already spawned multiple subsequent published results by human researchers.
Key quotes
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.
The total number of tokens needed to find solutions to these problems would cost roughly $2,000 at Sol API rates.
Today, we are sharing a selection of ten results to problems that have been open and have seen no progress on the main result for at least a decade, and in most cases much longer.