OpenAI's Astra cracks ten decades‑old math problems, proving AI can publish proofs
OpenAI released ten new results spanning sphere packing, coding theory, group theory, and circuit complexity, each discovered by its Astra model with about $2,000 of compute. The proofs were formalized in Lean and accompanied by model narration, proving large‑scale AI can generate publishable mathematics.