OpenAI teases Astra, its next major AI model, after it solves 10 long-standing math problems

OpenAI has announced Astra, an upcoming AI model designed to handle complex, long-running tasks, after an internal version solved ten difficult math and computer science problems that had not seen progress for at least a decade. The model works by having human researchers prepare arguments, which Astra then converts into Lean certificates (formal mathematical proofs that can be verified by a computer). OpenAI has not yet decided whether to release Astra as GPT-5.7, GPT-6, or under a different name.