Ten advances in mathematics and theoretical computer science
Simon Willison · Simon Willison · 2026-08-01
OpenAI reports that an internal model solved ten mathematical problems unsolved for over a decade at under $2,000 per problem, publishing Lean 4 formalizations and prompting mathematicians to compare the moment to Deep Blue's defeat of Kasparov.
Appears in
Extraction
Topics: ai-math-reasoningllm-researchopenaiformal-verificationai-scientific-discovery
Claims
- OpenAI used an internal version of its next major model ('Astra') to solve ten mathematical problems with no main-result progress for at least a decade.
- OpenAI claims each problem was solved for less than $2,000 at GPT-5.6 Sol token prices, though no data on failed attempts was disclosed.
- Lean 4 formalizations of the ten proofs are publicly available in the openai/ten-proofs GitHub repository.
- The results are producing a 'Deep Blue moment' among mathematicians, with some reporting existential crisis about the future of the discipline.
- Terence Tao envisions AI enabling 'big mathematics'—large-scale human-machine collaborations where humans claim creative work and AI handles technical grunt work.
Key quotes
(No news on how many problems they spent $2,000 on without reaching a solution though.)
He envisions a future of large-scale, decentralized collaborations between humans and machines, where complex mathematical tasks can be diced and sliced, with humans claiming the creative parts and AI doing the lion's share of the technical grunt work.
A lot of mathematicians online are experiencing a collective burst of Deep Blue.