
Lead story
OpenAI's next model has a name, Astra, and ten proofs a machine can check
OpenAI published ten results in mathematics and theoretical computer science on 1 August, produced by an internal version of its next model, Astra. Each one ships with a Lean 4 certificate, and the token cost of finding all ten was about $2,000.


















