Claude ने फ़र्मेट प्रमेय 11 दिनों में पूरा किया: Lean की 13.4 मिलियन लाइनें और एक भी "स्पष्ट रूप से" नहीं

4 सितंबर को, एंथ्रोपिक ने फ़र्मेट के अंतिम प्रमेय का पहला पूर्ण मशीन परीक्षण दिखाया। Claude 11 दिनों में, लगभग लोगों की मदद के बिना, एंड्रयू विल्स के प्रमाण का भाषा में अनुवाद किया Lean: कोड की 13.4 मिलियन पंक्तियाँ, लगभग 30 हजार मध्यवर्ती प्रमेय, शून्य "जो कहा गया है उससे स्पष्ट।" यह परियोजना, जिसकी गणितज्ञ वर्षों से योजना बना रहे थे - इंपीरियल कॉलेज लंदन के केविन बज़र्ड द्वारा केवल पहले चरण की ड्राइंग 86 पृष्ठ लंबी थी - डेढ़ सप्ताह में पूरी हो गई।

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

कंप्यूटर ने वास्तव में क्या जाँच की?

यहाँ विशेषणों की अपेक्षा अंक अधिक उपयुक्त हैं।

• Lean की 13.4 मिलियन पंक्तियाँ संपूर्ण मैथलिब, सिस्टम की मुख्य औपचारिक गणित लाइब्रेरी से पाँच गुना अधिक बड़ी हैं।
• लगभग 30 हजार मध्यवर्ती प्रमेय सिद्ध किये जा चुके हैं; अंतिम आउटपुट में लगभग 29,500 शामिल थे।
• 96-कोर मशीन पर रिपॉजिटरी को संकलित करने में मैथलिब को संकलित करने की तुलना में लगभग 20 गुना अधिक समय लगता है। परीक्षण की अवधि के लिए बज़ार्ड को 500 जीबी रैम वाला एक सर्वर दिया गया था।
• निर्भरता केवल तीन मानक सिद्धांतों Lean पर है। कोई "सरलता के लिए धारणाएँ" नहीं।

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

हाशिये पर एक पंक्ति, साढ़े तीन सदी का काम

1637 के आसपास, पियरे डी फ़र्मेट ने डायोफैंटस के अंकगणित के हाशिये में दिए गए कथन को जिम्मेदार ठहराया: दो से अधिक n के लिए, समीकरण aⁿ + bⁿ = cⁿ का प्राकृतिक संख्याओं में कोई समाधान नहीं है। नीचे एक वाक्यांश है जो एक किंवदंती बन गया है: "मुझे वास्तव में एक अद्भुत प्रमाण मिला है, लेकिन इसके लिए मार्जिन बहुत संकीर्ण है।" यूलर से कुमेर तक गणितज्ञों की पीढ़ियाँ टुकड़ों में परिणाम की ओर बढ़ीं। 1908 में, प्रमाण के लिए 100 हजार स्वर्ण अंकों का पुरस्कार दिया गया, और पहले वर्ष में 621 गलत समाधान प्राप्त हुए।

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

कोई नया प्रमाण नहीं, बल्कि एक नया अवसर

यह डार्मोन, डायमंड और टेलर के 1995 में लैंगलैंड्स-टनेल प्रमेय और रिबेट स्तर वंश के माध्यम से विल्स-टेलर तर्क के विश्लेषण पर आधारित है। विल्स को औपचारिक बनाने का विचार 2000 के दशक में डच कंप्यूटर वैज्ञानिक जान बर्गस्ट्रा द्वारा उठाया गया था, लेकिन हाल तक इसे संपूर्ण वैज्ञानिक दिशा के लिए काम माना जाता था। व्यक्तिगत मामले - चौथी डिग्री, नियमित सरल वाले - को पहले Lean में स्थानांतरित कर दिया गया था। नए भंडार के साथ, वेदिक की 100 औपचारिकीकरण कार्यों की पूरी सूची बंद हो गई है: जिस बेंचमार्क के विरुद्ध इस क्षेत्र की तुलना की गई थी वह बीस वर्ष पुराना है।

वैसे, बज़र्ड ईमानदारी से लिखते हैं: गणितीय रूप से, काम कुछ भी नया नहीं बताता है - वह पहले से ही विल्स पर विश्वास करते थे। मूल्य कहीं और है. गणित में एक नए लेख की समीक्षा करने में महीनों या वर्षों का समय लग जाता है; यदि किसी मशीन को तुरंत प्रमाण को औपचारिक रूप देने के लिए कहा जा सकता है, तो सहकर्मी समीक्षा कम हो जाएगी और विशेषज्ञ स्तर पर छिपी हुई धारणाएं सामने आने लगेंगी। विज्ञान के लिए, जहां सब कुछ निष्कर्षों की ईमानदारी पर निर्भर है, यह एक गंभीर बदलाव है।

वो 11 दिन अंदर से कैसे दिखते थे

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

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

कहाँ देखना है

रिपॉजिटरी GitHub पर पोस्ट की गई है - यदि आप चाहें, तो आप स्वयं चेक चला सकते हैं यदि आपके पास 96 कोर और मजबूत तंत्रिकाओं वाली मशीन है। प्राथमिक स्रोत: एंथ्रोपिक से विश्लेषण और बज़र्ड की पोस्ट ज़ेना प्रोजेक्ट ब्लॉग पर।

और यदि, 13 मिलियन पंक्तियों वाली कहानी के बाद, आप यह देखना चाहते हैं कि आधुनिक मॉडल छोटे कार्यों - एल्गोरिदम, कोड, गणना - को कैसे संभालते हैं - अनुभागों पर एक नज़र डालें "कोड" और "बात करना" NeuralSpace पर: वहां आप मॉडलों के साथ प्रयोग कर सकते हैं और उन्हें एपीआई के माध्यम से अपनी परियोजनाओं से जोड़ सकते हैं।