Ten Proofs, One Model, Still Unreleased

On August 6, 2026, OpenAI published a 249-page mathematical manuscript alongside Lean 4 proof certificates on GitHub. An internal version of Astra — the company’s next model family, still awaiting public release — had generated solutions to ten open problems in mathematics and theoretical computer science. None of the ten had seen meaningful progress in at least a decade.

The results span six fields: high-dimensional geometry, group theory, quantum complexity, lattice cryptography, coding theory, and extremal combinatorics. OpenAI released the repository under Apache 2.0. The “sorry” count — a measure of unverified proof steps in the Lean formalization language — stands at zero. Every inference step is machine-checkable.

The announcement followed a report from The Information on August 1 that OpenAI was building Astra as a multi-agent system designed for tasks that take hours or days to complete. The math paper was the first concrete demonstration of what that architecture can do.

What Was Actually Solved

The most significant result is the first explicit construction of a non-sofic group. The concept of soficity was formalized by Mikhail Gromov in 1999; whether any group fails to satisfy it has been an open question in group theory for 27 years. Astra produced a construction — and Lean 4 verified it.

The model also disproved Connes’s rigidity conjecture on von Neumann algebras, proved Ehrhart’s volume conjecture in high-dimensional geometry, and resolved three problems from Paul Erdős’s catalog, including problem 183 on multicolor Ramsey numbers. Resolving three at once is unusual even by human standards.

The remaining results cover lattice cryptography and coding theory — areas with direct implications for post-quantum security research. OpenAI published both the 249-page manuscript and a walkthrough of the model’s reasoning for each problem.

$2,000 for Decades of Unsolved Work

OpenAI states that the tokens used to generate all ten solutions would cost approximately $2,000 at current Sol API rates. Noam Brown, one of the researchers behind Astra’s test-time reasoning technology, was explicit: “Sadly, no Millennium Prize Problems (yet). But also, we didn’t spend a lot on each problem. It’s possible to push test-time compute much further.”

The $2,000 figure covers inference only — not training compute, the researchers who formalized proofs in Lean, or the human-model collaboration required to produce publishable papers. OpenAI acknowledged that researchers worked with Astra to prepare the manuscripts. The company cited the Leiden Declaration on AI and Mathematics as a framework for credit attribution.

What Mathematicians Said

Thomas Bloom at the University of Manchester called the results “big news,” ranking them above a previous counterexample to the unit distance conjecture. Bloom also rejected the “AI is replacing mathematicians” framing: the model draws on a century of mathematical theory, was built by mathematicians, and was trained on everything mathematicians have written. Without that accumulated human knowledge, he argued, the claim is incoherent.

That framing matters. Astra did not bootstrap mathematical intuition from scratch. It applied pattern recognition at scale across a deep corpus to find connections researchers had missed. Whether that differs qualitatively from human mathematical insight is philosophical — but the field takes verified proofs seriously regardless of origin.

What Astra Is and What Comes Next

Astra is still not public. OpenAI has not decided whether to release it as GPT-6 or a GPT-5 variant. Astra is framed as a multi-agent architecture where specialized agents coordinate on problems for hours or days — not a single general-purpose model. The math results are presented as evidence this design handles extended high-stakes reasoning without compounding errors, which remains a persistent weakness in current agentic systems.

Lean 4 verification changes the trust surface for AI-generated proofs. Formalizing an argument in Lean forces every claim into machine-checkable form. The zero “sorry” count is not marketing — Lean would have rejected any missing or unjustified step. Brown’s comment signals that harder problems are next. The seven Millennium Prize Problems — each worth $1 million from the Clay Mathematics Institute — are presumably on the list. For software engineers, AI-assisted formal verification is becoming infrastructure with direct applications in software correctness and cryptography.

Further Reading

• OpenAI’s Ten Proofs Manuscript (PDF) — The 249-page paper; start with the executive summary
• The Decoder: OpenAI Astra Announcement — Detailed reporting on the math paper and the Astra architecture
• AI for Mathematics: Progress, Challenges, and Prospects — A survey of where AI-assisted mathematics stands and what remains out of reach