क्या AI ने फर्मा के अंतिम प्रमेय को "सुलझाया"? 11 दिनों में पूरा हुआ 1.3 करोड़ पंक्तियों का प्रमाण गणित को कैसे बदल रहा है

11 दिनों में "सिद्ध" हुई 350 साल पुरानी पहेली

गणित के इतिहास में सबसे प्रसिद्ध पहेलियों में से एक फिर से दुनिया का ध्यान आकर्षित कर रही है।

Anthropic ने सितंबर 2026 में घोषणा की कि उनकी AI "Claude" ने फर्मा के अंतिम प्रमेय के लिए एक पूर्ण औपचारिक प्रमाण तैयार किया है जिसे कंप्यूटर द्वारा शुरू से अंत तक सत्यापित किया जा सकता है। इस कार्य में 11 दिन लगे। उत्पन्न हुआ Lean कोड लगभग 1.3 करोड़ पंक्तियों तक पहुंच गया, और कार्य के दौरान 33,000 प्रमेय सिद्ध किए गए, जिनमें से 29,500 को अंतिम प्रमाण में उपयोग किया गया।

इन संख्याओं को देखकर ऐसा लग सकता है कि AI ने मानवता को सदियों तक परेशान करने वाली पहेली को केवल 11 दिनों में हल कर दिया। लेकिन यहाँ एक महत्वपूर्ण भिन्नता है। Claude ने कोई अज्ञात समाधान खोजा नहीं। उसने एंड्रयू वाइल्स और रिचर्ड टेलर द्वारा 1990 के दशक में पूरा किए गए और गणितीय समुदाय द्वारा सही माने गए प्रमाण को कंप्यूटर द्वारा तार्किक रूप से सत्यापित की जा सकने वाली भाषा में अनुवाद किया और विशाल मध्यवर्ती भागों को भरा।

"नए प्रमाण की खोज" नहीं बल्कि "मौजूदा प्रमाण की पूर्ण मशीन सत्यापन"। इस भिन्नता को समझे बिना इस उपलब्धि को अधिक आंका जाएगा। दूसरी ओर, औपचारिकता को केवल अनुवाद कार्य मानना इसकी कठिनाई और इस बार के प्रभाव को कम आंकना होगा।

फर्मा द्वारा छोड़ी गई एक पंक्ति

फर्मा का अंतिम प्रमेय यह दावा करता है कि सकारात्मक पूर्णांक a, b, c और 2 से बड़े पूर्णांक n के लिए, "a की n घात + b की n घात = c की n घात" को संतुष्ट करने वाला कोई समूह मौजूद नहीं है।

पियरे डे फर्मा ने लगभग 1637 में प्राचीन ग्रीक गणित पुस्तक 'अर्थमेटिका' के हाशिये में यह दावा लिखा और कहा कि उसने एक अद्भुत प्रमाण खोजा है, लेकिन यह हाशिया उसे लिखने के लिए बहुत छोटा है। हालांकि, वह प्रमाण कभी नहीं मिला।

इसके बाद, कई पीढ़ियों के गणितज्ञों ने चुनौती ली, और व्यक्तिगत घातांक के लिए प्रमाण प्रगति करते रहे, लेकिन सामान्य मामले के लिए यह 350 से अधिक वर्षों तक अनसुलझा रहा। 1993 में एक मोड़ आया। वाइल्स ने वर्षों की गुप्त शोध के बाद प्रमाण प्रस्तुत किया, लेकिन सत्यापन के दौरान एक गंभीर दोष पाया गया। वाइल्स ने टेलर के साथ मिलकर इसे ठीक किया और 1994 में समस्या को हल किया। शोधपत्र 1995 में प्रकाशित हुआ।

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

"मानव के लिए स्पष्ट" कंप्यूटर के लिए नहीं

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

हालांकि, कंप्यूटर "यह स्पष्ट है" का अनुमान नहीं लगाता। परिभाषा, पूर्वधारणा, प्रकार, उपयोग किए गए प्रमेय, और उनसे निकाले गए निष्कर्षों को सटीक रूप से निर्दिष्ट करना पड़ता है, और यह दिखाना होता है कि प्रत्येक चरण नियमों का पालन करता है। इस कार्य में उपयोग किया गया था, Lean नामक प्रमेय प्रमाण सहायक प्रणाली।

Lean में, प्रमाण को एक प्रोग्राम के समान रूप में लिखा जाता है। दर्ज किए गए प्रमाण को तार्किक नियमों का पालन करने के लिए एक छोटा कर्नेल सत्यापित करता है, और यदि कोई छलांग होती है तो उसे स्वीकार नहीं करता। इस अर्थ में, औपचारिक प्रमाण गणितीय दावे के लिए एक बहुत ही कठोर स्वचालित परीक्षण के समान है।

