AI ने Lean में फ़र्मा के अंतिम प्रमेय को औपचारिक रूप दिया: कंप्यूटर-जाँचे प्रमाण का क्या अर्थ है

फ़र्मा का अंतिम प्रमेय कहता है कि जब n, 2 से बड़ा हो, तो xⁿ + yⁿ = zⁿ का धनात्मक पूर्णांकों में कोई हल नहीं है। पियरे द फ़र्मा ने 1630 के दशक में इसे किताब के हाशिये पर लिखा; एंड्रयू वाइल्स ने 1990 के दशक में अब तक लिखे गए सबसे कठिन गणित से इसे सिद्ध किया। 4 सितंबर 2026 को Anthropic ने घोषणा की कि Claude ने 11 दिनों में उस प्रमाण का पहला पूर्ण कंप्यूटर-जाँचा संस्करण तैयार किया^[1]। यह लेख बताता है कि इसका क्या अर्थ है, यह गणित जितनी ही कंप्यूटर विज्ञान की कहानी क्यों है, और इसका क्या अर्थ नहीं है।

समयरेखा

1630 का दशकफ़र्मा ऐसे प्रमाण का दावा करते हैं जिसके लिए "यह हाशिया बहुत तंग है"।
1994–95एंड्रयू वाइल्स (रिचर्ड टेलर के साथ) प्रमाण पूरा करते हैं।
2024केविन बज़र्ड इंपीरियल कॉलेज लंदन में प्रमाण को Lean में औपचारिक रूप देने की मानव-नेतृत्व परियोजना शुरू करते हैं।
अगस्त 2026Claude एजेंट 11 दिनों में Lean में पूर्ण औपचारिकीकरण पूरा करते हैं।
4 सितंबर 2026Anthropic परिणाम घोषित करता है; बज़र्ड समीक्षा करते हैं।

प्रूफ़ असिस्टेंट क्या करता है

GCSE मूल

मनुष्य का लिखा प्रमाण छोटे क़दम पाठक पर छोड़ देता है। विशेषज्ञ समीक्षक भी कोई कमी चूक सकते हैं। Lean जैसा प्रूफ़ असिस्टेंट यह जोखिम ख़त्म करता है। आप परिभाषाएँ और प्रमाण कोड के रूप में लिखते हैं, और एक छोटा, भरोसेमंद जाँचकर्ता (कर्नेल) पुष्टि करता है कि हर क़दम तर्क और पिछले परिणामों से निकलता है। अगर कोड कंपाइल हो जाए, तो प्रमेय सत्यापित है। यह ऐसे कंपाइलर जैसा है जो आपका प्रोग्राम तब तक नहीं चलाता जब तक वह सिद्ध रूप से सही न हो।

19 में से 0 क़दम जाँचे गए

औपचारिक प्रमाण एक वृक्ष है: अंतिम प्रमेय बड़े मध्यवर्ती परिणामों पर टिका है, वे लेमा पर, और लेमा परिभाषाओं व मूल तथ्यों पर। Lean हर कड़ी जाँचता है। नींव से शुरू करके वृक्ष जाँचने के लिए बटन दबाइए। योजनाबद्ध चित्र; असली वृक्ष में लगभग 29,500 प्रमेय हैं।

Claude ने असल में क्या किया

A-Level विस्तार

इसने वाइल्स के प्रमाण के एक सरलीकृत संस्करण को औपचारिक रूप दिया, जो डार्मन, डायमंड और टेलर का है^[1]।
परिणाम में लगभग 1.3 करोड़ पंक्तियाँ Lean और लगभग 30,300 प्रमेय हैं (अंतिम प्रमाण में लगभग 29,500 इस्तेमाल हुए), जो Mathlib से पाँच गुना से भी बड़ा है^[1]।
दर्जनों Claude एजेंटों ने 11 दिनों तक समानांतर काम किया, एक आंतरिक शोध मॉडल के लगभग छह अरब आउटपुट टोकन इस्तेमाल करके^[1]।
मानवीय गणितीय योगदान Anthropic के शोधकर्ता तियानयी पेंग के कभी-कभार के उच्च-स्तरीय निर्देशों तक सीमित रहा^[1]।
प्रमाण केवल Lean के तीन मानक अभिगृहीतों पर टिका है, और एक तुलनित्र ने पुष्टि की कि अंतिम प्रमेय ठीक वही कहता है जो Mathlib का अपना फ़र्मा के अंतिम प्रमेय का कथन कहता है^[1]।
इसने इंपीरियल कॉलेज लंदन में केविन बज़र्ड की FLT परियोजना के हिस्से दोबारा इस्तेमाल किए, और बज़र्ड ने पूरे प्रमाण की समीक्षा की^[1]।

