OpenAI has published ten AI-generated mathematical discoveries produced with its internal model Astra, accompanied by a 249-page research paper, a 62-page process explanation, and formal Lean 4 proofs released on GitHub. The results span high-dimensional geometry, coding theory, group theory, quantum complexity, lattice cryptography, and extremal combinatorics — including solutions to longstanding Erdős problems and newly constructed non-Sofic groups. The work was a human-AI collaboration: Astra generated proofs, researchers refined them into papers, and Astra then translated results into Lean 4 for formal verification. OpenAI estimates inference costs at roughly $2,000 in API tokens. Each paper will undergo independent peer review, and the formal proofs allow researchers to verify logical correctness independently. The release signals a broader industry shift toward AI contributing to scientific discovery rather than just software and content tasks.
