OPENAI'S NEXT MAJOR MODEL ASTRA CLAIMS BREAKTHROUGHS ON 10 LONG-STANDING MATH PROBLEMS

Summary from the TLDR newsletter

OpenAI recently gave a sneak peek into its next model, named Astra. An internal version of the model was able to create breakthroughs on 10 long-standing problems in mathematics and theoretical computer science. The total number of tokens used to discover all ten solutions would have cost around $2,000 at GPT-5.6 Sol API rates. Each solution was formalized in Lean, allowing them to be verified using the theorem-proving system.