Axiom Math announced the successful completion of the computer formalization of the classification theorem of finite simple groups, also known as the 'Monster Theorem'. This achievement is considered one of the most significant successes in the field of 20th-century mathematics.
This theorem deals with the classification of finite simple mathematical groups, which are fundamental building blocks for forming any finite group, analogous to how complex numbers are divided into prime factors.
Work on the proof of this theorem continued for more than half a century. The first steps were taken in 1963 when American mathematicians Walter Feit and John Thompson proved that the order of any non-abelian finite simple group is even.
The classification was finally completed in 1983 by Daniel Gorenstein. Furthermore, in 2004, Michael Ashbacher and Stephen Smith published a 1221-page exposition, marking the completion of the so-called first-generation proof. It was this work that Axiom Math undertook to formalize.