गणितज्ञों ने स्फीयर-पैकिंग समस्या के समाधान को पूरी तरह से सत्यापित करने के प्रयास में एक मील का पत्थर घोषित किया है – जिसके लिए यूक्रेनी गणितज्ञ मैरीना वियाज़ोव्स्का 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