🔢 mathematics

A Milestone in Formalization: The Sphere Packing Problem in Dimension 8

यह शोध पत्र लीन थ्योरम प्रूवर (Lean Theorem Prover) का उपयोग करके मैरिना वियाज़ोस्का के 2016 के 8-आयामी गोला पैकिंग (sphere packing) समस्या के समाधान के सफल औपचारिक सत्यापन पर चर्चा करता है, जो मानव गणितज्ञों और ऑटोफॉर्मलाइजेशन मॉडल "गॉस" (Gauss) के बीच एक सहयोगात्मक मील के पत्थर को रेखांकित करता है।

मूल लेखक: Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, Maryna Viazovska

प्रकाशित 2026-04-28

📖 4 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, Maryna Viazovska

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

महान गणितीय पहेली: एक आदर्श सूटकेस को पैक करना

कल्पना कीजिए कि आप एक सूटकेस में अधिक से अधिक संतरे भरने की कोशिश कर रहे हैं। यदि आप उन्हें बस यूँ ही अंदर डाल देंगे, तो उनके बीच में हवा के बड़े अंतराल रह जाएंगे। लेकिन यदि आप उन्हें एक बहुत ही विशिष्ट, लयबद्ध पैटर्न में व्यवस्थित करते हैं, तो आप और अधिक संतरे समाहित कर सकते हैं।

सदियों से, गणितज्ञ इस बात को लेकर जुनूनी रहे हैं: गोलों (जैसे संतरे या कंचे) को एक स्थान में भरने का सबसे अच्छा तरीका क्या है ताकि कोई भी जगह बर्बाद न हो?

हमारी सामान्य 3D दुनिया में, हमारे पास उत्तर का एक अच्छा विचार है। लेकिन उच्च आयामों में—गणितीय "दुनियाओं" में जिन्हें हम देख नहीं सकते लेकिन गणना कर सकते हैं—पैटर्न अविश्वसनीय रूप से जटिल हो जाते हैं। 2016 में, मैरीना वियाज़ोस्का नामक एक गणितज्ञ ने 8वें आयाम के लिए इस पहेली को हल किया। उन्होंने एक "जादुई" पैटर्न (जिसे $E_8$ लैटिस कहा जाता है) खोजा जो इतना सटीक है कि यह एक ऐसे ब्रह्मांड में ब्लॉकों को स्टैक करने के एक आदर्श तरीके को खोजने जैसा है जिसे हम छू भी नहीं सकते।

समस्या: "मानवीय त्रुटि" का कारक

भले ही वियाज़ोस्का का गणित शानदार था, लेकिन गणित कठिन है। सबसे बुद्धिमान इंसान भी सैकड़ों पन्नों की लंबी गणना में एक छोटी सी "टाइपो" (लिखने की गलती) कर सकते हैं। यह सुनिश्चित करने के लिए कि उत्तर 100% सही है, गणितज्ञ फॉर्मल वेरिफिकेशन (औपचारिक सत्यापन) का उपयोग करते हैं।

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

सफलता: मानव-AI की टीम वर्क

यह शोध पत्र फरवरी 2026 में हासिल किए गए एक बड़े मील के पत्थर का वर्णन करता है। टीम ने केवल कोड लिखने के लिए मनुष्यों का उपयोग नहीं किया; उन्होंने "गॉस" (Gauss) नामक एक विशेष AI मॉडल का उपयोग किया।

इस सहयोग को एक विशाल कैथेड्रल बनाने की तरह समझें:

मनुष्य (वास्तुकार): उन्होंने ब्लूप्रिंट तैयार किया। उन्होंने तय किया कि किन "पत्थरों" (गणितीय परिभाषाओं) का उपयोग करना है और कहाँ "मेहराब" (मुख्य प्रमेय) होने चाहिए। उन्होंने सबसे जटिल और रचनात्मक कार्यों का भारी काम किया।
AI, गॉस (मास्टर मेसन/कुशल राजमिस्त्री): एक बार जब ब्लूप्रिंट तैयार हो गया, तो गॉस ने काम शुरू किया। यह अविश्वसनीय रूप से तेज़ था, जिसने केवल पांच दिनों में हजारों "ईंटें" (कोड की लाइनें) बिछा दीं। इसने उन विशाल, उबाऊ अंतरालों को भर दिया जिन्हें टाइप करने में मनुष्यों को महीनों लग जाते।

