क्लॉड ने 11 दिनों में फर्मा का अंतिम प्रमेय Lean में कैसे औपचारिक रूप से लिखा

Anthropic का कहना है कि Claude ने फर्मा के अंतिम प्रमेय (Fermat’s Last Theorem या FLT) का पहला पूर्ण, आरंभ-से-अंत तक कंप्यूटर-जांच योग्य Lean औपचारिकीकरण तैयार किया। अहम फर्क यह है कि Claude ने FLT का नया प्रमाण खोजा नहीं। उसने पहले से स्थापित आधुनिक प्रमाण-पथ को ऐसे विशाल औपचारिक रूप में बदला जिसे Lean यांत्रिक ढंग से जांच सकता है। कंपनी के अनुसार, यह काम मुख्यतः स्वायत्त एजेंटों ने 11 दिनों में किया और इससे लगभग 1.3 करोड़ पंक्तियों का Lean कोड बना। 215

आखिर औपचारिक रूप किसका दिया गया?

FLT कहता है कि प्राकृतिक संख्याओं के लिए, यदि घात 3 या उससे अधिक हो, तो समीकरण (a^n+b^n=c^n) का कोई गैर-तुच्छ हल नहीं है। Lean की Mathlib लाइब्रेरी में इसका रूप यह है कि किसी भी हल में (a=0), (b=0) या (c=0) होना चाहिए। यह परिचित कथन—धनात्मक पूर्णांकों में कोई हल नहीं—के बराबर है। 31

परियोजना ने Wiles/Taylor–Wiles रणनीति की Darmon–Diamond–Taylor प्रस्तुति अपनाई; गणित के लिए कोई नया रास्ता नहीं बनाया गया। यह चुनाव महत्वपूर्ण है, क्योंकि औपचारिकीकरण में सिर्फ मुख्य तर्क नहीं लिखा जाता। परिभाषाएं, शर्तें, सहायक परिणाम और वे छोटे तार्किक जोड़ भी स्पष्ट करने पड़ते हैं जिन्हें सामान्य गणितीय शोध-पत्र अक्सर निहित मान लेते हैं। Imperial College की FLT परियोजना भी अपने मार्ग को Wiles/Taylor–Wiles प्रमाण का आधुनिक रूप बताती है। 511

1.3 करोड़ पंक्तियां क्यों लगीं?

औपचारिक प्रमाण-सहायक में “मानक तर्क से यह निष्कर्ष निकलता है” लिख देना पर्याप्त नहीं होता। हर अनुमान को ऐसे रूप में व्यक्त करना पड़ता है जिसे सिस्टम टाइप-चेक कर सके, और हर नतीजे के पीछे उसके औपचारिक रूप से दर्ज आधार होने चाहिए।

Anthropic के अनुसार, परियोजना में करीब 30,300 कंप्यूटर-सत्यापित प्रमेय बने, जिनमें लगभग 29,500 अंतिम निर्भरता-श्रृंखला में शामिल हैं। अंतिम विकास में बीजगणित, ज्यामिति, हार्मोनिक विश्लेषण और संख्या सिद्धांत जैसे क्षेत्र आते हैं। 215

इस पैमाने को देखते हुए 11 दिनों को FLT के बौद्धिक इतिहास का 11-दिन का विकल्प नहीं समझना चाहिए। Anthropic लगभग 6 अरब जनरेट किए गए टोकन का भी उल्लेख करता है। इस प्रक्रिया में अनेक संभावित प्रमाण, Lean द्वारा जांच, त्रुटियों के आधार पर सुधार और लंबे औपचारिकीकरण को व्यवस्थित रखने की इंजीनियरिंग शामिल थी। 5

असली तकनीक: कई एजेंटों के लिए बाहरी समन्वय

रिपोर्ट के अनुसार सफलता केवल किसी एक मॉडल द्वारा पूरे प्रमाण को अपने संदर्भ में याद रखने से नहीं आई। Anthropic कहता है कि शुरुआती प्रयासों में प्रगति हुई, लेकिन साझा परियोजना-स्थिति बनाए रखना कठिन था। सफल रन में Prove2Me पर आधारित एक हार्नेस इस्तेमाल हुआ, जो सहयोगी गणितीय औपचारिकीकरण के लिए बनाया गया मंच है। 529

इसका केंद्रीय विचार एक निर्देशित निर्भरता-ग्राफ है:

• ग्राफ के नोड अधूरी परिभाषाओं, लेम्माओं या प्रमेयों को दर्शाते हैं।
• किनारे बताते हैं कि कौन-सा परिणाम आगे के किस परिणाम के लिए जरूरी है।
• एजेंट खुले और उपयोगी कार्य चुन सकते हैं, उन्हें Lean में सिद्ध कर सकते हैं और तैयार नतीजे दूसरे एजेंटों के लिए उपलब्ध करा सकते हैं।
• इस तरह प्रणाली बुनियादी घटकों से शुरू करके अंतिम प्रमेय की ओर बढ़ सकती है।

Prove2Me इसे औपचारिकीकरण “मिशन” चलाने का मॉडल बताता है, जिनमें एजेंट दोबारा इस्तेमाल किए जा सकने वाले औपचारिक प्रमाण जोड़ते हैं। 29 व्यावहारिक रूप से, यह एक लंबे और नाजुक काम को कई जांच योग्य उपसमस्याओं में बांटता है और किसी एक मॉडल रन से बाहर टिकाऊ परियोजना-स्मृति तैयार करता है।

