OpenAI announced on August 1, 2026 that an internal version of Astra, its next major model, produced new results on ten open problems in mathematics and theoretical computer science that had seen no main-result progress for at least a decade. Domains include high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography, and extremal combinatorics.
Arguments were generated by Astra; humans prepared manuscripts with the same model; each argument was formalized into a Lean certificate. OpenAI cites roughly $2,000 total inference cost at Sol API rates. Lean formalizations are published at github.com/openai/ten-proofs. The company also releases model narrations of thinking processes. Attribution follows the Leiden declaration on AI and Mathematics: mathematical arguments attributed to the system; OpenAI takes responsibility for correctness of manuscripts and formalizations.
Commercial naming (GPT-6 vs GPT-5.x) and release timing remain undecided. Continuity with May 2026 Erdős unit-distance disproof noted.