त्वरित जाँच

Lean में प्रमाण के "कंपाइल" होने का क्या मतलब है?

कथन जाँचना क्यों ज़रूरी है

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

वह अंतर जिसे छात्र अक्सर भ्रमित कर देते हैं

सही का मतलब सुरुचिपूर्ण (या नया) नहीं है।

यह एक मौजूदा प्रमाण का औपचारिकीकरण था, नया प्रमाण नहीं। और Anthropic कहता है कि उसका संस्करण "संभवतः ज़रूरत से कहीं लंबा" है, असफल प्रयासों ने लगभग 7% ग़ैर-बॉयलरप्लेट पंक्तियाँ छोड़ दीं^[1]। उपलब्धि सत्यापित काम की गति और पैमाने में है, नई गणितीय अंतर्दृष्टि में नहीं। कंप्यूटरों ने नए परिणाम सिद्ध करने में कैसे मदद की, यह जानने के लिए कंप्यूटर से हल हुई गणित की समस्याएँ पढ़िए।

परीक्षा-शैली का प्रश्न

फ़र्मा के अंतिम प्रमेय के औपचारिक प्रमाण को उदाहरण बनाकर सत्यापन (verification) और वैधीकरण (validation) का अंतर समझाइए। [4 अंक]

आदर्श उत्तर और अंक विभाजन दिखाएँ

सत्यापन जाँचता है कि उत्पाद सही ढंग से बना है, यानी अपने विनिर्देश को पूरा करता है (1 अंक)
यहाँ Lean सत्यापित करता है कि प्रमाण का हर क़दम तार्किक रूप से सही है (1 अंक)
वैधीकरण जाँचता है कि सही उत्पाद बना है, यानी विनिर्देश वास्तव में ज़रूरी चीज़ से मेल खाता है (1 अंक)
यहाँ Lean कथन की Mathlib के स्वतंत्र FLT कथन से तुलना जाँचती है कि प्रमाण इच्छित प्रमेय को ही सिद्ध करता है (1 अंक)

परीक्षक किस पर ध्यान देता है: दोनों शब्दों की परिभाषा दें और हर एक को उदाहरण के किसी ख़ास हिस्से से जोड़ें।

सामान्य गलती: दोनों शब्दों को पर्यायवाची मानना। कोई प्रोग्राम हर सत्यापन जाँच पास करके भी ग़लत काम कर सकता है।

तर्क, प्रमाण और टेस्टिंग A-Level गणित और कंप्यूटर विज्ञान को जोड़ते हैं। हमारा लेख क्या AI सच में गणित कर सकता है? बड़ी तस्वीर दिखाता है, और मिलेनियम पुरस्कार समस्याएँ बताती हैं कि कौन-से प्रश्न अब भी खुले हैं।

स्रोत और आगे पढ़ने के लिए

Anthropic: Formalizing Fermat's Last Theorem (4 Sep 2026) — पैमाना, एजेंट, अभिगृहीत, मानवीय योगदान, बज़र्ड की समीक्षा, सावधानियाँ
AI Weekly: Claude formalized Fermat's Last Theorem in 11 days — समाचार कवरेज
Lean community: Mathlib — Lean की गणित लाइब्रेरी
Imperial College London: Fermat's Last Theorem formalisation project (Kevin Buzzard) — मानव-नेतृत्व परियोजना