“कंप्यूटर-जांच योग्य” होने का मतलब क्या है?

Anthropic के मुताबिक अंतिम परियोजना में sorry प्लेसहोल्डर नहीं हैं—Lean में यह किसी कथन को सिद्ध किए बिना स्वीकार कर लेने का तरीका है—और प्रमाण केवल Lean के तीन मानक स्वयंसिद्धों पर निर्भर है। 5

यह प्राकृतिक भाषा में AI द्वारा विश्वसनीय दिखने वाला प्रमाण लिख देने से काफी अलग है। Lean का कर्नेल जांचता है कि कूटबद्ध हर कदम उसके तार्किक नियमों, स्वयंसिद्धों और आयातित निर्भरताओं के अंतर्गत निकलता है या नहीं। Anthropic का यह भी कहना है कि अंतिम दावा Mathlib में स्थापित FermatLastTheorem वाले रूप से मेल खाता है। 531

फिर भी कर्नेल-जांच की एक स्पष्ट सीमा है: वह उसी औपचारिक कथन को सत्यापित करती है जो कोड में व्यक्त किया गया है। औपचारिक परिभाषाएं और बीच के कथन इच्छित अनौपचारिक गणित को सही ढंग से दर्शाते हैं या नहीं, यह मनुष्यों को देखना होगा। इसलिए जारी किए गए आर्टिफैक्ट को स्वतंत्र रूप से कंपाइल करना और विशेषज्ञों द्वारा उसकी निर्भरता-श्रृंखला की समीक्षा इस दावे की महत्वपूर्ण कसौटियां होंगी।

केविन बज़र्ड ने इसे असाधारण क्यों कहा?

Anthropic की रिपोर्ट के अनुसार, गणितज्ञ केविन बज़र्ड ने इसे “असाधारण ऑटोफॉर्मलाइज़ेशन उपलब्धि” कहा। 21 महत्व सिर्फ इतना नहीं है कि एजेंट अलग-अलग Lean अभ्यास हल कर सकते हैं। बड़ा दावा यह है कि उन्होंने परत-दर-परत जुड़ा, दोबारा इस्तेमाल योग्य औपचारिक विकास उस पैमाने पर बनाया, जिसके लिए पहले वर्षों के समन्वित मानवीय श्रम की अपेक्षा की जाती थी।

यदि ऐसा काम दोहराने योग्य और सस्ता बनता है, तो गणित को कुछ संभावित लाभ मिल सकते हैं:

• अधिक कठोर सत्यापन: औपचारिक प्रणालियां छूटी हुई शर्तों, गलत रूपांतरणों और परिभाषाओं के बेमेल को पकड़ सकती हैं।
• पुन: प्रयोज्य आधारभूत ढांचा: एक बार किसी लेम्मा का औपचारिक रूप बन जाए, तो अगली परियोजनाएं उसे आयात कर सकती हैं और कर्नेल-जांच पर भरोसा कर सकती हैं।
• पीयर रिव्यू का पूरक: मशीन-जांच योग्य प्रमाण लंबे तकनीकी तर्कों के सत्यापन का बोझ घटा सकते हैं, जबकि अर्थ, प्रासंगिकता और रणनीति का मूल्यांकन गणितज्ञों के पास रहेगा।

ये संभावित फायदे हैं, गणितीय निर्णय का स्वचालित विकल्प नहीं। कोई औपचारिक प्रमाण तार्किक रूप से वैध हो सकता है, फिर भी वह गलत या अनपेक्षित कथन को औपचारिक रूप दे रहा हो; और 1.3 करोड़ पंक्तियों का आर्टिफैक्ट तैयार करने की लागत भी बहुत बड़ी है।

इस दावे को कैसे समझें?

रिपोर्ट किया गया FLT परिणाम AI-सहायित औपचारिकीकरण के लिए महत्वपूर्ण बेंचमार्क है, क्योंकि लक्ष्य प्रमेय पहले ही स्थापित था और अंतिम आर्टिफैक्ट को स्वतंत्र रूप से जांचने के लिए जारी करने का इरादा है। इसे Claude द्वारा फर्मा का अंतिम प्रमेय नए सिरे से हल कर देने के रूप में पेश करना गलत होगा।

ज्यादा सटीक और अधिक महत्वपूर्ण व्याख्या यह है: Anthropic के अनुसार, एजेंटों की समन्वित प्रणाली ने एक बड़े, ज्ञात प्रमाण को Lean विकास में बदला, जिसमें ग्राफ-आधारित कार्य-विभाजन और औपचारिक सत्यापन को लगातार फीडबैक की तरह इस्तेमाल किया गया। 21529

अब असली सवाल व्यावहारिक हैं: क्या बाहरी शोधकर्ता इस बिल्ड को दोहरा सकते हैं, क्या वे औपचारिकीकरण के गणितीय अर्थ का ऑडिट कर सकते हैं, इसके हिस्सों को आगे के काम में इस्तेमाल कर सकते हैं और दूसरी उन्नत गणितीय समस्याओं पर ऐसे ही नतीजे पा सकते हैं? इन्हीं कसौटियों से पता चलेगा कि यह एक बार का इंजीनियरिंग कारनामा है या आधुनिक प्रमाणों के निर्माण और जांच में टिकाऊ बदलाव।