Axiom Math ने समूहों के वर्गीकरण का 43.1 मिलियन पंक्तियों वाला Lean प्रमाण जारी किया

Axiom Math ने 27 अक्टूबर, 2026 को कहा कि वह परिमित सरल समूहों के वर्गीकरण का पहला पूर्ण कंप्यूटर-सत्यापित प्रमाण जारी कर रही है। इंजीनियरों और गणितज्ञों ने दर्जनों AI एजेंटों के समूहों का निर्देशन करते हुए इसे 24 दिनों में तैयार किया; इन एजेंटों ने Lean प्रूफ असिस्टेंट में लगभग 43.1 मिलियन पंक्तियों का कोड लिखा।

कंपनी ने अपनी घोषणा में लिखा, “आज हम परिमित सरल समूहों के वर्गीकरण (CFSG) का पहला पूर्ण कंप्यूटर-सत्यापित प्रमाण जारी कर रहे हैं।” यह वर्गीकरण परिमित समूहों के बुनियादी निर्माण-खंडों की पहचान करता है। इसका मूल प्रमाण लगभग 100 गणितज्ञों के 500 से अधिक लेखों में फैले करीब 15,000 पृष्ठों का है—इसी विशाल आकार के कारण इसे ‘विशाल प्रमेय’ का उपनाम मिला।

Axiom ने क्या जारी किया

CFSG के अनुसार, हर परिमित सरल समूह या तो अभाज्य कोटि का चक्रीय समूह होता है, कम-से-कम पाँच प्रतीकों पर बना प्रत्यावर्ती समूह होता है, परिमित क्षेत्रों पर निर्मित Lie प्रकार के समूहों के 16 अनंत परिवारों में से किसी एक का सदस्य होता है, या ठीक 26 अलग-थलग अपवादात्मक समूहों में से एक होता है। घोषणा में कहा गया है कि कुछ लेखक Tits समूह को 27वाँ समूह मानते हैं। सबसे बड़ा अपवादात्मक समूह, Monster, Robert Griess ने 1980 में 196,884 विमाओं वाले बीजगणित का उपयोग करके निर्मित किया था।

इस प्रमाण पर मनुष्यों का काम कई दशकों तक चला। 1963 में Walter Feit और John Thompson ने 255 पृष्ठों के एक शोधपत्र में सिद्ध किया कि हर गैर-आबेलियन परिमित सरल समूह की कोटि सम होती है। यह शोधपत्र Pacific Journal of Mathematics के एक पूरे अंक में समाया था। Daniel Gorenstein ने 1972 में वर्गीकरण पूरा करने के लिए 16 चरणों का कार्यक्रम प्रस्तुत किया और 1983 में इसे पूरा घोषित किया। लेकिन क्वासिथिन मामले का आधार Geoffrey Mason की एक अधूरी पांडुलिपि थी। Michael Aschbacher और Stephen Smith ने 2004 में 1,221 पृष्ठों का विवरण प्रकाशित किया, जिससे वह काम पूरा हुआ जिसे बाद में पहली पीढ़ी का प्रमाण कहा गया। Gorenstein और Richard Lyons ने दूसरी पीढ़ी का अधिक व्यवस्थित प्रमाण शुरू किया, जिसमें बाद में Ronald Solomon और Inna Capdeboscq भी शामिल हुए; यह प्रमाण अब भी अधूरा है। इसलिए Axiom ने पहली पीढ़ी के प्रमाण को औपचारिक रूप दिया।

