एक्ज़िओम मैथ कंपनी ने सीमित सरल समूहों के वर्गीकरण के प्रमेय, जिसे 'विशाल प्रमेय' भी कहा जाता है, के कंप्यूटर औपचारिकरण के सफल समापन की घोषणा की है। इस उपलब्धि को बीसवीं सदी के गणित के क्षेत्र में सबसे महत्वपूर्ण सफलताओं में से एक माना जाता है।
यह प्रमेय सीमित सरल गणितीय समूहों के वर्गीकरण से संबंधित है, जो किसी भी सीमित समूह के निर्माण के लिए मौलिक निर्माण खंड हैं, ठीक उसी तरह जैसे जटिल संख्याएँ अभाज्य गुणनखंडों में विभाजित होती हैं।
इस प्रमेय के प्रमाण पर काम आधे शताब्दी से अधिक समय तक चला। पहले कदम 1963 में उठाए गए थे, जब अमेरिकी गणितज्ञ वॉल्टर फेइट और जॉन टम्पसन ने सिद्ध किया कि किसी भी गैर-एबेलियन सीमित सरल समूह का क्रम सम होता है।
वर्गीकरण को 1983 में डेनियल गोरेनस्टाइन द्वारा अंतिम रूप दिया गया था। इसके अलावा, 2004 में माइकल आसबाहर और स्टीवन स्मिथ ने 1221 पृष्ठों का एक विवरण प्रकाशित किया, जिसने तथाकथित पहली पीढ़ी के प्रमाण के समापन का प्रतीक था। इसी कार्य को एक्ज़िओम मैथ कंपनी ने औपचारिक रूप देने का जिम्मा लिया।