OpenAI published ten claimed advances in mathematics and theoretical computer science on 1 August, all attributed to an unreleased internal model it calls Astra. The release includes a 249-page collection of full manuscripts and a public Lean repository containing machine-checkable formalizations of every result. No individual mathematician is credited as an author, and no independent expert review has been published.
Key facts
- Ten claimed results spanning sphere packing, coding theory, group theory, operator algebras, circuit complexity, quantum games, lattice hardness, convex geometry, Ramsey theory and extremal graphs.
- The formalization manifest in OpenAI's ten-proofs repository reports zero
sorryplaceholders, meaning nothing in the Lean code is left as an unproved assumption. - Published 1 August 2026, credited to "OpenAI" as a corporate author with no named individuals.
- Primary source: OpenAI's announcement, with the full manuscripts and reasoning walkthroughs as PDFs.
The way to read this release is not "a model solved ten open problems." It is that OpenAI has done something labs rarely do: made an extraordinary claim in a form the outside world can attack. A benchmark screenshot cannot be refuted by a stranger. A theorem can.
Some background helps. Most AI capability claims arrive as scores on tests that the lab chose, ran, and reported. Mathematics does not work that way. A proof is either correct or it is not, and anybody with the relevant training can sit down and find the hole. By publishing manuscripts rather than metrics, OpenAI has swapped a claim nobody can check for ten claims a few hundred specialists worldwide can check - and, unusually, has also encoded each of them in Lean, a proof assistant that mechanically verifies every logical step.
What OpenAI actually says is narrower than the reaction to it. The announcement describes Astra only as "our next major model." It says humans used that same model to help prepare the manuscripts, and that the arguments were subsequently formalized in Lean. It does not disclose the architecture, the prompts, how many problems were attempted, how many attempts failed, how much human steering was involved, or when Astra ships.
The cost figure circulating in coverage needs the same care. OpenAI's "roughly $2,000" is a hypothetical price for the tokens consumed by the searches that found these solutions, quoted at Sol API rates. It is not the cost of the project, not the cost of Astra, and not a cost that includes the attempts that went nowhere. It is closer to the fuel bill for the flights that landed than for the whole flight programme.
A second correction matters more than it looks. The published "reasoning walkthroughs" are not raw chains of thought. The first page of that document says an AI wrote the notes after reading the original reasoning traces and the finished papers. They are retrospective explanations written for readers, not audit logs of what the model did. Anyone treating them as evidence of how Astra thinks is reading the wrong artifact.
The results themselves are specific and bounded in ways the viral summaries flatten. Claim five gives new lower bounds for computing the permanent of a matrix and explicitly does not prove that a famous complexity separation holds. Claim seven proves a hardness result for approximating the closest vector in a lattice and is not a claim that deployed cryptography is broken. Claim eight proves a sharp volume inequality and openly leaves the classification of the equality cases unresolved. Claim one pins down the limit of a well-known linear-programming bound for sphere packing, which is not the same thing as determining the optimal packing density. In each case the paper is more careful than the headline.
There is real external contact, but it is thin. The group-theory manuscript thanks Henry Bradford, Michael Chapman, Alon Dogon and Francesco Fournier-Facio for comments; the operator-algebras chapter thanks Sorin Popa, Francois Charles and Cyril Houdayer for careful readings. Acknowledgments are not endorsements, and none of these researchers has published a verdict.
The honest caveat is about what Lean does and does not settle. A clean Lean build proves that the statement written in Lean follows from Lean's axioms. It does not prove that the statement written in Lean is the theorem the prose manuscript claims - a subtly weaker formal statement can compile perfectly. The decisive next step is an outside team building the repository themselves and auditing whether the formal definitions match the mathematics. OpenAI's own First Proof disclosure is the relevant precedent: it publicly revised a proof assessment after expert feedback and conceded its process was not a clean controlled evaluation.
The surrounding noise should be kept separate from the release. The Information reported on 31 July that OpenAI previewed Astra in Washington; that is secondary reporting, and no first-party record confirms what was shown to whom. Claims that Astra is GPT-6, or ships in September, or self-improves, are extrapolation, not evidence from this publication. This site has covered the earlier round of AI proof claims and Terence Tao's argument that the bottleneck is understanding rather than proof generation; both remain the right frame for reading this one.
Originally published on Ground Truth, where every claim is checked against the primary source.
Top comments (0)