परियोजना का पृष्ठ इस औपचारिकीकरण को पहली पीढ़ी के प्रमाण का अनुसरण करने वाले ऐसे काम के रूप में प्रस्तुत करता है, जिसमें Lean का कर्नेल हर तार्किक चरण की जाँच करता है। इस पृष्ठ के अनुसार, इसमें Lean की 43.1 मिलियन पंक्तियाँ, 2.05 मिलियन घोषणाएँ और इसके संग्रह में 715 शोधपत्र व पुस्तकें शामिल हैं। Axiom का कहना है कि उसके प्रमाण-मानचित्र का आधार दूसरी पीढ़ी के खंड थे और इस औपचारिकीकरण में पहले की Qiuzhen-CFSG परियोजना के लगभग 1.2 मिलियन कोड-पंक्तियाँ शामिल हैं। यह Mathlib पर भी आधारित है, जिसके लिए कंपनी ने सैकड़ों योगदानकर्ताओं को श्रेय दिया है। परियोजना में Dean Cureton, Vasily Ilin, Bhavik Mehta और Niels Voss को मुख्य योगदानकर्ता तथा Letong Hong को प्रधान अन्वेषक बताया गया है।

सार्वजनिक GitHub रिपॉज़िटरी इस नतीजे को ऐसा Lean4 प्रमाण बताती है जिसमें कोई `sorry` नहीं है। यह संस्करण 4.35.0-rc3 पर स्थिर है, Mathlib और TauCeti परियोजना पर आधारित है और केवल मानक स्वयंसिद्धों Classical.choice, propext और Quot.sound का उपयोग करता है; इसमें native_decide का उपयोग नहीं है। TauCeti से लिया गया वर्गीकरण का औपचारिक कथन है: “हर परिमित सरल समूह, वर्गीकरण सूची में स्पष्ट रूप से निर्मित समूहों में से किसी एक के समरूप होता है।” README के अनुसार, `lake build` पूरे विकास-कार्य की जाँच करता है। इसमें Lake बिल्ड टूल में किए गए खुले बदलावों और उन अनुकूलनों की मदद से—जिन्हें टीम मुख्य परियोजना में शामिल करने की योजना बना रही है—बिल्ड का समय 24 घंटे से कम हो गया। कोड Apache-2.0 लाइसेंस के तहत उपलब्ध है।

24 दिनों में पूरा हुआ एजेंटों का सामूहिक प्रयास

1 अक्टूबर, 2026 को Axiom ने परियोजना के समन्वय के लिए Slack चैनल खोला। पहले से मौजूद Lean कार्य और प्रकाशित साहित्य के आधार पर तैयार किए गए आंतरिक प्रमाण-मानचित्र ने इस प्रयास को 108 पड़ावों और लगभग 380 छोटे कार्यों में बाँटा। एजेंटों का पहला समूह 2 अक्टूबर, 2026 को सक्रिय हुआ। एजेंटों ने GitHub इश्यू के ज़रिए पड़ाव अपने नाम किए और पूरा हुआ काम Slack में दर्ज किया। प्रमुख एजेंटों ने कठिन तर्कों को छोटे हिस्सों में बाँटा और कथनों की समीक्षा की, जबकि अन्य एजेंटों ने मौजूदा नतीजे खोजे या Lean प्रमाण लिखे। कोई एजेंट अधूरी पूर्वापेक्षाओं का काम दूसरे एजेंटों को सौंप सकता था; उनके नतीजे साझा रिपॉज़िटरी में जोड़े जाते थे।

शुरुआती प्रगति से कुछ कमज़ोरियाँ सामने आईं। कुछ ऐसे पड़ाव, जो देखने में आसानी से पूरे किए जा सकने वाले लगते थे, उनके पीछे बहुत बड़ी पूर्वापेक्षाएँ छिपी थीं। एजेंटों ने उन्हें सिद्ध करने के बजाय मान लिया था। टीम ने उन मान्यताओं पर आधारित दसियों हज़ार पंक्तियाँ हटा दीं और अधिक ठोस योजना के साथ फिर से काम शुरू किया। शुरुआती पड़ावों में से एक सिग्नलाइज़र फ़ंक्टर प्रमेय से जुड़ा था; उसके संभावित प्रमाण में संरचनात्मक मान्यताएँ थीं, जिन्हें अब भी उचित ठहराना बाकी था। एजेंटों के प्रमाण लिखने की गति Lean की दोबारा जाँच करने की गति से तेज़ होने पर बिल्ड का समय भी एक अड़चन बन गया। Axiom का कहना है कि उसके इंजीनियरों ने कैश किए गए बिल्ड नतीजों को विभिन्न वर्करों में बाँटा, स्वतंत्र जाँचें एक साथ चलाईं और समय लेने वाली परिमित गणनाओं को अलग-अलग जाँचे जा सकने वाले प्रमाणपत्रों में रखा। कंपनी के अनुसार, इन बदलावों से सत्यापन की गति कई गुना बढ़ गई।