AI की "अव्यवस्थित" वास्तविकता

शोध पत्र यह भी स्वीकार करता है कि AI के साथ काम करना एक बहुत ही तेज़, लेकिन बहुत ही शाब्दिक (literal) इंटर्न को काम पर रखने जैसा है।

गॉस काम पूरा करने में अद्भुत था, लेकिन यह "सुंदर" या "परिष्कृत" नहीं था। जहाँ एक मानव गणितज्ञ एक ऐसा प्रमाण लिखने की कोशिश करता है जो सुंदर और संक्षिप्त हो (जैसे एक अच्छी तरह से लिखी गई कविता), वहीं गॉस ने एक ऐसा प्रमाण लिखा जो विशाल और दोहराव वाला था (जैसे एक विशाल निर्देश पुस्तिका जो हर पांच सेकंड में "बाएं मुड़ें" दोहराती है)।

टीम को वापस जाकर AI के काम को "साफ" करना पड़ा—अनावश्यक भाग को हटाना और कोड को भविष्य के गणितज्ञों के लिए पुन: उपयोग योग्य बनाना।

यह क्यों मायने रखता है?

आप पूछ सकते हैं, "8वें आयाम में संतरे भरने से किसे फर्क पड़ता है?"

यद्यपि यह समस्या स्वयं सैद्धांतिक है, लेकिन जो उपकरण बनाए जा रहे हैं वे क्रांतिकारी हैं। AI को मनुष्यों के साथ मिलकर अस्तित्व की सबसे कठिन समस्याओं को हल करने के लिए सिखाकर, हम एक ऐसा भविष्य बना रहे हैं जहाँ:

गणितीय सत्य पूर्ण (Absolute) है: हम "हमें लगता है कि यह सच है" से "हमारे पास डिजिटल प्रमाण है कि यह सच है" की ओर बढ़ सकते हैं।
AI केवल एक उपकरण नहीं, बल्कि एक साथी बन जाता है: हम यह सीख रहे हैं कि AI को उच्च-स्तरीय तर्क करने के लिए कैसे निर्देशित किया जाए, न कि केवल टेक्स्ट का सारांश बनाने या चित्र बनाने के लिए।

संक्षेप में: हमने सफलतापूर्वक एक "डिजिटल जज" और एक "AI मेसन" का उपयोग करके यह सिद्ध किया है कि 8वें आयाम में सबसे सुंदर पैटर्न वास्तव में पूर्ण है।

तकनीकी सारांश: औपचारिकीकरण में एक मील का पत्थर: आयामी 8 में गोला पैकिंग (Sphere Packing) की समस्या

1. समस्या: $\mathbb{R}^8$ में गोला पैकिंग (Sphere Packing)

गोला पैकिंग की समस्या यह पूछती है कि यूक्लिडियन स्पेस $\mathbb{R}^n$ में गैर-अतिव्यापी (non-overlapping) $n$ -आयामी गोलों की सबसे सघन संभव व्यवस्था क्या है। जबकि $n=1, 2,$ और $3$ के लिए समाधान सुस्थापित हैं, आयामी 8 में यह समस्या एक बड़ी चुनौती बनी रही जब तक कि 2016 में, मरिना वियाज़ोस्का (Maryna Viazovska) ने यह सिद्ध नहीं किया कि $E_8$ लैटिस (lattice) इष्टतम पैकिंग प्रदान करता है।

