AI formalized the 'Enormous Theorem' in 24 days — the longest proof in history

🤖 AI formalized the longest proof in the history of mathematics in 24 days

Axiom Math announced the first computer-verifiable proof of the Classification of Finite Simple Groups (CFSG, the 'Enormous Theorem') in Lean. The AxiomProver agent swarm generated approximately 43.1 million lines of code in 24 days: 108 milestones, ~380 tasks, under the guidance of mathematicians. The classical proof (~15,000 pages) contained 34 significant discrepancies with the literature, and on October 10, the agents proved the simplicity of the Monster group.

🌍 The formalization revealed actual gaps in published works, and the combination of an agent swarm with Lean turns the multi-year verification of theorems into a manageable process.

👤 AI is already writing proofs and finding counterexamples, but this is currently a statement from a single company without independent peer review.

Source 1: https://axiommath.ai/research/the-enormous-theorem-formalized/ Source 2: https://cryptobriefing.com/axiom-ai-formalizes-enormous-theorem-24-days/