Ten advances in mathematics and theoretical computer science

This article reports on OpenAI's claim of using an internal version of Astra, their next major model, to solve ten mathematical problems that had seen no progress for at least a decade. The solutions were formalized in Lean 4 and published in a repository, with a paper and an LLM-generated PDF reconstructing the proof process. The cost per problem was under $2,000 at GPT-5.6 Sol token prices. The article also discusses the reaction from mathematicians, including an essay by Kirwin Hampshire on a 'spiritual crisis' in the field, and references Terence Tao's concept of 'big mathematics'—a future of human-AI collaboration in mathematical research. The author notes a lack of transparency regarding the prompts used and questions how many problems were attempted without success.