कंपनी के मुताबिक, 10 अक्टूबर, 2026 को चैनल पर एक संदेश में बताया गया कि एजेंटों ने Monster के सरल होने का प्रमाण दे दिया है। एजेंटों ने Griess बीजगणित के माध्यम से Monster के अस्तित्व को भी औपचारिक रूप दिया और एक ऐसा प्रमेय सिद्ध किया जो Monster प्रकार के समूहों की पहचान Monster से करता है। 13 अक्टूबर, 2026 को केवल एक पड़ाव पूरा हुआ। इसके बाद इंजीनियरों ने नए सिरे से योजना बनाई और अधूरे पड़ावों को छोटे, सटीक रूप से व्यक्त प्रमेयों में बाँटा। हर विभाजन में यह दिखाना ज़रूरी था कि उन हिस्सों से एक छोटे Lean प्रमाण के माध्यम से मूल पड़ाव कैसे सिद्ध होगा।

प्रकाशित प्रमाण में मिली कमियाँ

Axiom के अनुसार, प्रमाण को Lean में रूपांतरित करने पर प्रकाशित तर्कों में कुछ समस्याएँ सामने आईं। इनमें से ज़्यादातर मामूली थीं—जैसे टाइप संबंधी त्रुटियाँ, तालिकाओं की गलतियाँ या छूटी हुई परिकल्पनाएँ—लेकिन कंपनी के मुताबिक, प्रकाशित विवरण से 34 उल्लेखनीय विचलन मिले। इनमें सबसे बड़ा विचलन अनबैलेंस्ड ग्रुप प्रमेय (UGT) से जुड़ा था।

इसका एक उदाहरण Aschbacher और Smith के क्वासिथिन खंडों में मिला, जहाँ एक लेम्मा में दावा किया गया था कि दो संख्यात्मक राशियाँ बराबर हैं। एजेंटों को समूह SL₂(5) से जुड़ा एक प्रतिउदाहरण मिला, जिसमें एक राशि 1 थी, जबकि कथित समानता के अनुसार उसका मान 2 होना चाहिए था। समानता की जगह असमानता रखने से लेम्मा ठीक हो गया, लेकिन बाद के तर्कों में कुछ मामलों को खारिज करने के लिए समानता का उपयोग किया गया था। इसलिए टीम ने उन विन्यासों को भी समेटने के लिए पहले के एक तर्क का दायरा बढ़ाया।

UGT, उपसमूहों के बारे में मिली जानकारी के आधार पर पूरे समूह की पहचान करने में मदद करता है: साथ दिए गए शोधपत्र के सार के अनुसार, वर्गीकरण की आगमनात्मक परिकल्पनाओं के तहत, किसी इनवोल्यूशन के सेंट्रलाइज़र में नॉर्मल कोई गैर-तुच्छ विषम-कोटि उपसमूह होने पर मूल सरल समूह का होना विषम अभिलक्षणिकता वाले Lie प्रकार या कुछ निश्चित कोटियों वाले वैकल्पिक समूहों में अनिवार्य हो जाता है। Axiom ने John Walter के 1986 के संस्मरण के ज़रिए UGT पर काम शुरू किया। उस तर्क को औपचारिक रूप देते समय, उसके एजेंटों को उसमें इस्तेमाल किए गए एक क्लोज़र कथन के स्पष्ट प्रतिउदाहरण मिले: जिस संक्रिया के बारे में माना गया था कि वह संबंधित सरल समूहों को एक निर्दिष्ट परिवार के भीतर रखेगी, वह ऐसा समूह उत्पन्न कर सकती थी जिसे उस परिवार से स्पष्ट रूप से बाहर रखा गया था।

