OpenAI's Next Model Solves Ten Open Math Problems

OpenAI says an internal version of Astra resolved ten open math problems, including three Erdős problems, for roughly $2,000 in compute, with Lean-formalized proofs released for verification.