OpenAI published a blog post describing an unreleased model, referred to as Astra, that produced machine-checkable Lean proofs for ten decade-old mathematics problems. The Telegraph and BleepingComputer reported the claims based on the company post. No independent verification of the problems' prior unsolved status or the proofs' novelty has appeared in the cited sources.