कंपनी के विवरण के अनुसार, PSL₂(49) से शुरू करने पर—जिसके क्षेत्र इनवोल्यूशन का सेंट्रलाइज़र PGL₂(7) है—इस संक्रिया से सरल घटक PSL₂(7) मिलता है। इसे उस परिवार से बाहर रखा गया है, क्योंकि 7 एक मर्सेन अभाज्य संख्या है। Axiom का कहना है कि इन प्रतिउदाहरणों ने न तो UGT को गलत साबित किया, न ही Walter के प्रस्ताव II.5.9(ii) के निष्कर्ष को।

इस सुधार में Solomon के 1976 के मैक्सिमल 2-कंपोनेंट सिद्धांत का सहारा लिया गया। Axiom के अनुसार, इसी सिद्धांत ने उसके AxiomProver सिस्टम द्वारा तैयार और औपचारिक रूप दिए गए वैकल्पिक तर्क के मुख्य विचार उपलब्ध कराए। शोधपत्र में प्रमेय 2.3 (सरल टॉप्स का परिरक्षण) के रूप में बताया गया निर्णायक चरण, Axiom के मुताबिक, समूह सिद्धांत का एक नया परिणाम है, जिसे AxiomProver ने सिद्ध किया। Gilman और Solomon के अपचयन तथा Foote और Harris के पहचान प्रमेयों के साथ मिलकर, यह वर्गीकरण के लिए आवश्यक UGT का सरल-समूह रूप देता है। औपचारिकीकरण के बाद, Axiom के गणितज्ञों ने पहली पीढ़ी की विधियों के भीतर एक छोटा निगमन खोजा, जिसे टिप्पणी 9.5 में दर्ज किया गया है। यह प्रमेय 2.3 के बिना उसी निष्कर्ष तक पहुँचता है।

Colin Defant और Ken Ono के योगदान वाला वह शोधपत्र, The Unbalanced Group Theorem, 27 अक्टूबर 2026 को Hexagon प्रीप्रिंट सर्वर पर संस्करण 1 के रूप में CC BY 4.0 लाइसेंस के तहत प्रकाशित हुआ; परियोजना के पृष्ठ पर इसकी लंबाई 35 पृष्ठ बताई गई है। Axiom का कहना है कि वह साहित्य में मिली त्रुटियों की सूची तैयार करने के लिए समूह सिद्धांतकारों के साथ काम कर रहा है और उन्हें परियोजना के त्रुटि-सुधार पृष्ठ पर प्रकाशित करेगा। Lyons और Solomon से UGT के सुधार पर परामर्श लिया गया; वर्गीकरण की बुनियाद उनका काम है। कंपनी का कहना है कि वह बाहरी सलाहकार Dan Nakano के साथ-साथ Lyons और Solomon को शामिल करने वाले सलाहकार मंडल की मदद से इन त्रुटियों का संकलन और समाधान करती रहेगी। Axiom अपने योगदान को इस रूप में प्रस्तुत करता है कि उसने प्रमाण को मशीन से जाँचे जाने योग्य बनाया, सामने आई बाधाओं का दस्तावेज़ीकरण किया और उन्हें दूर करने वाले औपचारिक तर्क दिए। साथ ही, उसका कहना है कि समूहों की खोज करने और तर्क विकसित करने वाले गणितज्ञों की उपलब्धि ही इस वर्गीकरण का श्रेय है।