OpenAI has offered an early look at Astra, its next frontier model, by describing how an internal version produced new results on ten long-standing open problems in mathematics and theoretical computer science. The company states that the total computational effort required to generate the solutions amounted to roughly two thousand dollars in tokens at current GPT-5.6 Sol rates, after which the same system formalized the arguments in Lean so that the proofs could be machine-checked. Manuscripts, Lean certificates, and model-generated reasoning walkthroughs are being released for scrutiny by the wider mathematical community.
The problems were chosen because their central claims had seen no meaningful progress for a decade or longer. They span high-dimensional geometry, coding theory, group theory, quantum complexity, lattice-based cryptography, operator algebras, and extremal combinatorics. Among the claimed advances are tighter upper bounds on sphere-packing density that reach the Cohn–Elkies threshold, exponentially improved bounds on binary and spherical codes, a construction of non-sofic groups, a disproof of Connes’s rigidity conjecture for certain von Neumann algebras, new lower bounds on arithmetic circuits for the permanent, an exponential parallel-repetition theorem for quantum games, polynomial-factor hardness results for the closest-vector problem, a resolution of Ehrhart’s volume conjecture across all dimensions, a superexponential lower bound on multicolor triangle Ramsey numbers, and progress on compactness and degeneracy conjectures in extremal graph theory.
Formal verification in Lean removes one common source of doubt, yet the deeper questions of significance and novelty remain for specialists to settle. Mathematical discovery has long mixed human insight with mechanical assistance, from early computer-assisted proofs to more recent systems that generate candidate lemmas. What is newer is the scale at which a single model can propose complete arguments across such varied domains and then package them for peer examination. The modest token budget cited for the discovery phase is notable only against the backdrop of the enormous training costs that precede any such run; it does not erase the broader resource asymmetry between industrial labs and academic groups.
Whether these results hold under independent review will determine how much they actually shift the research landscape. Even verified formal proofs can rest on subtle assumptions or fail to illuminate the underlying structure in ways that advance further work. OpenAI’s decision to publish the full trail of reasoning invites that examination rather than asking the community to accept the claims at face value. In fields where progress has stalled for years, any credible new avenue is worth testing, but the test itself must still be conducted by people who understand the problems deeply enough to know when a claimed breakthrough is genuine and when it is merely cleverly packaged.
