Anthropic की 4 सितंबर 2026 की तकनीकी घोषणा के अनुसार, Claude-आधारित बहु-अभिकर्ता व्यवस्था ने 11 दिनों में Fermat के अंतिम प्रमेय का पूर्ण Lean औपचारिकीकरण तैयार किया। अभियान में 30,300 प्रमेयों के कंप्यूटर-जाँच योग्य प्रमाण बने, अंतिम प्रमाण ने उनमें से लगभग 29,500 का उपयोग किया और कुल सामग्री करीब 1.3 करोड़ Lean पंक्तियों तक पहुँची।
इसका अर्थ यह नहीं कि Claude ने Fermat के अंतिम प्रमेय का नया गणितीय समाधान खोजा। Nature की 7 सितंबर की रिपोर्ट भी 4 सितंबर को सामने आए परिणाम को पहले से सिद्ध प्रमेय का पहला पूर्ण कंप्यूटर-सत्यापित रूप बताती है: Andrew Wiles और Richard Taylor से जुड़ा स्थापित तर्क वही है, लेकिन अब Lean उसका हर औपचारिक कदम दोबारा जाँच सकता है।
प्रमाण, औपचारिकीकरण और नया गणित अलग हैं
गणितीय खोज और मशीन-जाँच योग्य प्रस्तुति एक ही उपलब्धि नहीं हैं। Wiles ने 1990 के दशक में प्रमेय की मूल गणितीय बाधा पार की थी; त्रुटि सुधारे जाने के बाद सही प्रमाण 1995 में प्रकाशित हुआ। Claude का काम Frey, Serre, Ribet, Wiles और Taylor–Wiles की स्थापित तर्क-परंपरा तथा Darmon, Diamond और Taylor की व्याख्या का अनुसरण करता है।
मनुष्यों के लिए लिखा शोध-पत्र परिचित परिभाषाएँ, स्वीकृत परिणाम और बीच के सहज कदम छोड़ सकता है। Lean को प्रत्येक परिभाषा, निर्भरता और निष्कर्ष औपचारिक भाषा में चाहिए, ताकि उसका छोटा सत्यापन केंद्र—कर्नेल—तय नियमों के आधार पर उसे स्वीकार या अस्वीकार कर सके। इसलिए औपचारिकीकरण केवल पाठ का अनुवाद नहीं, बल्कि पूरे तर्क को स्पष्ट मशीन-जाँच योग्य संरचना में पुनर्निर्मित करना है।
Imperial College London के गणितज्ञ Kevin Buzzard ने अपने Xena Project विश्लेषण में बताया कि उन्होंने कोड संकलित करके तुलनित्र चलाया और जाँच सफल रही। उनके अनुसार औपचारिकीकरण शुरुआती साहित्य का निष्ठापूर्वक अनुसरण करता है और गणितीय रूप से लगभग कुछ नया नहीं जोड़ता; वास्तविक नवीनता इतने बड़े प्रमाण को स्वचालित ढंग से औपचारिक बनाने की गति और पैमाने में है।
11 दिनों का परिणाम एक पूरी व्यवस्था ने बनाया
“Claude ने 11 दिन में किया” का अर्थ यह नहीं कि एक संवाद खिड़की ने अकेले एक लंबा उत्तर लिख दिया। दर्जनों Claude अभिकर्ताओं ने समानांतर रूप से अवधारणाएँ परिभाषित कीं, सहायक परिणाम सिद्ध किए और उन परिणामों को जोड़कर अधिक कठिन कथनों तक पहुँचे। Anthropic के शोधकर्ता Tianyi Peng ने बीच-बीच में सीमित उच्च-स्तरीय प्राथमिकताएँ बताईं।
काम को Prove2Me नामक सहयोगी मंच ने व्यवस्थित किया। उसने प्रमेयों और उनकी निर्भरताओं का निर्देशित अचक्रीय आलेख सँभाला, कथनों को उनके प्रमाणों से अलग रखकर संकलन का बोझ घटाया और प्राकृतिक भाषा के विवरणों के आधार पर पहले से बने परिणाम खोजने में मदद की। शुरुआती प्रयासों में अभिकर्ता परियोजना की स्थिति भूलने लगे थे; Prove2Me और Claude Code-आधारित बहु-अभिकर्ता ढाँचे के बाद समन्वय सुधरा।
अभियान ने लगभग छह अरब आउटपुट टोकन इस्तेमाल किए और एक आंतरिक सामान्य-उद्देश्य शोध मॉडल पर चला। इसलिए 11 दिन मानव श्रम, संगणकीय संसाधन और सहायक ढाँचे से अलग कोई शुद्ध मॉडल-गति माप नहीं हैं। उपलब्धि Claude की क्षमता के साथ उस व्यवस्था की भी है जिसने हजारों परस्पर निर्भर औपचारिक कार्य बाँटे और जोड़े।
सार्वजनिक प्रमाण को किन स्तरों पर जाँचा गया
Anthropic का सार्वजनिक GitHub संग्रह पूर्ण Lean 4 साक्ष्य, प्रमाण-पथ, परिभाषाएँ और सत्यापन निर्देश उपलब्ध कराता है। संग्रह के मुताबिक सभी 60,475 मॉड्यूल Lean कर्नेल से जाँचे गए; अंतिम कथन केवल Lean के तीन मानक स्वयंसिद्धों पर निर्भर है और अधूरे प्रमाण-संकेत या अतिरिक्त स्वयंसिद्ध जैसे रास्तों को अलग जाँच रोकती है।
सत्यापन की दूसरी परत में तुलनित्र ने सिद्ध कथन और उसमें प्रयुक्त स्थिरांकों को Mathlib में दिए Fermat कथन से मिलाया तथा पूरे प्रमाण को कर्नेल के जरिये दोहराया। तीसरी परत में Rust में लिखा स्वतंत्र कर्नेल nanoda उसी वातावरण की 10,52,234 घोषणाएँ बिना त्रुटि स्वीकार कर चुका है। इससे यह जोखिम घटता है कि सही नाम के नीचे कोई कमजोर या अलग कथन सिद्ध कर दिया गया हो।
फिर भी सार्वजनिक उपलब्धता आसान पुनरुत्पादन के बराबर नहीं है। संग्रह लगभग 67 गीगाबाइट निर्माण स्थान बताता है; मूल 96-कार्य निर्माण में 153 गीगाबाइट तक स्मृति लगी और तुलनित्र की जाँच ने लगभग 15 घंटे तथा 230 गीगाबाइट की चरम स्मृति ली। विशेषज्ञ निर्देशों और पर्याप्त हार्डवेयर के साथ जाँच दोहरा सकते हैं, लेकिन यह सामान्य लैपटॉप पर हल्का प्रयोग नहीं है।
मशीन की स्वीकृति क्या बताती है—और क्या नहीं
Lean की स्वीकृति बताती है कि औपचारिक अंतिम कथन घोषित परिभाषाओं और स्वयंसिद्धों से तार्किक रूप से निकलता है। यह किसी मध्यवर्ती प्रमेय के नाम, व्याख्या या गणितीय महत्व की मानवीय गुणवत्ता अपने आप प्रमाणित नहीं करती। संग्रह भी स्पष्ट करता है कि नाम और कथन में अंतर हो तो औपचारिक कथन ही निर्णायक है।
यह 1.3 करोड़ पंक्तियों का शोध-साक्ष्य संक्षिप्त, शिक्षण योग्य या सीधे Mathlib में मिलाने के लिए तैयार पुस्तकालय होने का दावा नहीं करता। संग्रह को अनुरक्षित परियोजना के बजाय शोध-कलाकृति बताया गया है और बाहरी योगदान स्वीकार करने की योजना नहीं है। समुदाय के लिए अगला प्रश्न प्रमाण के अस्तित्व का नहीं, उसकी संरचना, पुनः उपयोग योग्य हिस्सों और मानवीय समझ में उसके स्थान का है।
अभी पुष्टि इतनी है: पुराना Wiles-आधारित तर्क पूर्ण मशीन-जाँच योग्य रूप में उपलब्ध है, Lean और दो अतिरिक्त सत्यापन विधियाँ उसे स्वीकार कर चुकी हैं, और एक बाहरी विशेषज्ञ ने कोड संकलित करके तुलनित्र चलाया है। Claude ने Fermat का नया गणितीय प्रमाण नहीं रचा; उसने स्थापित प्रमाण को पहली बार आरंभ से अंत तक कंप्यूटर से जाँचे जा सकने वाले औपचारिक साक्ष्य में बदला।
