OpenAI Astra: Lean 4–Verified Solutions to 10 Open Math Problems, Then a Safety Lockdown

Forum topic · QianXun · 2026-08-23

Summary

On August 1, 2026, OpenAI announced that an internal model called Astra solved ten long-standing open problems in mathematics and theoretical computer science, delivering the results as Lean 4 formal proofs with zero sorry-count, alongside a 249-page manuscript and a 62-page reasoning walkthrough, all released under Apache 2.0. The corpus covers an explicit construction of a non-sofic group, a disproof of the Connes rigidity conjecture, a new upper bound on sphere packing density, Erdős problems including multi-color Ramsey bounds, permanent circuit-complexity lower bounds, an exponential parallel-repetition theorem for quantum games, and post-quantum lattice hardness results. Estimated inference cost on the GPT-5.6 Sol API is roughly USD 2,000, though OpenAI selected the targets and co-wrote the write-ups. On August 7, OpenAI paused portions of Astra's development after internal evaluation suggested possible Critical-tier cyber capabilities under the Preparedness Framework, encrypting weights, restricting tools, and gating any public release behind U.S. government review.

Overview

In a single week, OpenAI's internal model Astra demonstrated large-scale formal mathematical reasoning and was subsequently locked down for safety review. The August 1 announcement described ten solved open problems across mathematics and theoretical computer science, all formalized in Lean 4. Six days later, on August 7, OpenAI paused portions of Astra's development after flagging a possible Critical-tier cybersecurity capability under its Preparedness Framework, pending U.S. government review.

What Astra solved

The ten problems span eight sub-fields:

Group theory: an explicit construction of a non-sofic group (open since Gromov introduced soficity in 1999).
Operator algebras: a disproof of the Connes rigidity conjecture.
High-dimensional geometry: a new upper bound on sphere packing density, improving the standing record from 1978.
Erdős problems: three items, including a bound related to the multi-color Ramsey number R(183).
Arithmetic circuit complexity: a lower bound on the permanent.
Quantum games: an exponential parallel-repetition theorem.
Post-quantum cryptography: a polynomial-factor hardness result for the closest-vector problem on lattices.

Lean 4 formalization — the key shift

Unlike prior LLM-generated papers that merely *look* correct, OpenAI published the proofs as Lean 4 certificates with a reported sorry count of 0. Releases include:

A 249-page research manuscript
A 62-page reasoning walkthrough
Lean 4 proof certificates on GitHub under Apache 2.0

Any reader with a Lean compiler can independently verify every step without trusting OpenAI's prose — the largest concentrated demonstration to date of *machine-checkable mathematics*.

The USD 2,000 figure, broken down

At GPT-5.6 Sol API rates, the token cost to derive all ten solutions is approximately USD 2,000. Caveats:

1. OpenAI selected the ten problems; failed attempts are not reported. 2. OpenAI researchers co-authored the write-ups and formalization. 3. The number represents the cost of *published, formalized proofs*, not the full cost of mathematical discovery.

Community reception

Timothy Gowers (Fields Medalist): would unhesitatingly recommend at least one paper to a top journal.
Thomas Bloom (University of Manchester, maintainer of the Erdős problems table): called the August results "big news," surpassing the May Erdős unit-distance breakthrough that nine mathematicians jointly verified.
Gary Marcus and other AI critics: positive on the results, reserved on whether every item counts as a true breakthrough — some problems were technically *near-tractable* but *unwatched*.

The August 7 reversal

Internal evaluation could not rule out Astra reaching Critical-tier cyber capability, defined as:

> The model can, without human intervention, discover and develop multiple effective zero-day exploits against hardened real-world critical systems, *or* devise and execute novel end-to-end attack strategies from high-level goals alone.

This is the first time OpenAI has flagged a specific model as *possibly Critical-tier*. Imposed measures:

Partial pause of Astra's internal development
Isolated test environments
Restricted network and tool access
Encrypted model weights
Real-time monitoring of high-risk behavior

Public release is gated on passing U.S. government review; no timeline has been announced. OpenAI clarified that Astra was not involved in the earlier Hugging Face security incident.

Why the week matters

The signal is not the ten problems themselves, but the *coupling* of two formerly separate threat models in one product cycle:

1. AI producing mathematics that the research community accepts. 2. AI of comparable capability no longer being safely deliverable to the public.

Frontier capability gains are outpacing regulators' ability to keep up. OpenAI has effectively self-demonstrated that the next binding constraint on frontier model development is safety-gate design — the discipline of releasing capabilities in carefully staggered fragments. That gating problem is itself now a research problem.

Two threads worth watching

1. Astra's safety-review milestones. Any acceleration or delay will reshape market expectations of frontier-model pacing. 2. Migration of Lean-style formal verification from mathematics to software engineering. DeepMind's Vero benchmark for verified code generation suggests the same discipline — replace "looks right" with "a trusted checker can verify it" — is landing simultaneously on both AI research and AI coding fronts.