वियाज़ोस्का के प्रमाण ने कोहन-एल्कीज़ लीनियर प्रोग्रामिंग बाउंड (Cohn-Elkies linear programming bound) का उपयोग किया, जो कहता है कि यदि एक विशिष्ट प्रकार का "जादुई" श्वार्ट्ज़ फलन (Schwartz function) $f$ मौजूद है (जो कुछ धनात्मकता और फूरियर ट्रांसफॉर्म की शर्तों को पूरा करता है), तो यह गोला पैकिंग स्थिरांक $\Delta_d$ पर एक ऊपरी सीमा (upper bound) प्रदान कर सकता है। वियाज़ोस्का ने क्वासिमोड्यूलर फॉर्म्स (quasimodular forms) का उपयोग करके इस फलन का निर्माण किया।

2. कार्यप्रणाली: लीन (Lean) और ऑटोफॉर्मलाइजेशन (Autoformalization) के माध्यम से औपचारिकीकरण

इस परियोजना का प्राथमिक उद्देश्य वियाज़ोस्का के अनौपचारिक गणितीय प्रमाण को लीन थ्योरम प्रूवर (Lean Theorem Prover) का उपयोग करके एक औपचारिक रूप से सत्यापित, मशीन-चेक किए गए प्रमाण में परिवर्तित करना था। इसमें एक हाइब्रिड दृष्टिकोण अपनाया गया:

मानव-नेतृत्व वाला बुनियादी ढांचा (Human-Led Infrastructure): मानव औपचारिककारों (हरिहरण और वियाज़ोस्का के नेतृत्व में) ने प्रमाण के लिए आवश्यक आधारभूत गणितीय पुस्तकालयों का निर्माण किया। इसमें गोला पैकिंग की ज्यामिति, $E_8$ लैटिस के गुण, और मॉड्यूलर फॉर्म का सिद्धांत (आइजनस्टीन सीरीज़, जैकोबी थीटा फंक्शन्स, आदि) को परिभाषित करना शामिल था।
ऑटोफॉर्मलाइजेशन (The 'Gauss' Model): मानव-लिखित परिभाषाओं और पूर्ण प्रमाण के बीच के अंतर को पाटने के लिए, परियोजना में 'गॉस' (Gauss) का उपयोग किया गया, जो Math, Inc. द्वारा विकसित एक ऑटोफॉर्मलाइजेशन मॉडल है। गॉस को मानव-प्रदान किए गए ब्लूप्रिंट और लीन परिभाषाओं के आधार पर प्रमाण का मुख्य भाग उत्पन्न करने का कार्य सौंपा गया था।
मेटाप्रोग्रामिंग (Metaprogramming): जटिल संख्या अंकगणित और सीमा प्रमाणों (limit proofs) की भारी कम्प्यूटेशनल आवश्यकताओं को संभालने के लिए, टीम ने कस्टम लीन टैक्टिक्स विकसित किए, जैसे कि norm_numI (कॉम्प्लेक्स नंबर नॉर्मलाइजेशन के लिए) और tendsto_cont (निरंतरता के माध्यम से सीमा प्रमाणों को सरल बनाने के लिए)।

3. प्रमुख तकनीकी योगदान