कठिनाई यह है कि वाइल्स के शोधपत्र को केवल मशीन भाषा में बदलने से काम नहीं चलता। मानव-उन्मुख प्रमाण, बीजगणित, ज्यामिति, हार्मोनिक विश्लेषण, और संख्या सिद्धांत जैसे विशाल ज्ञान प्रणालियों पर आधारित होते हैं। यदि आवश्यक अवधारणाएं या सहायक प्रमेय Lean की साझा लाइब्रेरी में मौजूद नहीं हैं, तो उन्हें भी नए सिरे से परिभाषित और सिद्ध करना होगा। 1.3 करोड़ पंक्तियों का यह पैमाना इस "अदृश्य नींव" को एक-एक करके बनाने का परिणाम भी है।

कई AI ने विशाल प्रमाण को विभाजित किया

Anthropic के प्रयोग में, दर्जनों Claude एजेंट्स ने समानांतर में काम किया। एक एजेंट ने अवधारणाओं को परिभाषित किया, दूसरे एजेंट ने सहायक प्रमेयों को सिद्ध किया, और अन्य एजेंट ने उन्हें संयोजित किया और उच्चतर प्रमेयों की ओर बढ़ा। यह मानव द्वारा किए गए सहयोगी अनुसंधान की तरह, AI समूह ने बड़े पैमाने पर विभाजन किया।

हालांकि, शुरुआत से ही सब कुछ सुचारू नहीं था। प्रारंभिक प्रयासों में, एजेंट्स ने परियोजना की समग्र प्रगति को खो दिया और एक-दूसरे के परिणामों का सही उपयोग नहीं कर सके। दीर्घकालिक कार्यों में, न केवल व्यक्तिगत AI की तर्कशक्ति बल्कि यह प्रबंधन करने की प्रणाली कि कौन सा कार्य समाप्त हो गया है और आगे क्या सिद्ध किया जाना चाहिए, निर्णायक रूप से महत्वपूर्ण था।

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

अंततः AI समूह ने लगभग 60 अरब आउटपुट टोकन का उपभोग किया और 11 दिनों से कम में प्रमाण की जड़ तक पहुंच गया। Anthropic के अनुसार, Lean द्वारा जांच के अलावा, प्रमेय के अंतिम विवरण की तुलना मौजूदा लाइब्रेरी Mathlib के फर्मा के अंतिम प्रमेय से भी की गई। इसका मतलब यह है कि उन्होंने किसी अन्य समस्या को प्रमाणित करके समाप्त नहीं किया, बल्कि लक्षित दावे तक पहुंचने की पुष्टि की।

मानव के 5 साल की योजना और AI के 11 दिन की तुलना नहीं की जा सकती

इस बार अक्सर तुलना की जाती है, इंपीरियल कॉलेज लंदन के गणितज्ञ केविन बज़ार्ड द्वारा संचालित मानव-केंद्रित औपचारिकता परियोजना के साथ। यह परियोजना 2024 में शुरू हुई और कई वर्षों में फर्मा के अंतिम प्रमेय को Lean में औपचारिक बनाने का लक्ष्य है।

"मानव द्वारा 5 साल में किया गया कार्य AI ने 11 दिनों में समाप्त कर दिया" का वर्णन प्रभावशाली है, लेकिन दोनों के उद्देश्य पूरी तरह से समान नहीं हैं। Anthropic की उपलब्धि का प्राथमिक उद्देश्य प्रमेय को अंत से अंत तक मशीन द्वारा सत्यापित करने योग्य बनाना था। जबकि बज़ार्ड और उनकी टीम का उद्देश्य साझा लाइब्रेरी में शामिल किए जा सकने वाले बुनियादी सिद्धांतों को व्यवस्थित करना और मानव को आधुनिक प्रमाणों का अन्वेषण करते हुए सीखने योग्य गतिशील दस्तावेज़ बनाना भी है।

संक्षेप में "पास" होने वाले विशाल कोड को बनाना और गणितज्ञों द्वारा समझा जा सके, पुनः उपयोग किया जा सके, और अगले अनुसंधान से जोड़ा जा सके, यह एक अलग चुनौती है। Anthropic ने स्वयं भी बताया कि उन्होंने मानव परियोजनाओं और मौजूदा Mathlib द्वारा निर्मित नींव का उपयोग किया। इस प्रतिस्पर्धा को AI बनाम गणितज्ञ की सरल गति प्रतिस्पर्धा के रूप में चित्रित करना सटीक नहीं है।

फिर भी, अंत से अंत तक की औपचारिकता को वर्षों के बजाय दिनों में संभव बनाने का तथ्य महत्वपूर्ण है। बज़ार्ड ने अपने ब्लॉग में कहा कि इस उपलब्धि से गणितीय रूप से कुछ नया नहीं सीखा गया, लेकिन AI समूह ने हजारों पृष्ठों के बराबर साहित्य को 11 दिनों में औपचारिक बना दिया, जो स्वचालित औपचारिकता की संभावना को दर्शाता है। उन्होंने यह भी कहा कि पहले जो प्रमाण 99.9% सही माने जाते थे, औपचारिकता के बाद 100% निश्चितता हो जाती है, जो इस उपलब्धि का प्रतीक है।

