OpenAI's unreleased Astra model solved 10 math problems that stumped humans for a decade
2026-08-07
Astra produced machine-checkable Lean 4 proofs for ten open problems across eight fields of math — for about $2,000 in compute. The proofs are on GitHub under Apache 2.0, so nobody has to take OpenAI's word for it.