Axiom Math's formalization of the Classification of Finite Simple Groups demonstrates the potential of AI in verifying complex mathematical proofs.

So Axiom Math (yet another AI company, of a much smaller size, and whose range seems to be exclusively math) has formalized the Classification of Finite Simple Groups. This is a theorem whose proof is so large that some people doubt the validity of its proof. The formalized proof remains extremely large : 43 million lines of code. I wonder who will try to understand it now… https://axiommath.ai/research/the-enormous-theorem-formalized/

Formalizing the Enormous Theorem (Axiom has formalized in Lean the classification of finite simple groups, the longest proof in the history of mathematics). https://axiommath.ai/research/the-enormous-theorem-formalized/ #LeanProver #ITP #AI4Math #AI #Math

> Formalizing the Enormous Theorem > Axiom has formalized in Lean the classification of finite simple groups, the longest proof in the history of mathematics. > October 26, 2026 > Today, we are releasing the first complete computer-checked proof of the Classification of Finite Simple Groups (CFSG). One of the major achievements of twentieth-century mathematics, the classification identifies the basic building blocks of finite groups. Widely considered to be the longest mathematical proof ever written by humans, the original proof of CFSG extends across roughly 15,000 pages in more than 500 articles by about 100 mathematicians, earning CFSG the nickname “the enormous theorem.” https://axiommath.ai/research/the-enormous-theorem-formalized/ https://en.wikipedia.org/wiki/Classification_of_finite_simple_groups This is now 40 years after the original scattered proof. I have nothing to do with this, but my friend Arunas Rudvalis in 1973 discovered a comparatively small but significant piece, the Rudvalis Group Ru, one of the 26 sporadic groups, constructed by John H. Conway later the same year. https://en.wikipedia.org/wiki/Rudvalis_group I threw a holiday party in 1985, and Arunas showed up a bit late, and burst in saying with excitement, "Do you have the current Scientific American? My name is in it!" > The Enormous Theorem > The classification of the finite, simple groups is unprecedented in the history of mathematics, for its proof is 15, 000 pages long. The exotic solution has stimulated interest far beyond the field. Daniel Gorenstein (1985), "The Enormous Theorem", Scientific American, December 1, 1985, vol. 253, no. 6, pp. 104–115. [Arunas was semi-temporarily in my area for personal reasons; his career was in Amherst.]