एक प्रमाण जिसे कंप्यूटर जाँच सकता है
एंथ्रोपिक ने 4 सितंबर को बताया कि उसके एक आंतरिक शोध मॉडल ने फ़र्मा के अंतिम प्रमेय का पहला ऐसा प्रमाण तैयार किया है जिसे कंप्यूटर आरंभ से अंत तक जाँच सकता है। यह औपचारिकीकरण लीन की लगभग एक करोड़ तीस लाख पंक्तियों में है। लीन वह प्रूफ़ असिस्टेंट है जिससे गणितज्ञ किसी तर्क के हर चरण को ऐसी शक्ल में लाते हैं जिसे मशीन सत्यापित कर सके। कंपनी के अनुसार यह काम ग्यारह दिनों में हुआ।
फ़र्मा का अंतिम प्रमेय कहता है कि दो से बड़े किसी भी पूर्णांक n के लिए कोई तीन धनात्मक पूर्णांक a^n + b^n = c^n को संतुष्ट नहीं करते। एंड्रयू वाइल्स ने इसे 1995 में लगभग 129 पृष्ठों के शोधपत्र में सिद्ध किया, जो बीसवीं सदी भर में बनी गणितीय मशीनरी पर टिका था। ऐसे प्रमाण को हाथ से जाँचने में विशेषज्ञों को वर्षों लगते हैं। उसके औपचारिकीकरण में भी उतना ही समय लगने की उम्मीद थी।
मॉडल ने असल में क्या किया
एंथ्रोपिक के अनुसार यह कोई विशेष गणित इंजन नहीं, बल्कि सामान्य प्रयोजन का आंतरिक शोध मॉडल था, जो मोटे तौर पर क्लॉड फ़ेबल 5.1 के बराबर है। कंपनी का कहना है कि कई दर्जन एजेंट समानांतर चले, लगभग छह अरब टोकन तैयार किए और 30,300 प्रमेय सिद्ध किए, जिनमें से 29,500 अंतिम परिणाम में शामिल हैं। मानवीय हस्तक्षेप केवल उच्च स्तरीय दिशा तक सीमित रहा।
एंथ्रोपिक बताती है कि शुरुआती प्रयास पूरी तरह विफल रहे। जो प्रयास सफल हुआ, वह एक आंतरिक मंच पर टिका था जिसे कंपनी प्रूव2मी कहती है। यह मंच दर्ज रखता है कि कौन सा प्रमेय किस पर निर्भर है और कई एजेंटों को एक ही प्रमाण की अलग-अलग शाखाओं पर काम करने देता है। अंतिम फ़ाइल की लगभग सात प्रतिशत गैर-नियमित पंक्तियाँ विफल प्रयासों से आईं।
नीचे मौजूद मानवीय आधार
यह परिणाम शून्य से नहीं निकला। यह हेनरी डार्मन, फ़्रेड डायमंड और रिचर्ड टेलर द्वारा प्रस्तुत वाइल्स के तर्क के सरलीकृत रूप का अनुसरण करता है, और मैथलिब पर टिका है — वह सामुदायिक गणित पुस्तकालय जिसे हज़ारों योगदानकर्ता एक दशक से अधिक समय से लीन में बना रहे हैं — तथा इंपीरियल कॉलेज लंदन में केविन बज़ार्ड के औपचारिकीकरण प्रोजेक्ट पर। बज़ार्ड ने, जिन्होंने परिणाम की समीक्षा की, इसका महत्व भरोसेमंदी के रूप में बताया: उनके अनुसार ये कलाकृतियाँ अब इतनी मज़बूत हैं कि उन पर आगे निर्माण किया जा सके।
एंथ्रोपिक ने खुद सीमाएँ बताईं। प्रमाण केवल लीन के तीन मानक अभिगृहीतों पर टिका है, और एक तुलनित्र ने पुष्टि की कि सिद्ध किया गया कथन मैथलिब वाले सूत्रीकरण से मेल खाता है — यही जाँच किसी तंत्र को दावे से थोड़ा कमज़ोर बात सिद्ध करने से रोकती है। पर कंपनी यह भी कहती है कि प्रमाण संभवतः ज़रूरत से कहीं लंबा है, जो उसके हिस्सों का पुनः उपयोग करने वालों के लिए मायने रखता है।
औपचारिकीकरण ही दिलचस्प हिस्सा क्यों है
गणित में दशकों से सत्यापन की अड़चन रही है: अग्रिम मोर्चे के प्रमाण इतने लंबे होते हैं कि गिने-चुने लोग ही उन्हें परख सकते हैं, और कुछ त्रुटियाँ प्रकाशन के बाद भी बची रहीं। औपचारिकीकरण समीक्षक की समस्या हटा देता है, पर उसकी कीमत भारी उबाऊ श्रम है। इसी सौदे ने इसे दुर्लभ बनाए रखा।
अगर उबाऊ आधा हिस्सा इस पैमाने पर स्वचालित हो सके तो गणित बदल जाता है। यह ऐसे ही कई दावों की कड़ी में जुड़ता है: एंथ्रोपिक ने अगस्त में रीमान ज़ीटा फलन पर क्लॉड के नए परिणामों का काम प्रकाशित किया, और ओपनएआई का कहना है कि उसके एस्ट्रा मॉडल ने कई खुली एर्दश समस्याएँ हल कीं।
देखने लायक बात स्वतंत्र पुनः उपयोग है। एक करोड़ तीस लाख पंक्तियों की लीन फ़ाइल अपनी बनावट से ही सत्यापनीय है — लीन का मक़सद यही है — पर कार्यरत गणितज्ञों के लिए उसका मूल्य इस पर निर्भर करता है कि बीच के प्रमेय मैथलिब में लिए जाकर कहीं और काम आ सकें या नहीं। एंथ्रोपिक ने नहीं बताया कि पूरी कलाकृति कब, या क्या, इसके लिए जारी होगी।