सोशल मीडिया "आश्चर्य" और "यह कोई नई खोज नहीं है" में विभाजित

घोषणा के बाद, X, Reddit, Hacker News आदि पर बड़ी प्रतिक्रिया हुई। Lean के आधिकारिक अकाउंट ने इसे पहले पूर्ण कंप्यूटर सत्यापित प्रमाण के रूप में प्रस्तुत किया। Hacker News पर संबंधित पोस्ट में सैकड़ों टिप्पणियाँ आईं, और Reddit पर भी "कुछ साल पहले यह अकल्पनीय था", "1.3 करोड़ पंक्तियों के पैमाने से अभिभूत", "क्या 29,000 से अधिक मध्यवर्ती प्रमेयों की आवश्यकता है" जैसी आश्चर्यजनक प्रतिक्रियाएँ आईं।

दूसरी ओर, सबसे अधिक दोहराया गया चेतावनी थी कि शीर्षक को कैसे समझा जाए। "AI ने फर्मा के अंतिम प्रमेय को हल किया" के कथन के खिलाफ, "वाइल्स और टेलर ने इसे हल किया, और Claude ने मौजूदा प्रमाण को Lean में औपचारिक बनाया", "यह कोई नई गणितीय खोज नहीं है" जैसी टिप्पणियाँ पोस्ट की गईं। प्रतिक्रियाओं में, औपचारिकता को केवल स्वरूप परिवर्तन के रूप में हल्का मानने वाले विचार भी थे, लेकिन इसके खिलाफ यह तर्क भी था कि लंबी प्रमाण की खोई हुई नींव को भरना और हजारों मध्यवर्ती प्रमेयों को मशीन द्वारा सत्यापित करने योग्य बनाना अपने आप में एक बड़ी अनुसंधान उपलब्धि है।

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

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

सही प्रमाण और उपयोगी प्रमाण एक ही नहीं हैं

इस उपलब्धि में स्पष्ट कमजोरियाँ भी हैं। 1.3 करोड़ पंक्तियों का पैमाना प्रमुख गणितीय लाइब्रेरी Mathlib के पूरे आकार से 5 गुना अधिक है। मशीन द्वारा सहीता की पुष्टि की जा सकती है, लेकिन मानव के लिए पूरे चित्र को समझना, आवश्यक भागों को ढूंढना, और अन्य प्रमाणों में पुनः उपयोग करना आसान नहीं है।

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

इसलिए अगली चुनौती AI द्वारा बनाए गए कोड को संक्षिप्त करना, Mathlib में वापस लाना, और मानव द्वारा पढ़ी जा सकने वाली व्याख्या से जोड़ना होगी। AI ने मार्ग को कठोरता से खोला है, और मानव और AI मिलकर उस मार्ग को नक्शे में बदलेंगे। इस उपलब्धि को एक लक्ष्य के बजाय इस नई विभाजन का प्रारंभिक बिंदु माना जाना चाहिए।

समीक्षा की सीमाओं को पूरा करने वाला "थका हुआ दूसरा पाठक"

सबसे बड़ा महत्व यह नहीं है कि एक प्रसिद्ध प्रमेय को फिर से सिद्ध किया गया, बल्कि यह कि मशीन सत्यापन को बड़े पैमाने पर निष्पादित करने की संभावना को दिखाया गया, जो पहले लागत और समय के कारण व्यावहारिक नहीं था।

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

यह और भी महत्वपूर्ण होगा जब AI गणितीय उपलब्धियों का बड़े पैमाने पर उत्पादन शुरू कर दे। यदि AI शोधपत्रों के उम्मीदवारों को मानव द्वारा पढ़ने की गति से तेज उत्पन्न करता है, तो पारंपरिक समीक्षा प्रणाली इसे संभाल नहीं पाएगी। उत्पन्न करने वाले AI, औपचारिकता करने वाले AI, और अंततः एक छोटा सत्यापन कर्नेल जो तर्क की पुष्टि करता है, के संयोजन के माध्यम से, कम से कम यह सुनिश्चित किया जा सकेगा कि "तर्कसंगत रूप से निष्कर्ष निकाला गया है" को कुशलतापूर्वक सत्यापित किया जा सके।

बेशक, औपचारिक प्रमाण शोधपत्र के मूल्य को पूरी तरह से नहीं मापते। यह तय करना कि परिभाषाएँ वास्तविक समस्याओं का सही प्रतिनिधित्व करती हैं, शोध का विषय महत्वपूर्ण है, प्रमाण नई अंतर्दृष्टि प्रदान करता है, और व्याख्या शैक्षिक है, ये निर्णय शेष रहते हैं। इसके अलावा, सत्यापन सॉफ़्टवेयर या आधारभूत लाइब्रेरी पर विश्वास, विशाल कोड की ऑडिटिंग, और कंप्यूटेशनल संसाधनों का असमान वितरण जैसी समस्याएँ भी अपरिहार्य हैं।

फिर