'जादुदुई' फलन का निर्माण: टीम ने रेडियल श्वार्ट्ज़ फूरियर $\pm 1$ -आइजनफंक्शन्स के एक रैखिक संयोजन के रूप में फलन $g(x)$ के निर्माण को सफलतापूर्वक औपचारिक रूप दिया। चूंकि लीन के mathlib में उन्नत कंटूर इंटीग्रेशन मशीनरी का अभाव था, इसलिए टीम को विशिष्ट आयताकार कंटूर (rectangular contours) को परिभाषित करना पड़ा ताकि अनबाउंडेड पाथ के विरूपण (deformation) की अनुमति मिल सके, जिससे फलन के आइजनफंक्शिन गुणों के प्रमाण को सक्षम बनाया जा सके।
मॉड्यूलर फॉर्म सिद्धांत: परियोजना ने वेट 2 आइजनस्टीन सीरीज़ ( $E_2$ ), डिस्क्रीमिनेंट फॉर्म ( $\Delta$ ), और रामानुजन की पहचान (identities) से संबंधित आवश्यक पहचानों को औपचारिक रूप दिया। यह कोहन-एल्कीज़ की शर्तों को संतुष्ट करने के लिए आवश्यक असमानताओं को सिद्ध करने के लिए महत्वपूर्ण था।
कंटूर डिफॉर्मेशन प्रमाण: एक महत्वपूर्ण बाधा यह सिद्ध करना था कि कुछ कंटूरों को तब भी विकृत किया जा सकता है जब वे वास्तविक रेखा (real line) को छूते हैं (जहाँ इंटीग्रेंड्स अपरिभाषित हो सकते हैं)। गॉस ने इन विशिष्ट कंटूर-विरूपण पहचानों के लिए प्रमाणों में योगदान दिया।
एल्गोरिदम में सुधार: विशेष मेटाप्रोग्रामिंग टूल के विकास ने जटिल गणितीय अभिव्यक्तियों के स्वचालित सरलीकरण की अनुमति दी, जो अन्यथा मैन्युअल औपचारिकीकरण के लिए बहुत कठिन होतीं।

4. परिणाम

औपचारिक सत्यापन: फरवरी 2026 में, परियोजना ने $\mathbb{R}^8$ में इष्टतम गोला पैकिंग $E_8$ लैटिस है, इसका एक पूर्ण, "सॉरी-मुक्त" (sorry-free) औपचारिक सत्यापन (जिसका अर्थ है कि प्रत्येक चरण को बिना किसी sorry प्लेसहोल्डर के लीन कर्नेल द्वारा सत्यापित किया गया है) प्राप्त करने का मील का पत्थर हासिल किया।
कोडबेस विस्तार: परियोजना ने अपने कोडबेस को लगभग 20,000 लाइनों से बढ़ाकर अंतिम, रिफैक्टर्ड संस्करण में लगभग 60,000 लाइनों के लीन कोड तक विस्तारित किया।
AI प्रदर्शन: 'गॉस' मॉडल ने कुछ ही दिनों में जटिल, सैकड़ों लाइनों वाले प्रमाण उत्पन्न करने की क्षमता प्रदर्शित की, हालांकि इसने महत्वपूर्ण "कोड ब्लोट" (सहायक परिभाषाएं) भी उत्पन्न किया जिसके लिए लाइब्रेरी मानकों को पूरा करने के लिए मानव रिफैक्टरिंग की आवश्यकता पड़ी।

5. महत्व

यह शोध पत्र शुद्ध गणित और आर्टिफिशियल इंटेलिजेंस के संगम पर एक ऐतिहासिक उपलब्धि का प्रतीक है।

गणितीय कठोरता: यह विविक्त ज्यामिति (discrete geometry) के सबसे महत्वपूर्ण परिणामों में से एक का स्थायी, मशीन-चेक किया गया रिकॉर्ड प्रदान करता है, जो इसकी पूर्ण शुद्धता सुनिश्चित करता है।
गणित में AI: यह दर्शाता है कि ऑटोफॉर्मलाइजेशन मॉडल उच्च-स्तरीय, "फ्रंटियर" गणित को संभाल सकते हैं, जो साधारण प्रमाणों से आगे बढ़कर जटिल, बहु-चरणीय सैद्धांतिक तर्कों तक पहुँच सकते हैं।
औपचारिकीकरण का भविष्य: यह परियोजना एक नए वर्कफ़्लो को उजागर करती है: मनुष्य "ब्लूप्रिंट" और उच्च-स्तरीय बुनियादी ढांचे को डिजाइन करते हैं, जबकि AI सूक्ष्म प्रमाण चरणों को उत्पन्न करने के लिए "भारी काम" (heavy lifting) संभालता है। यह सहयोग सुझाव देता है कि भविष्य में औपचारिक सत्यापन की गति, गणितीय खोज की गति के साथ तालमेल बिठा सकेगी।