OpenAI's internal version of Astra, its next major model, has produced results on ten long-standing open problems in mathematics and theoretical computer science. The problems span high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography, and extremal combinatorics — many unsolved for decades. Solutions cost roughly $2,000 in compute at API rates. Each result was formalized in Lean, and OpenAI is releasing the proofs alongside narrations of the model's reasoning process. The announcement raises questions about AI attribution in academic research, with OpenAI acknowledging the AI generated the mathematical arguments while humans prepared manuscripts and verified correctness.
