Axiom Math kompaniyasi cheklangan oddiy guruhlar tasniflash teoremasining kompyuterli formalallashtirilishini muvaffaqiyatli yakunlaganini eʼlon qildi, bu teorema «Katta teorema» deb ham ataladi. Bu yutuq XX asr matematikasidagi eng muhim yutuqlardan biri hisoblanadi.
Ushbu teorema cheklangan oddiy matematik guruhlarni tasniflash bilan shugʻullanadi, ular istalgan cheklangan guruhlarni shakllantirish uchun fundamental qurilish bloklari boʻlib xizmat qiladi, bu murakkab sonlarning oddiy omillarga boʻlinishiga oʻxshaydi.
Bu teorema isbotidagi ish yarim asrga ortiq davom etdi. Birinchi qadamlar 1963-yilda tashlangan boʻlib, amerikalik matematiklar Walter Feit va John Thompson har qanday noabelian cheklangan oddiy guruhning tartibi juft ekanligini isbotladilar.
Tasnif 1983-yilda Daniel Gorenstein tomonidan yakunlandi. Bundan tashqari, 2004-yilda Michael Ashbacher va Stephen Smith 1221 sahifadan iborat bayonotni nashr etishdi, bu «birinchi avlod isbotining» tugashini bildirdi. Aynan shu ishni Axiom Math kompaniyasi formalallashtirishni oldi.