Axiom says AI agents formalized the Classification of Finite Simple Groups in Lean

Axiom, an AI math company, announced on X a complete Lean auto-formalization of the Classification of Finite Simple Groups, a result it calls the "periodic table of symmetry". It describes the original proof as about 15,000 pages written by over 100 mathematicians across generations, and calls it the largest math proof in history to be computer-verified.

According to Axiom's open-source repository, swarms of AI agents produced about 43.1 million lines of Lean in 24 days, covering 715 papers and books, and flagged 34 deviations from the published record. A post by the AI news account TestingCatalog adds that the agents split the work like software teams and wrote code faster than Lean could check it.

These figures are Axiom's own account; no independent review of the formalization is part of the announcement. The post had about 6,200 likes on X by October 28.