On August 1, OpenAI announced that its internal model Astra had, in one run, cracked 10 long-standing open problems in mathematics and theoretical computer science. On August 7, the same model was partially suspended by OpenAI itself — development paused, model weights encrypted, tool access restricted — pending a U.S. government security review. In one week, the same model broke records in mathematics and then got locked down: arguably the most telling week of 2026's first half for AI research's shifting identity.
What Astra Actually Solved
The 10 problems span 8 subfields:
- Group theory: an explicit construction of a non-sofic group (open since Gromov introduced soficity in 1999)
- Von Neumann algebras: a refutation of the Connes rigidity conjecture
- High-dimensional geometry: a new upper bound on sphere-packing density, improving a record dating to 1978
- Three Erdős problems, including multicolor Ramsey number #183
- Arithmetic circuit complexity: lower bounds on the permanent
- Quantum games: an exponential parallel repetition theorem
- Post-quantum cryptography: polynomial-factor hardness for the Closest Vector Problem
- Fields medalist Timothy Gowers said he would recommend one of the papers to a top journal "without hesitation."
- Thomas Bloom (University of Manchester), maintainer of the Erdős problems list, called the August results "big news," going further than May's Erdős unit distance round (which had been reviewed by 9 mathematicians jointly).
- Most commentators — including AI critic Gary Marcus — were positive about the results themselves but reserved judgment on whether every problem counts as a true breakthrough, noting some were technically "advanceable" but simply "not being watched."
- Suspension of parts of Astra's internal development
- Isolated testing environments
- Restricted network and tool access
- Encrypted model weights
- Real-time monitoring of high-risk behaviors
Everything Was Formalized in Lean 4
This is the biggest difference from earlier "an LLM wrote a paper that looks right" moments. OpenAI released a 249-page research manuscript, a 62-page reasoning walkthrough, and Lean 4 proof certificates (open-sourced on GitHub under Apache 2.0). The README reports a sorry count of zero — any step not rigorously grounded in prior steps would be rejected by the Lean kernel. Anyone with a Lean compiler installed can independently verify every step of all 10 results, without reading OpenAI's paper or trusting its wording. This is the largest single hammer-drop ever for machine-checkable mathematics.
$2,000 Is a Real Number — but Read It Carefully
At GPT-5.6 Sol API rates, the token cost for Astra to find all 10 solutions was roughly $2,000. But three caveats matter:
1. The 10 problems were selected by OpenAI itself. 2. The figure excludes problems the model attempted but failed. 3. OpenAI researchers participated in writing the manuscript and the formalization.
So $2,000 cannot represent the total cost of mathematical discovery — but it is genuinely the cost of the published, formalized proofs.
The Math Community's Response
Then, the August 7 Reversal
OpenAI's internal evaluation found that Astra's agentic coding and cybersecurity capabilities made it impossible to rule out crossing the "Critical" cybersecurity capability threshold defined in its Preparedness Framework. The Critical tier means a model can, without human intervention, discover and weaponize zero-day exploits against multiple hardened real-world critical systems, or plan and execute novel end-to-end cyberattack campaigns from only a high-level objective.
This is the first time OpenAI has judged any specific model as *possibly* reaching Critical. Measures taken include:
The Real Paradigm Signal of the Week
The significance of the Astra line isn't the 10 problems themselves — it's that in one week it fused two things that previously belonged to separate threat models:
1. "AI can produce research the mathematics community accepts" 2. "An AI of the same capability level can no longer be safely handed to the public"
In other words, the pace of single-point frontier capability breakthroughs is approaching the upper limit of what regulators can keep up with. This week, OpenAI demonstrated with its own product that the next real constraint on frontier AI research is neither algorithms nor compute, but the safety-gate design of "how to release different pieces at different times" — which is itself the true research problem.
Two Things Worth Watching
1. Concrete milestones of Astra's security review and release — any acceleration or delay will rewrite market expectations for frontier model pacing. 2. The migration of Lean-style formal verification from mathematics to software engineering — DeepMind has extended this chain to verified code generation (see the Vero benchmark), showing that the discipline of replacing "looks right" with "verifiable by a trusted checker" is landing simultaneously in AI research and AI coding.