💻 computer science

Auto formalisation of Chaitin and of the surprise incompleteness Theorem

यह शोध पत्र एक एलएलएम (Claude) का उपयोग करके चैटिन के प्रथम अपूर्णता प्रमेय के प्रमाण और कृतनमैन-राज़ सरप्राइज एग्जामिनेशन पैराडॉक्स वाले द्वितीय अपूर्णता प्रमेय के अगडा (Agda) में ऑटोफॉर्मलाइजेशन के लिए एक केस स्टडी प्रस्तुत करता है, जो जटिल कम्प्यूटेशनल सिमुलेशन बनाने और मशीन-चेक्ड प्रमाण उत्पन्न करने की मॉडल की क्षमता को प्रदर्शित करता है और साथ ही गणितीय तर्क में वर्तमान शक्तियों और सीमाओं को भी उजागर करता है।

मूल लेखक: Thierry Coquand

प्रकाशित 2026-06-12

📖 7 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Thierry Coquand

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

मुख्य चित्र: एक रोबोट को गणित करना सिखाना

कल्पना कीजिए कि आपके पास एक बहुत ही बुद्धिमान रोबोट (एक AI जिसका नाम क्लॉड है) और एक बहुत ही सख्त, नियमों से बंधा हुआ गणित का पाठ्यपुस्तक है जिसका नाम "बेसिक रिकर्सिव अरिथमेटिक" (Basic Recursive Arithmetic) है। यह पाठ्यपुस्तक एक खेल की तरह है जिसके बहुत विशिष्ट नियम हैं: आप केवल बुनियादी गिनती और सरल तर्क का उपयोग कर सकते हैं, कोई फैंसी शॉर्टकट या "जादुई" तरकीबें नहीं।

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

इसका उत्तर हाँ है। रोबोट ने इस सख्त भाषा में दो गहरे गणितीय विचारों को सफलतापूर्वक अनुवादित किया, जिससे एक ऐसा प्रमाण तैयार हुआ जिसे एक कंप्यूटर 100% सही होने के लिए जांच सकता है।

दो मुख्य विचार

