The one that matters
OpenAI's next model cracks ten long-stuck math problems
OpenAI says an internal version of Astra, its next major model, produced solutions to ten problems in mathematics and theoretical computer science that had seen no progress for at least a decade, at under $2,000 in tokens per solved problem at GPT-5.6 Sol prices. It published a paper, Lean 4 formalizations, and model-written reasoning walkthroughs.
Why it matters
Machine-checkable Lean proofs make these results stand on their own: verification is the difference between a benchmark claim and new mathematics. Simon Willison's caveat is the right one, OpenAI has not said how many problems it spent money on without a solution, but ten decade-old problems is a real capability marker.
