What was released
On August 1, OpenAI published ten mathematics and theoretical-computer-science results from Astra, an unreleased next-generation model, along with manuscripts, reasoning narrations and Lean certificates. The company says the selected problems had seen no progress on their main result for at least a decade.
Topics include high-dimensional sphere packing, binary and spherical codes, non-sofic groups, Connes rigidity, arithmetic-circuit lower bounds, quantum parallel repetition, the closest vector problem, Ehrhart volume, multicolor Ramsey numbers and extremal graph theory. Claims range from new bounds to counterexamples and resolutions.
Division of AI and human work
OpenAI says Astra generated the mathematical arguments, humans prepared manuscripts with the same model, and the model formalized every argument in Lean. It estimates the search tokens would cost roughly $2,000 at Sol API rates.
The company explicitly credits the AI rather than presenting the proofs as wholly human work. A formal certificate can check derivation under encoded assumptions, but it does not by itself establish novelty, significance, or whether the chosen formal statement captures every intended claim.
Importance and remaining verification
Publishing manuscripts and Lean artifacts enables external mathematicians to inspect assumptions, proofs and prior work. This is still an immediate vendor announcement, not completed independent peer review. Each theorem's correctness, relationship to existing literature and formal assumptions needs domain-by-domain scrutiny.