अंतिम समीक्षा: 5 अक्टूबर 2026। आँकड़े सामान्यतः प्रकाशित विशिष्ट मान हैं, और नियम बदल सकते हैं। परीक्षा की भाषा प्रत्येक स्पेसिफिकेशन के अनुसार अलग हो सकती है, इसलिए अपना स्पेसिफिकेशन ज़रूर देखें।

अक्सर पूछे जाने वाले प्रश्न

क्या AI ने फ़र्मा का अंतिम प्रमेय सिद्ध किया?

नहीं: इसे 1990 के दशक में एंड्रयू वाइल्स ने सिद्ध किया। 2026 में हुआ यह कि Claude एजेंटों ने उस प्रमाण के एक संस्करण को Lean में अनूदित किया, एक प्रोग्रामिंग भाषा जिसका जाँचकर्ता हर तार्किक क़दम की पुष्टि करता है। 4 सितंबर 2026 को Anthropic द्वारा घोषित यह परिणाम प्रमेय का पहला पूर्ण, कंप्यूटर-जाँचा प्रमाण है।

Lean क्या है?

एक प्रूफ़ असिस्टेंट: ऐसी प्रोग्रामिंग भाषा जिसमें परिभाषाएँ, प्रमेय और प्रमाण कोड के रूप में लिखे जाते हैं। एक छोटा भरोसेमंद प्रोग्राम, कर्नेल, जाँचता है कि हर क़दम तर्क के नियमों और पिछले परिणामों से निकलता है। अगर प्रमाण कंपाइल हो जाए, तो केवल Lean में निर्मित अभिगृहीतों को मानते हुए प्रमेय सत्यापित है।

प्रमाण कितना बड़ा था?

लगभग 1.3 करोड़ पंक्तियाँ Lean कोड और लगभग 30,000 प्रमेय (अंतिम प्रमाण में लगभग 29,500 इस्तेमाल हुए), जो Lean की मुख्य सामुदायिक गणित लाइब्रेरी Mathlib से पाँच गुना से भी बड़ा है। इसमें 11 दिन लगे, दर्जनों Claude एजेंट समानांतर काम करते रहे और Anthropic के शोधकर्ता तियानयी पेंग ने कभी-कभार उच्च-स्तरीय मार्गदर्शन दिया।

क्या AI का लिखा प्रमाण अच्छा है?

इस अर्थ में सही है कि Lean ने उसे जाँचा है, और इंपीरियल कॉलेज लंदन में मानव-नेतृत्व वाली FLT औपचारिकीकरण परियोजना चलाने वाले केविन बज़र्ड ने उसकी समीक्षा की। पर Anthropic कहता है कि यह संभवतः ज़रूरत से कहीं लंबा है, और असफल प्रयासों ने इसकी ग़ैर-बॉयलरप्लेट पंक्तियों का लगभग 7% छोड़ दिया। सही और सुरुचिपूर्ण अलग बातें हैं।

पाठकों की रेटिंग और समीक्षाएँ

इस लेख को कई अलग-अलग पहलुओं पर रेट करें — आपकी रेटिंग दूसरे पाठकों की मदद करती है, और हमें बेहतर बनाने में मदद करती है।

क्या यह लेख उपयोगी था?

हमें अपनी राय बताएं — कोई सुधार, कोई सवाल जिसका जवाब नहीं मिला, या कोई विषय जिसे आप अगली बार कवर होते देखना चाहते हैं।

बात करना पसंद करेंगे? अपनी सुविधा के समय पर मुफ़्त वीडियो कॉल बुक करें: छोटे सवाल के लिए 15 मिनट, बाकी के लिए 30 मिनट। समय आपके अपने टाइम ज़ोन में दिखता है।

कॉल बुक करें

लेखक के बारे में

Sudershan Soni

मोस्तक सर्विसेज़ में संस्थापक व मुख्य शिक्षक — MSc-योग्य गणित, विज्ञान, कंप्यूटर साइंस और STEM शिक्षक, 20+ वर्षों के पेशेवर अनुभव के साथ, 11+ और GCSE से A-Level और उससे आगे तक के छात्रों को दुनिया भर में ऑनलाइन पढ़ाते हैं।

पूरी प्रोफ़ाइल पढ़ें