A empresa Axiom Math anunciou a conclusão bem-sucedida da formalização computacional do teorema de classificação dos grupos simples finitos, também conhecido como 'Teorema Gigante'. Este feito é considerado um dos avanços mais significativos na área da matemática do século XX.
Este teorema trata da classificação dos grupos matemáticos simples finitos, que são blocos de construção fundamentais para a formação de quaisquer grupos finitos, de forma análoga à divisão de números complexos em fatores primos.
O trabalho no provamento deste teorema durou mais de meio século. Os primeiros passos foram dados em 1963, quando os matemáticos americanos Walter Feit e John Thompson provaram que a ordem de qualquer grupo simples finito não abeliano é par.
A classificação foi concluída definitivamente em 1983 por Daniel Gorenstein. Além disso, em 2004, Michael Ashbacher e Stephen Smith publicaram uma exposição de 1221 páginas, marcando o fim da chamada prova de primeira geração. Foi este trabalho que a Axiom Math assumiu a formalização.