OpenAI Reveals Astra, Its Next Major Model Family, by Publishing Ten Solved Math Problems

What happened

On August 1, 2026, OpenAI published a blog post titled "Ten advances in mathematics and theoretical computer science." The third paragraph contained the first official confirmation of Astra, which OpenAI calls its "next major model family." The post announced that an internal version of Astra had solved ten open problems in mathematics and theoretical computer science, each of which had been open for at least a decade.

The results span high-dimensional geometry, coding theory, group theory, operator algebras, quantum complexity, lattice cryptography, and extremal combinatorics. The headline result is the first explicit construction of a non-sofic group, resolving a central question in group theory that has stood since Mikhail Gromov introduced the concept of soficity in 1999. Other results include a counterexample to Connes's rigidity conjecture on von Neumann algebras, a proof of Ehrhart's volume conjecture, the first improvement to the general upper bound on high-dimensional sphere-packing density since 1978, an exponential parallel-repetition theorem for finite two-player entangled games, and three problems from Paul Erdős's famous catalogue closed, including problem 183 on multicolored Ramsey numbers.

OpenAI released a 249-page manuscript alongside a 62-page account of the model's discovery paths and Lean 4 formalizations for the principal results on GitHub. Lean is a proof assistant that can mechanically check whether a formal argument follows from its stated assumptions. The formalization manifest reports no unfinished sorry goals and lists only standard Lean axioms, but labels the review status "agent-reviewed" rather than peer-reviewed.

According to OpenAI's research announcement, Astra generated the mathematical arguments. Humans then used the same model to prepare them as manuscripts, after which Astra formalized each argument in Lean. OpenAI said the tokens used to generate all ten solutions would have cost approximately $2,000 at its Sol API rates. Sebastien Bubeck, OpenAI's head of mathematics research, confirmed the results on X, calling them "beautiful." Noam Brown, an OpenAI research scientist who works on reasoning and multi-agent systems, wrote that Astra represents a "major step for scientific reasoning."

Astra is a multi-agent model family designed for long-running tasks lasting hours or days. CEO Sam Altman has already showcased the technology to policymakers and regulators in Washington, D.C. Astra is expected to become the first system evaluated under a planned U.S. government framework requiring federal pre-release approval. OpenAI has not yet determined whether Astra will launch publicly as GPT-6 or as a variant within the GPT-5 lineup. The naming convention of the GPT-5.6 series—Terra (earth), Luna (moon), Sol (sun)—suggests Astra ("the stars") may be another GPT-5.6 variant.

Why it matters

The announcement is notable for two reasons. First, OpenAI chose to reveal its next major model family not with a product launch but with a research artifact: ten proofs, each machine-checkable via Lean 4, covering problems that had resisted human mathematicians for decades. Second, the Lean formalizations mean anyone can independently verify the proofs without trusting OpenAI. A Lean-checked argument is not the same as a peer-reviewed one—the human community still has to agree the formalized statement matches the intended mathematical claim—but it represents a higher standard of verifiability than typical AI benchmark announcements.

The closest-vector result strengthens worst-case hardness evidence relevant to lattice cryptography, but OpenAI clarified it does not provide an attack on deployed post-quantum systems. The broader significance is that Astra gives OpenAI its clearest evidence that frontier models may generate auditable research results, potentially opening a market for AI systems sold as discovery infrastructure.

This follows OpenAI's earlier disclosure in May 2026 that another AI-generated result had produced a claimed disproof of the Erdős unit-distance conjecture during testing of an unreleased model.

What to watch

• Peer-review reception of the ten proofs by the broader mathematics community.
• The U.S. government review process for Astra, which could become a template for future frontier model approvals.
• Whether Astra launches as GPT-6 or as a GPT-5.6 variant.
• Whether other frontier labs adopt Lean-formalized proof releases as a standard for AI-generated mathematical claims.