Axiom Verifies 15,000 Page Mathematical Proof With New AI Agents

Axiom's AI system spent 24 days translating the 15,000-page Classification of Finite Simple Groups into the Lean programming language for automated verification. Operating with human guidance, the company's agents converted the proof into checkable logical steps while repairing errors found in the original text, creating a version that other researchers can verify without manual review.