AI·
Ten decade-old math problems fell to an unreleased OpenAI model, for about $2,000 of tokens each
OpenAI published ten results in math and theoretical CS from an internal build of Astra, with Lean 4 certificates for every proof. What that verification does and doesn't settle.