Ten advances in mathematics and theoretical computer science

OpenAI set an internal version of Astra, its next major model, on ten problems that had seen no progress on their main results for at least a decade, and reports spending under 2,000 dollars per problem at current token prices. The claimed results span high-dimensional geometry, coding theory, group theory, operator algebras, quantum complexity, and lattice cryptography, including the first improvement to the general sphere-packing exponent since 1978 and a construction addressing the existence of non-sofic groups, open since 1999. To their credit, the artifacts are public: Lean 4 formalizations in the ten-proofs repository, a paper, and reconstructed proof-development traces. The honest caveats travel with the claims. Specialist review of whether the formal statements match the informal ones is still pending, and nobody outside OpenAI knows how many problems consumed the same budget without producing anything. As a shop that pre-registers its own much smaller experiments, we read the publish-the-artifacts posture as the right instinct and the missing failure denominator as the number to ask about.