Ten advances in mathematics and theoretical computer science

<p><strong><a href="https://openai.com/index/ten-advances-in-mathematics/">Ten advances in mathematics and theoretical computer science</a></strong></p> A few days ago it was Anthropic <a href="https://simonwillison.net/2026/Jul/28/discovering-cryptographic-weaknesses-with-claude/">discovering cryptographic weaknesses with Claude</a> using Mythos Preview, spending $100,000 on tokens and with prompts that included "again we are not looking for low hanging fruit, we want proper research to find genuinly hard findings."</p> <p>Now it's OpenAI's turn to flex. They set "an internal version of Astra, our next major model" on finding solutions to ten mathematical problems that "have seen no progress on the main result for at least a decade". They claim to have spent less than $2,000 at GPT-5.6 Sol token prices on each one.</p> <p>(No news on how many problems they spent $2,000 on <em>without</em> reaching a solution though.)</p> <p>The <a href="https://github.com/openai/ten-proofs">openai/ten-proofs</a> repository has Lean 4 formalizations of their results, and there's also <a href="https://cdn.openai.com/pdf/ten-proofs-oai.pdf">a paper</a> describing the solutions and an additional <a href="https://cdn.openai.com/pdf/reasoning-walkthroughs.pdf">LLM-generated PDF</a> where the model "reconstructs how the proof came together" based on the unpublished reasoning traces.</p> <p>That's a decent level of transparency, but I want to see the prompts they used!</p> <p>A lot of mathematicians online are experiencing a collective burst of <a href="https://simonwillison.net/2026/Feb/15/deep-blue/">Deep Blue</a>.</p> <p>OpenAI's results reminds me of what Terence Tao described as "big mathematics" in <a href="https://spectrum.ieee.org/ai-in-mathematics">IEEE Spectrum in June</a>:</p> <blockquote> <p>Unlike some of his peers, Tao is neither dismissive of AI nor fearful. Instead, he sees it as the catalyst for a fundamental shift in the discipline—a transition toward what he calls “big m