Ten advances in mathematics and theoretical computer science

Source: OpenAI Date: 2026-08-01 URL: https://openai.com/index/ten-advances-in-mathematics

Summary

OpenAI published ten results to open mathematics and theoretical-computer-science problems — spanning high-dimensional sphere packing, binary/spherical coding bounds, a construction of a non-sofic group (resolving a longstanding open question), and a counterexample to Connes’s rigidity conjecture — attributed to Astra, described as OpenAI’s next major model, each accompanied by Lean proof certificates and chain-of-thought walkthroughs. These are problems with no progress on the main result for at least a decade.

Implications

• The two model clocks. This is a closed-model capability signal disguised as a research post: “Astra” is named as an upcoming model, and formally verified (Lean-certified) novel mathematical results are a much harder capability claim to fake or overstate than a benchmark score — worth treating as a leading indicator of Astra’s eventual capability positioning ahead of any formal launch announcement.
• Watch: whether Astra’s eventual launch post references this math release as evidence, and whether competing labs (Anthropic, Google DeepMind, open-weight labs) respond with their own verified-proof claims — formal verification could become the next capability battleground the way benchmark suites were for GPT-5.5.