यह शोध पत्र दो प्रसिद्ध अवधारणाओं पर ध्यान केंद्रित करता है: चैतिन का प्रमाण (Chaitin's Proof - जो पहले अपूर्णता प्रमेय से संबंधित है) और सरप्राइज एग्जामिनेशन पैराडॉक्स (Surprise Examination Paradox - जो दूसरे अपूर्णता प्रमेय का एक संस्करण है)।

1. "लघु विवरण" का खेल (चैतिन का प्रमाण)

कल्पना कीजिए कि आपके पास अक्षरों के एक सीमित सेट का उपयोग करके लिखी जा सकने वाली हर संभव कहानी का एक पुस्तकालय है।

नियम: कुछ कहानियाँ बहुत छोटी और वर्णन करने में आसान होती हैं। अन्य इतनी जटिल होती हैं कि उन्हें वर्णित करने का सबसे छोटा तरीका बस पूरी कहानी को लिखना ही होता है।
समस्या: चैतिन का प्रमाण एक ऐसी कहानी खोजने की कोशिश करता है जो इतनी जटिल है कि उसे एक छोटे प्रोग्राम द्वारा वर्णित नहीं किया जा सकता।
रोबोट की चुनौती: इस बात को सिद्ध करने के लिए, रोबोट को उस गणित की पाठ्यपुस्तक के भीतर एक "मशीन" बनानी पड़ी जो एक कहानी को पढ़ सके, उसे चला सके और देख सके कि वह क्या करती है।
बाधा: गणित की पाठ्यपुस्तक स्वाभाविक रूप से "प्रोग्राम चलाने" को संभालने के लिए बहुत सरल है क्योंकि इसके लिए आमतौर पर एक जटिल फंक्शन (जैसे कि एकमैन फंक्शन) की आवश्यकता होती है जिसे पाठ्यपुस्तक अनुमति नहीं देती है।
समाधान: मानव लेखक ने "गैंडी/हावर्ड मेजरेशन" (Gandy/Howard majorisation) नामक एक ट्रिक का सुझाव दिया। इसे रोबोट को एक ईंधन टैंक देने के रूप में समझें। मशीन को अनंत काल तक चलाने के बजाय, रोबोट सटीक रूप से गणना करता है कि एक प्रोग्राम को समाप्त करने के लिए कितने "ईंधन" (चरणों) की आवश्यकता है। यह एक विशेष "ईंधन गेज" बनाता है जो गारंटी देता है कि प्रोग्राम टैंक खत्म होने से पहले रुक जाएगा।
परिणाम: रोबोट ने अपने आप यह ईंधन गेज बनाया। इसने सिद्ध किया कि यदि आप एक ऐसे नंबर को वर्णित करने की कोशिश करते हैं जो "सरल रूप से वर्णित होने के लिए बहुत जटिल है," तो आप एक तार्किक विरोधाभास (जैसे कि यह सिद्ध करना कि 0, 1 के बराबर है) पैदा करते हैं।

2. "सरप्राइज एग्जाम" और रेत का ढेर

शोध पत्र का दूसरा भाग एक प्रसिद्ध विरोधाभास (paradox) से संबंधित है: एक शिक्षक घोषणा करता है कि अगले सप्ताह एक सरप्राइज परीक्षा होगी। छात्र तर्क देते हैं कि यह शुक्रवार नहीं हो सकता (क्योंकि यदि शुक्रवार तक परीक्षा नहीं हुई, तो वे जान जाएंगे कि यह शुक्रवार है), इसलिए यह गुरुवार भी नहीं हो सकता, और इसी तरह... जब तक वे इस निष्कर्ष पर नहीं पहुँचते कि परीक्षा हो ही नहीं सकती। लेकिन फिर शिक्षक बुधवार को परीक्षा ले लेता है, और वह एक सरप्राइज होता है।

शोध पत्र इस तर्क के एक संस्करण (क्रित्समैन और राज द्वारा) का उपयोग यह सिद्ध करने के लिए करता है कि एक गणितीय प्रणाली अपनी स्वयं की निरंतरता (consistency - कि इसमें विरोधाभास नहीं हैं) को सिद्ध नहीं कर सकती।

पुराना तरीका: पिछले प्रमाण विरोधाभास खोजने के लिए दिनों या संख्याओं की गिनती करते थे।
नया तरीका (सोराइट्स/रेत का ढेर): लेखक इसकी तुलना रेत के ढेर के विरोधाभास (Heap of Sand Paradox) से करते हैं।
- यदि आपके पास रेत का एक ढेर है और आप एक कण हटाते हैं, तो यह अभी भी एक ढेर है।
- यदि आप एक और कण हटाते हैं, तो यह अभी भी एक ढेर है।
- यदि आप एक-एक करके कण हटाते रहते हैं, तो अंततः आपके पास शून्य कण बचते हैं। लेकिन किस सटीक बिंदु पर यह "ढेर" होना बंद हो गया?
अनुप्रयोग:
- कल्पना कीजिए कि 0 से लेकर एक बहुत बड़ी संख्या $N$ तक की संख्याओं की एक सूची है।
- तर्क यह सिद्ध करने की कोशिश करता है: "यह असंभव है कि इन सभी संख्याओं का एक संक्षिप्त विवरण हो।"
- रोबोट इसे चरण-दर-चरण सिद्ध करता है। वह कहता है, "यदि हम यह मान लें कि 0 से $N$ तक की सभी संख्याओं का संक्षिप्त विवरण है, तो हमें एक विरोधाभास मिलता है।"
- फिर वह 0 को हटा देता है। "ठीक है, यदि 1 से $N$ तक की संख्याओं का संक्षिप्त विवरण है, तो भी विरोधाभास मिलता है।"
- वह एक-एक करके संख्या हटाता रहता है (जैसे रेत के कण हटाना)।
- अंततः, वह एक ऐसे बिंदु पर पहुँच जाता है जहाँ सूची खाली हो जाती है, लेकिन तर्क फिर भी एक विरोधाभास पैदा करता है।
ट्विस्ट: शोध पत्र तर्क देता है कि यह आत्म-संदर्भ (self-reference) का "दुष्चक्र" (vicious circle) नहीं है; यह रेत के ढेर जैसा है। आप एक कण (एक संख्या) सुरक्षित रूप से हटा सकते हैं, लेकिन यदि आप इसे करते रहते हैं, तो पूरी संरचना ढह जाती है। यह पतन सिद्ध करता है कि गणितीय प्रणाली खुद को तोड़े बिना यह सिद्ध नहीं कर सकती कि वह सुरक्षित (सुसंगत) है।

यह क्यों महत्वपूर्ण है (शोध पत्र के अनुसार)

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

निष्कर्ष

यह शोध पत्र एक केस स्टडी है जो दिखाता है कि AI अब औपचारिक गणित (formal mathematics) में एक शक्तिशाली भागीदार के रूप में कार्य कर सकता है। यह एक उच्च-स्तरीय विचार (जैसे "गणित की सीमाएँ हैं") को एक कठोर, मशीन-चेकेबल प्रारूप में अनुवादित कर सकता है।

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

तकनीकी सारांश: चैटिन और सरप्राइज इनकम्प्लीटनेस थ्योरम का ऑटो फॉर्मलाइजेशन

समस्या और संदर्भ
यह रिपोर्ट गोडेल के दूसरे इनकम्प्लीटनेस थ्योरम के ऑटो-फॉर्मलाइजेशन के एक पिछले प्रयोग का विस्तार करती है, जिसमें लार्ज लैंग्वेज मॉडल (LLM) क्लॉड (Claude) और प्रूफ़ असिस्टेंट एगडा (Agda) का उपयोग किया गया है। प्राथमिक उद्देश्य जटिल गणितीय प्रमाणों को औपचारिक रूप देने की वर्तमान LLMs की क्षमताओं और सीमाओं की जांच करना है, विशेष रूप से वे जो गणना के आंतरिक प्रतिनिधित्व (internal representation of computation) से जुड़े हैं। पेपर दो विशिष्ट लक्ष्यों पर केंद्रित है: चैटिन का प्रथम इनकम्प्लीटनेस थ्योरम का प्रमाण और कृतचमन-राज़ का "सरप्राइज एग्जामिनेशन पैराडॉक्स" वाला दूसरा इनकम्प्लीटनेस थ्योरम।

एक केंद्रीय तकनीकी चुनौती को संबोधित किया गया है जो बेसिक रिकर्सिव अरिथमेटिक (BRA) के भीतर गणना के एन्कोडिंग से जुड़ी है, जो कि गार्ड (Guard) द्वारा तैयार किया गया एक सिस्टम है जिसमें ऑब्जेक्ट क्वांटिफायर और मानक टैक्टिक्स का अभाव है। ऐसे सिस्टम में, एक आंतरिक मूल्यांकन फ़ंक्शन (evaluation function) को परिभाषित करना असंभव है क्योंकि यह प्रिमिटिव रिकर्सिव बाउंड्स (जैसे कि एकमैन फ़ंक्शन) को पार कर जाएगा। समस्या के लिए प्रोग्रामों और उनके निष्पादन चरणों (execution steps) को पूरी तरह से ऑब्जेक्ट लैंग्वेज के भीतर प्रस्तुत करने की आवश्यकता है, बिना मेटा-लेवल फ़ंक्शंस या बाहरी लाइब्रेरीज़ पर निर्भर रहे।

कार्यप्रणाली (Methodology)
यह प्रोजेक्ट एक "स्पार्टन" दृष्टिकोण अपनाता है जहाँ मानव लेखक द्वारा एगडा (Agda) कोड की एक भी पंक्ति नहीं लिखी गई; फॉर्मलाइजेशन उच्च-स्तरीय गणितीय विवरणों के आधार पर क्लॉड द्वारा स्वायत्त रूप से जनरेट किया गया था। कार्यप्रणाली निम्नलिखित तकनीकी रणनीतियों पर निर्भर करती है:

टर्नरी स्ट्रिंग एनकोडिंग (Ternary String Encoding): प्रोग्रामों को प्राकृतिक संख्याओं के रूप में दर्शाया जाता है जिन्हें टर्नरी स्ट्रिंग्स (अंक 1, 2, 3) के रूप में व्याख्यायित किया जाता है। यह $L^*$ लंबाई के अधिकतम प्रोग्रामों के सेट को प्राकृतिक संख्याओं के एक सरल प्रारंभिक खंड $\{p < N\}$ के रूप में मानने की अनुमति देता है, जहाँ $N = 3^{L^*+1}$ है, जिससे जटिल एन्यूमरेशन तंत्रों से बचा जा सकता है।
CK मशीन कार्यान्वयन: एक ग्लोबल इवैल्यूएशन फ़ंक्शन की आवश्यकता को दरकिनार करने के लिए, क्लॉड ने स्वायत्त रूप से एक कंटीन्यूएशन स्टैक स्मॉल-स्टेप इवैल्यूएशन मशीन (एक लैंडिन CK मशीन) का निर्माण किया। यह मशीन एक्सप्रेशंस को डिकंपोज करती है और कंटीन्यूशन का एक स्टैक प्रबंधित करती है, जिससे स्टेप-बाय-स्टेप गणना का अनुकरण (simulation) संभव होता है।
गैंडी/हावर्ड मेजरोसेशन (Gandy/Howard Majorisation): एक महत्वपूर्ण बाधा यह सिद्ध करना था कि मशीन किसी दिए गए फ़ंक्शन $f$ के लिए विशिष्ट चरणों के भीतर रुकती (halt) है। चूंकि स्टेप काउंट एक मेटा-लेवल नेचुरल नहीं हो सकता, इसलिए लेखकों ने क्लॉड को गैंडी/हावर्ड मेजरोसेशन पद्धति का उपयोग करने के लिए निर्देशित किया। इसमें प्रिमिटिव रिकर्सन के माध्यम से एक क्लोज्ड कॉम्बिनेटर fuel(f) को परिभाषित करना शामिल है जो वास्तव में $f$ के रनिंग टाइम को मेजरो (majorise) करता है। यह इंटरप्रेटर की पूर्णता (completeness) को BRA के भीतर ही घोषित और सिद्ध करने की अनुमति देता है।
सरप्राइज एग्जामिनेशन को सोराइट्स (Sorites) के रूप में: दूसरे इनकम्प्लीटनेस थ्योरम के प्रमाण में उन काउंटिंग तर्कों से बचा गया है जो कृतचमन और राज़ द्वारा उपयोग किए गए थे। इसके बजाय, यह तर्क को एक सोराइट्स (रेत के ढेर का विरोधाभास) के रूप में मॉडल करता है। यह स्टेज $r$ पर बाहरी इंडक्शन (external induction) के माध्यम से आगे बढ़ता है, यह सिद्ध करते हुए कि अंतराल $[r, N]$ में सभी संख्याओं का संक्षिप्त विवरण (short description) होना असंभव है।

प्रमुख योगदान और परिणाम
पेपर चर्च के बेसिक रिकर्सिव अरिथमेटिक के लिए एगडा (Agda) में एक पूर्णतः मशीन-चेक्ड प्रमाण प्रस्तुत करता है:

ऑटो-फॉर्मलाइज्ड चैटिन थ्योरम: सिस्टम ने सफलतापूर्वक चैटिन के प्रमाण को औपचारिक रूप दिया, जो लाइर सेंटेंस (liar sentence) को कोलमोगोरोव कॉम्प्लेक्सिटी से बदल देता है। यह फॉर्मलाइजेशन एक स्पष्ट प्रूफ-ट्रांसफॉर्मर $G$ उत्पन्न करता है। थ्योरम बताता है कि यदि एक टर्म $w$ , इनकम्प्रेसिबिलिटी स्टेटमेंट $K(out(w)) > L^*$ के प्रमाण को कोड करता है, तो $G \cdot w$ , $0=1$ के प्रमाण को कोड करता है। इसे प्रमाण योग्यता के मेटा-थ्योरेटिक निषेध के बजाय एक सकारात्मक ऑब्जेक्ट-लेवल इम्प्लिकेशन के रूप में तैयार किया गया है।
आंतरिक दूसरा इनकम्प्लीटनेस (Internalised Second Incompleteness): पेपर यह दिखाने के लिए कृतचमन-राज़ तर्क को औपचारिक रूप देता है कि यदि $T$ अपनी स्थिरता ( $Con_T$ ) को सिद्ध करता है, तो $T$ असंगत ( $0=1$ ) है। प्रमाण $S(0)$ (पिजनहोल प्रिंसिपल) से $S(N+1)$ (एक विरोधाभास) तक के डिसेंट (descent) के माध्यम से आगे बढ़ता है, जहाँ प्रत्येक चरण $S(r) \to S(r+1)$ कंसिस्टेंसी हाइपोथेसिस को ठीक एक बार उपभोग करता है।
रचनात्मक अंतर्दृष्टि (Constructive Insights): फॉर्मलाइजेशन रचनात्मक गणित में पार्शियल फंक्शन्स की भूमिका को उजागर करता है। विशेष रूप से, डायगोनल प्रोग्राम लक्ष्य मिलने तक व्युत्पन्न सूत्रों (derivable formulas) को सूचीबद्ध करता है। जबकि प्रोग्राम को बाह्य रूप से समाप्त होने के लिए सिद्ध किया गया है, इसकी साइज की गणना बिना समाप्ति प्रमाण को आंतरिक बनाने के की जाती है। यह ब्लम के स्पीड-अप फेनोमेनन (Blum's speed-up phenomenon) के प्रकटीकरण को दर्शाता है, जहाँ एक पार्शियल रिकर्सिव प्रोग्राम (जिसे बाह्य प्रमाण द्वारा टोटल रखा गया है) का उपयोग करने से उन प्रोग्रामों की तुलना में अनबाउंडेडली छोटे प्रोग्राम प्राप्त होते हैं जो आंतरिक रूप से समाप्ति को प्रमाणित करने चाहिए।

महत्व और दावे
पेपर का दावा है कि वर्तमान कोडिंग LLMs, जैसे कि क्लॉड, गणितीय शोध पत्रों के सूक्ष्म विवरणों को समझने के लिए प्रभावी उपकरण हैं, बशर्ते वे निरंतर पर्यवेक्षण के तहत कार्य करें। यह प्रोजेक्ट एक केस स्टडी के रूप में कार्य करता है जो प्रदर्शित करता है कि:

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

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