गणितज्ञों के एक समूह ने स्फीयर-पैकिंग समस्या के समाधान को पूरी तरह से सत्यापित करने के प्रयास में एक मील का पत्थर घोषित किया है – जिसके लिए यूक्रेनी गणितज्ञ मैरीना वियाज़ोव्स्का 2022 में एक मशीन का उपयोग करके फील्ड्स मेडल जीता।
समस्या का यह संस्करण पूछता है कि आठ आयामों में गोले के एक समूह को पैक करने का सबसे अच्छा तरीका क्या है।
23 फरवरी को, इसे हासिल करने वाली टीम ने कहा कि अब उसके पास इस बात का सबूत है कि एक मशीन ने पूरी तरह से सत्यापन कर लिया है।
वियाज़ोव्स्का का प्रमाणकठिन गणित समस्याओं के कई अन्य (मानवीय) प्रमाणों की तरह, मूल रूप से गणितज्ञों को समझने के लिए लिखा गया था। इसका मतलब यह है कि उसका पेपर उन चरणों को छोड़ देता है जिन्हें “स्पष्ट” माना जाता है या जो कुछ प्रमेय जागरूकता से अनुसरण करते हैं जिन्हें गणितज्ञ हल्के में ले सकते हैं।
दूसरी ओर, नई उपलब्धि में एक मशीन शामिल थी जो स्पष्ट और ‘छिपे हुए’ दोनों चरणों की जाँच कर रही थी।
जाँच के लाभ
गणितज्ञ यह प्रयास इसलिए कर रहे हैं क्योंकि कभी-कभी कोई तार्किक दोष या कोई अघोषित धारणा बिना ध्यान दिए निकल सकती है।
एक बार इस तरह से प्रमाण की जांच हो जाने के बाद, अन्य गणितज्ञ यह जान सकते हैं कि सभी बिंदुओं पर उपयोग किए गए प्रमाण की कौन सी परिभाषाएँ हैं, कहावत किस प्रमेय पर भरोसा करती है, आदि, जिससे उनके लिए इसे स्वयं ऑडिट करना या अपने काम में इसके कुछ हिस्सों का पुन: उपयोग करना आसान हो जाता है। अन्य मशीनें भी भविष्य में अन्य समस्याओं के अधिक जटिल प्रमाणों की पुष्टि करते समय इसका उपयोग कर सकती हैं।
यहां औपचारिकीकरण का अर्थ कागजों में लिखे एक गैर-विस्तृत मानव प्रमाण को मशीन की भाषा में अनुवाद करना है।
मैरीना वियाज़ोव्स्का | फोटो साभार: रॉयटर्स
यहां की भाषा लीन नामक सॉफ़्टवेयर के एक टुकड़े के लिए थी।
‘उल्लेखनीय योगदान’
यह विकास कैलिफोर्निया स्थित कंपनी मैथ, इंक. द्वारा विकसित ‘गॉस’ नामक ऑटो-औपचारिकीकरण एजेंट के उपयोग के लिए भी उल्लेखनीय है।
स्फीयर पैकिंग लीन प्रोजेक्ट, वियाज़ोव्स्का के प्रमाण को औपचारिक रूप देने के लिए एक ओपन-सोर्स प्रयास, पहले से ही कई लेम्मा और परिभाषाओं के साथ एक बड़ा लीन कोडबेस था और उन बयानों की एक सूची थी जिन्हें अभी भी साबित करने की आवश्यकता थी। ‘गॉस’, जो एक एआई उपकरण है, ने लीन को जाँचने के लिए शेष कथनों को औपचारिक रूप दिया।
“प्रोजेक्ट टीम पहले से ही गॉस कोड की समीक्षा और संशोधन करने की प्रक्रिया में है, जिससे यह सुनिश्चित हो सके कि यह औपचारिकीकरण समुदाय के संपादकीय मानकों को पूरा करता है। यह प्रक्रिया सुनिश्चित करेगी कि कोड रखरखाव योग्य और पुन: प्रयोज्य है, और यह भविष्य के औपचारिकीकरण कार्य का समर्थन करेगा,” कार्नेगी मेलन विश्वविद्यालय के पीएचडी छात्र सिद्धार्थ हरिहरन ने एक में लिखा है डाक लिंक्डइन पर. “गॉस के उल्लेखनीय योगदान ने परियोजना के महीनों के प्रयास को बचा लिया है, और गॉस संशोधनों में भूमिका निभाते रहेंगे।”
श्री हरिहरन इसके अनुरक्षक भी हैं स्फीयर पैकिंग लीन परियोजना.
लीन कैसे काम करता है
लीन एक तार्किक आधार वाली प्रोग्रामिंग भाषा है। गणितज्ञ पहले परिभाषाओं, प्रमेयों और प्रमाणों का अनुवाद लीन कोड के रूप में करते हैं, फिर इसका कर्नेल – जो चेकर है – सत्यापित करता है कि क्या वे सही हैं।
कर्नेल लीन के अंतर्निहित तार्किक नियमों का उपयोग करके प्रमाणों की जांच करता है, जबकि मैथलिब नामक एक अलग लाइब्रेरी अधिकांश मानक परिभाषाओं और प्रमेयों की आपूर्ति करती है जिन्हें गणितज्ञ पुन: उपयोग कर सकते हैं।
लीन का उपयोग करने के लिए, गणितज्ञ किसी समस्या को लीन स्टेटमेंट के रूप में एन्कोड करके शुरू करते हैं, जिसमें प्रमाण में शामिल वस्तुएं क्या हैं और वास्तव में क्या दावा किया जा रहा है। फिर वे लीन के अंदर प्रमाण के आवश्यक गणितीय ‘भागों’ को शामिल करते हैं, इस मामले में वास्तविक और जटिल विश्लेषण, फूरियर रूपांतरण, विशेष कार्य, मॉड्यूलर/थीटा-फ़ंक्शन, असमानताएं, माप सिद्धांत, आदि।
प्रत्येक कदम जो एक मानव कागज में छोड़ सकता है उसे लेम्मा की एक श्रृंखला में विस्तारित करने की आवश्यकता है जिसे लीन सत्यापित कर सकता है। फिर अंततः कर्नेल काम करने लगता है।
जनवरी में लीन टुगेदर सम्मेलन में, लीन निर्माता लियो डी मौरा ने कहा कि इस वर्ष की प्राथमिकताओं में लीन 4 कंपाइलर को अंतिम रूप देना और संकलन समय को कम करने और आधुनिक लीन पुस्तकालयों के बड़े पैमाने को संभालने के लिए इसके प्रदर्शन में सुधार करना शामिल है।
औपचारिकता की चुनौती
गणितज्ञों के अनुसार, अंतिम उद्देश्य गणितीय शुद्धता को विश्वास और सामाजिक प्रक्रियाओं पर कम और स्पष्ट और सत्यापन योग्य गणित पर अधिक निर्भर बनाना है।
उदाहरण के लिए, 1879 में, अंग्रेजी गणितज्ञ अल्फ्रेड केम्पे ने चार-रंग प्रमेय का प्रमाण प्रकाशित किया। यदि आप कागज की एक सपाट शीट पर एक नक्शा बनाते हैं, तो आप प्रत्येक क्षेत्र को रंग सकते हैं ताकि सीमा साझा करने वाले किन्हीं दो क्षेत्रों को केवल चार रंगों का उपयोग करके अलग-अलग रंग मिलें। और केम्पे ने कहा कि उन्होंने यह साबित कर दिया है।
केम्पे के साथियों ने उसके प्रमाण को लगभग एक दशक तक स्वीकार किया क्योंकि प्रमाण उचित लग रहा था और वह अत्यधिक प्रतिष्ठित था। लेकिन 1890 में गणितज्ञ पर्सी हेवुड ने एक गलती पाई जिसने इसे अमान्य कर दिया। बाद में प्रमेय सत्य निकला लेकिन केम्पे का प्रमाण अभी भी ग़लत था।
गणितज्ञों ने 20वीं सदी में यह भी पाया कि गणितीय ‘प्रमाण’ एक औपचारिक वस्तु है, जिसे सैद्धांतिक रूप से एक मशीन द्वारा जांचा जा सकता है, और लोग ऐसा करने के लिए व्यावहारिक उपकरण चाहते थे।
आधुनिक गणित में प्रमाण भी बहुत लंबे हो सकते हैं और सहकर्मी-समीक्षक हमेशा यह जांचने के कार्य में सक्षम नहीं हो सकते हैं कि वे शुरू से अंत तक सही हैं या नहीं। इस प्रकार प्रमाण सहायक सत्यापन के लिए बार को बढ़ाने और पूरा करने के एक तरीके के रूप में उभरे।
औपचारिकता में सहायता करना
किसी प्रमाण को मशीन की भाषा में लाने के लिए किसी मशीन की पूरी तरह से जांच करने में मुख्य बाधा – यानी औपचारिकता।
कुछ प्रमुख प्रमेय जिन्हें पूरी तरह से औपचारिक रूप दिया गया है उनमें 2005 में स्वयं चार-रंग प्रमेय शामिल हैं; अभाज्य संख्या प्रमेय भी 2005 में; 2012 में फीट-थॉम्पसन विषम क्रम; और 2014 में केप्लर अनुमान।
स्वचालन ने इस संबंध में मदद की है, हालांकि यह अभी भी उस बिंदु पर नहीं आया है जहां कोई उपकरण ‘मानव प्रमाण’ ले सकता है और इसे विश्वसनीय तरीके से पूर्ण औपचारिक प्रमाण में बदल सकता है।
सितंबर 2025 में, भारतीय विज्ञान संस्थान के गणित के प्रोफेसर सिद्धार्थ गाडगिल के नेतृत्व में एक टीम अनुदान जीता ‘लीनएड’ पर अपने काम के लिए एआई फॉर मैथ फंड से। उद्धरण में लिखा है, “एक सुलभ, नो-कोड एआई + लीन वातावरण बनाकर, परियोजना लीन उपयोगकर्ताओं के लिए औपचारिकता प्रक्रिया को सरल बनाने और गणितज्ञों को अनुसंधान के लिए नए, नवीन उपकरणों के साथ सशक्त बनाने का प्रयास करती है, जिसमें एजेंटिक समाधान भी शामिल हैं।”
गॉस जैसे कुछ अन्य उपकरणों में लीन कोपायलट, लीन के अंदर एक एआई सहायक शामिल है जो सुझाव देता है कि अगला कदम क्या प्रयास करना है; स्लेजहैमर, एक उपकरण जो अन्य प्रोग्रामों को कॉल करके आपके वर्तमान लक्ष्य को स्वचालित रूप से हल करने का प्रयास करता है; और अल्फा प्रूफ, एक एआई उपकरण है जो डीपमाइंड द्वारा सबूत तैयार करने के लिए विकसित किया गया है जिसे लीन जैसा प्रूफ सहायक जांच सकता है।
गणित में ए.आई
एआई गणित को नया आकार दे रहा है, जबकि यह केवल एक शक्तिशाली कैलकुलेटर से दूर विकसित हो रहा है। फोटोमैथ और स्पेशलाइज्ड एजुकेशनल इंटेलिजेंस या एसईआई मॉडल जैसे प्लेटफॉर्म आज ऑन-डिमांड ट्यूटर के रूप में काम करते हैं जो प्राकृतिक भाषा में चरण-दर-चरण स्पष्टीकरण प्रदान करते हैं और व्यक्तिगत छात्रों के लिए अनुकूल हो सकते हैं।
उच्च गुणवत्ता वाले मानकीकृत परीक्षण उत्पन्न करने के साथ-साथ अंतर्राष्ट्रीय गणितीय ओलंपियाड जैसी चुनौतियों का सामना करने के लिए बड़े भाषा मॉडल (एलएलएम) का उपयोग किया जा रहा है। 2025 में, OpenAI और Google DeepMind के रीज़निंग मॉडल ने स्वर्ण पदक के योग्य अंक हासिल किए।
एआई मॉडल अनुभवी गणितज्ञों के लिए एक तर्क भागीदार भी बन गए हैं, जो बड़े डेटासेट में पैटर्न का पता लगाकर समस्याओं को हल करने में मदद करते हैं। इसका उपयोग टोपोलॉजी और ज्यामिति में उपन्यास अनुमान उत्पन्न करने के लिए किया गया है, जो अक्सर विशेषज्ञों से बचने वाले अलग-अलग क्षेत्रों में कनेक्शन का पता लगाता है।
उदाहरण के लिए, 13 फरवरी को, OpenAI ने घोषणा की कि कंपनी द्वारा दो मॉडल बनाए गए हैं भौतिकविदों को नई खोज करने में मदद मिली कण भौतिकी में, समुदाय द्वारा कई वर्षों से चली आ रही धारणा को उलट दिया गया।
“[xAI cofounder] क्रिश्चियन सजेगेडी ने भविष्यवाणी की है कि छह महीने से एक साल में मॉडल गणितीय रूप से ‘लगभग सभी मामलों में अतिमानवीय’ हो जाएंगे,” टोरंटो विश्वविद्यालय के सहायक प्रोफेसर डैनियल लिट ने अपने लेख में लिखा है ब्लॉग 21 फरवरी को.
“मुझे लगता है कि गणितीय अनुसंधान के अधिकांश पहलुओं के लिए उस सटीक समयरेखा पर विश्वास करना कठिन है, लेकिन मुझे संदेह है कि जब इसमें शामिल बयानों के कुछ वर्ग को साबित करने की बात आती है, जिसके लिए पहले एक विशेषज्ञ की आवश्यकता होती है, तो वह ज्यादा पीछे नहीं हटेंगे। यह वास्तव में गणित की एक संकीर्ण अवधारणा है, लेकिन यह सच है कि ऐसे प्रमाण तैयार करना गणित अनुसंधान का एक बड़ा हिस्सा है।”
mukunth.v@thehindu.co.in
