We Hid Mistakes in 28 Proofs. GPT-6, Claude, Gemini and Grok Caught Every One

Axiom says it has released "the first complete computer-checked proof of the Classification of Finite Simple Groups" (blog, Oct 26, 2026): the original proof runs to roughly 15,000 pages by about 100 mathematicians, and Axiom says its engineers and mathematicians directed dozens of agents for 24 days to turn it into about 43.1 million lines of Lean, a language a computer checks step by step. Axiom says it found 34 noteworthy deviations from the published record along the way, and that "Humans inspect that statement and the definitions it uses to confirm that it expresses the intended classification."