Axiom used swarms of AI agents to check the classification of finite simple groups in 43.1 million lines of Lean, and found errors in the published proof.