Ten advances in mathematics and theoretical computer science

Blog · Read

• OpenAI claims an internal version of its next model (“Astra”) solved ten long-standing math problems — each with “no progress on the main result for at least a decade” — for under $2,000/problem at GPT-5.6 Sol token prices.
• Formal Lean 4 proofs published in the openai/ten-proofs repo, alongside a paper and an LLM-generated PDF narrating the proof development.
• Willison flags a transparency gap: no disclosure of the prompting/scaffolding methodology used to get there, making the result hard to independently assess or reproduce.
• Connects it to mathematician Kirwin Hampshire’s essay “The Dark Night of Mathematics” on AI’s growing role in the field — floats a future where humans focus on creative direction and AI absorbs the computational grind.