💻 computer science

A formalization of the Gelfond-Schneider theorem

यह शोध पत्र गल्फोंड-स्नाइडर प्रमेय का एक औपचारिक रूप प्रस्तुत करता है, जो लीन 4 (Lean 4) में यह सिद्ध करके हिल्बर्ट की सातवीं समस्या का समाधान करता है कि यदि $\alpha \notin \{0,1\}$ एक बीजगणितीय संख्या है और $\beta$ एक अपरिमेय बीजगणितीय संख्या है, तो $\alpha^\beta$ एक अपरिमेय संख्या (transcendental) है।

मूल लेखक: Michail Karatarakis, Freek Wiedijk

प्रकाशित 2026-03-27

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

CC BY 4.0

मूल लेखक: Michail Karatarakis, Freek Wiedijk

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

कल्पना कीजिए कि आपके पास संख्याओं का एक विशाल, अनंत पुस्तकालय है। इनमें से अधिकांश संख्याएँ गणितीय अर्थों में "उबाऊ" हैं: वे बीजीय (algebraic) हैं। इसका मतलब है कि वे पूर्णांक गुणांकों वाले सरल समीकरणों के मूल (roots) हैं। उदाहरण के लिए, $\sqrt{2}$ बीजीय है क्योंकि यह समीकरण $x^2 - 2 = 0$ को हल करता है।

फिर, वहाँ "जंगली" (wild) संख्याएँ हैं, जिन्हें अतीन्द्रिय (transcendental) कहा जाता है। ये संख्याएँ इतनी जटिल हैं कि वे पूर्णांकों के साथ किसी भी सरल समीकरण का समाधान नहीं हो सकतीं। $\pi$ और $e$ जैसे प्रसिद्ध उदाहरण यहाँ मिलते हैं।

लंबे समय तक, गणितज्ञों को पता था कि ऐसे जंगली नंबर मौजूद हैं, लेकिन वे यह सिद्ध करने के लिए संघर्ष करते थे कि विशिष्ट संयोजनों का मेल जंगली होगा। यह एक बड़ी पहेली थी: यदि आप एक बीजीय संख्या (जैसे 2) को दूसरी बीजीय संख्या (जैसे $\sqrt{2}$ ) की घात के रूप में लेते हैं, तो क्या आपको एक जंगली संख्या प्राप्त होगी?

यह हिल्बर्ट की सातवीं समस्या थी, जिसे 1900 में प्रस्तुत किया गया था। 1934 में गेल्फ़ोंड और श्नाइडर द्वारा सिद्ध उत्तर, एक जोरदार हाँ है (कुछ अपवादों जैसे $2^1$ या $2^2$ को छोड़कर)। यदि आधार 0 या 1 नहीं है, और घातांक एक अपरिमेय बीजीय संख्या है, तो परिणाम निश्चित रूप से अतीन्द्रिय होगा।

शोध पत्र का मिशन: डिजिटल प्रमाण

यह शोध पत्र उन दो शोधकर्ताओं के बारे में है जिन्होंने निर्णय लिया कि वे उस 1934 के प्रमाण को एक ऐसी भाषा में अनुवादित करेंगे जिसे एक कंप्यूटर समझ सके और सत्यापित कर सके: Lean 4।

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

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

उन्होंने यह कैसे किया: जासूसी कहानी

यह सिद्ध करने के लिए कि संख्या "जंगली" (transcendental) है, गणितज्ञों ने एक क्लासिक रणनीति का उपयोग किया: विरोधाभास द्वारा प्रमाण (Proof by Contradiction)।

जाल (The Trap): वे शुरुआत में इसके विपरीत सच होने का नाटक करते हैं। वे कहते हैं, "मान लीजिए कि हमारी संख्या, $\alpha^\beta$ , वास्तव में एक 'उबाऊ' बीजीय संख्या है।"
निर्माण (सहायक फलन - The Auxiliary Function): संख्या को झूठ पकड़ने के लिए, वे एक विशेष गणितीय मशीन बनाते हैं जिसे सहायक फलन (Auxiliary Function) कहा जाता है।
- उपमा: कल्पना कीजिए कि आप यह सिद्ध करने की कोशिश कर रहे हैं कि संदिग्ध दोषी है। आप एक विशेष जाल (फलन) बनाते हैं जो इस तरह से डिज़ाइन किया गया है कि यदि संदिग्ध निर्दोष है, तो वह विशिष्ट स्थानों पर शून्य होगा।
- वे सीगल के लेम्मा (Siegel's Lemma) नामक उपकरण का उपयोग करते हैं ताकि इस मशीन के लिए सही "सामग्री" (गुणांक) मिल सकें। सीगल का लेम्मा एक जादुई रेसिपी बुक की तरह है जो गारंटी देता है कि आप अपनी विशिष्ट आवश्यकताओं के अनुरूप एक मशीन बनाने के लिए छोटे, पूर्णांक सामग्री पा सकते हैं।
सिक्के के दो पहलू:
- बीजीय पक्ष (The Algebraic Side): यदि संख्या बीजीय होती, तो यह मशीन स्वयं एक "उबाऊ" संख्या होती। क्योंकि यह पूर्णांकों से बनी है, यह बहुत छोटी नहीं हो सकती। इसका एक "न्यूनतम आकार" (lower bound) होता है।
- विश्लेषणात्मक पक्ष (The Analytic Side): जटिल विश्लेषण (complex analysis - काल्पनिक संख्याओं के साथ कैलकुलस) का उपयोग करते हुए, वे दिखाते हैं कि यह मशीन वास्तव में अविश्वसनीय रूप से छोटी हो जाती है जब वे मापदंडों (parameters) को बदलते हैं। यह उस "न्यूनतम आकार" के नियम की तुलना में बहुत तेज़ी से सिकुड़ती है।
विस्फोट (The Explosion): यहाँ विरोधाभास है। मशीन को एक ही समय में बड़ा (बीजीय नियमों के कारण) और बहुत छोटा (कैलकुलस नियमों के कारण) होने के लिए मजबूर किया जाता है।
- उपमा: यह एक जासूस द्वारा यह सिद्ध करने जैसा है कि संदिग्ध एक ही समय में दो स्थानों पर मौजूद था। संदिग्ध (संख्या) एक साथ "उबाऊ" और "जंगली" नहीं हो सकता। इसलिए, प्रारंभिक धारणा (कि वह उबाऊ था) गलत होनी चाहिए। संख्या जंगली होनी चाहिए।

कंप्यूटर चुनौती: "छेद" को ठीक करना

इस शोध पत्र का सबसे दिलचस्प हिस्सा यह है कि उन्होंने कंप्यूटर की कठोरता को कैसे संभाला।

मूल 1934 के प्रमाण में, गणितज्ञों ने एक फलन का उपयोग किया जिसमें कुछ बिंदुओं पर "छेद" (singularities) थे। कागज़ पर, वे बस कह देंगे, "हम उन छेदों से बच जाएंगे," या "छेद एक सीमा (limit) के कारण गायब हो जाता है।"

लेकिन एक कंप्यूटर को "छेद" पसंद नहीं हैं। उसे "बस बचना" पसंद नहीं है। यदि किसी बिंदु पर एक फलन अपरिभाषित है, तो कंप्यूटर क्रैश हो जाता है।

लेखकों को अविश्वसनीय रूप से चतुर होना पड़ा। उन्होंने उस फलन को लिया जिसमें छेद थे और उसे पैच (patch) किया।

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

यह क्यों मायने रखता है?

आप पूछ सकते हैं, "90 साल पहले सिद्ध हो चुके प्रमेय को सिद्ध करने में महीनों क्यों बिताएं?"

विश्वास: जटिल गणित के युग में, एक कंप्यूटर द्वारा प्रमाण को सत्यापित करने से सभी संदेह समाप्त हो जाते हैं। यह अंतिम "चेकमेट" है।
गणित का पुस्तकालय: उन्होंने इस प्रमाण को Mathlib में जोड़ा, जो सत्यापित गणित का एक विशाल ओपन-सोर्स पुस्तकालय है। अब, अन्य गणितज्ञ और कंप्यूटर बुनियादी बातों को फिर से सत्यापित किए बिना और भी अधिक जटिल प्रमाण बनाने के लिए इस परिणाम का उपयोग कर सकते हैं।
भविष्य के उपकरण: इसे औपचारिक रूप देकर, वे भविष्य में कंप्यूटरों को और भी कठिन समस्याओं को हल करने में मदद करने का मार्ग प्रशस्त कर रहे हैं, जैसे नए अतीन्द्रिय (transcendental) नंबरों को खोजना या जटिल लघुगणक (logarithms) की स्वतंत्रता को सत्यापित करना।

संक्षेप में

यह शोध पत्र एक शानदार, 90 साल पुराने गणितीय जासूसी कहानी को एक त्रुटिहीन, कंप्यूटर-पठनीय स्क्रिप्ट के रूप में फिर से लिखने की कहानी है। उन्होंने एक डिजिटल जाल बनाया, एक संख्या को तार्किक विरोधाभास में पकड़ा, और एक बार फिर सिद्ध किया कि संख्याओं के कुछ संयोजन वास्तव में "जंगली" और अतीन्द्रिय हैं। यह मानव तर्क और मशीन की सटीकता के मिलन की विजय है।

यहाँ मिचायल करातारकिस और फ्रीक वीडिक के शोध पत्र "ए फॉर्मलाइजेशन ऑफ द गेलफ़ोंड-स्नाइडर थ्योरम" का विस्तृत तकनीकी सारांश दिया गया है।

1. समस्या विवरण (Problem Statement)

यह शोध पत्र लीन 4 (Lean 4) प्रूफ़ असिस्टेंट और मैथलिब (Mathlib) लाइब्रेरी के भीतर हिल्बर्ट की सातवीं समस्या और उसके समाधान, गेलफ़ोंड-स्नाइडर प्रमेय (Gelfond-Schneider theorem) के औपचारिककरण (formalization) को संबोधित करता है।

प्रमेय: यदि $\alpha$ और $\beta$ बीजगणितीय संख्याएँ (algebraic numbers) हैं जहाँ $\alpha \notin \{0, 1\}$ और $\beta$ अपरिमेय (irrational) है, तो $\alpha^\beta$ एक ट्रांसेंडेंटल (transcendental) संख्या है।
संदर्भ: जबकि $e$ और $\pi$ जैसे विशिष्ट स्थिरांकों की ट्रांसेंडेंस (transcendence) को औपचारिक रूप दिया जा चुका है, गेलफ़ोंड-स्नाइडर प्रमेय बीजगणितीय संख्याओं के बीच घातांकीय संबंधों (exponential relationships) से जुड़े एक गहरे परिणाम का प्रतिनिधित्व करता है। इस कार्य से पूर्व, किसी भी थ्योरम प्रूवर में इस प्रमेय का औपचारिककरण मौजूद नहीं था।
लक्ष्य: प्रमेय के पूर्ण, मशीन-चेक्ड प्रमाण का निर्माण करना, जिसमें आवश्यक बीजगणितीय और विश्लेषणात्मक यंत्र (machinery) शामिल हों, और गेलफ़ोंड-स्नाइडर स्थिरांक ( $\sqrt{2}^{\sqrt{2}}$ ) की ट्रांसेंडेंस को सत्यापित करना।

2. कार्यप्रणाली (Methodology)

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

अ. बीजगणितीय संख्या सिद्धांत के आधार (Algebraic Number Theory Foundations)

बीजगणितीय संख्या का "हाउस" (The "House" of an Algebraic Number): लेखकों ने एक बीजगणितीय संख्या $\alpha$ $α$ के "हाउस" की अवधारणा को औपचारिक रूप दिया, जिसे उसके संयुग्मियों (conjugates) के अधिकतम मापांक (maximum modulus) के रूप में परिभाषित किया गया है ( $|\alpha| = \max_i |\sigma_i(\alpha)|$ $∣ α ∣ = max_{i} ∣ σ_{i} (α) ∣$ )।
- तकनीकी चुनौती: बहुपद मूलों (polynomial roots - unordered sets) का उपयोग करने वाले प्रारंभिक प्रयासों ने बीजगणितीय सीमाओं को कठिन बना दिया था। लेखकों ने एक कैनोनिकल एम्बेडिंग (canonical embedding) दृष्टिकोण ( $K \to \prod_{\sigma} \mathbb{C}$ ) अपनाया, जिसमें 'हाउस' को एक बानाच अल्जेब्रा (Banach algebra) पर $L_\infty$ -नॉर्म के रूप में माना गया। इसने मल्टीप्लिकेटिविटी और त्रिकोण असमानता (triangle inequality) के प्रमाणों को सरल बनाने के लिए मैथलिब के नॉर्मेड स्पेस API का लाभ उठाया।
नंबर फील्ड्स के लिए सीगल का लेम्मा (Siegel's Lemma for Number Fields): प्रमाण के लिए एक सहायक फलन (auxiliary function) के लिए छोटे बीजगणितीय पूर्णांक गुणांकों को खोजने की आवश्यकता होती है।
- लेखकों ने एक नंबर फील्ड $K$ के पूर्णांक रिंग $\mathcal{O}_K$ के लिए सीगल के लेम्मा के एक सामान्यीकृत संस्करण को औपचारिक रूप दिया।
- तकनीक: उन्होंने एक "डेसेंट तर्क" (descent argument) का उपयोग किया, जिसने $\mathcal{O}_K$ पर रैखिक प्रणाली को $\mathbb{Z}$ पर एक बड़ी प्रणाली में बदल दिया, मानक पूर्णांक सीगल लेम्मा लागू किया, और समाधान को वापस $\mathcal{O}_K$ पर लाया।

ब. विश्लेषणात्मक कोर और सहायक फलन (Analytic Core and Auxiliary Functions)

प्रमाण विरोधाभास (contradiction) द्वारा आगे बढ़ता है, यह मानते हुए कि $\alpha^\beta$ बीजगणितीय है, और एक सहायक फलन $R(z)$ का निर्माण करता है जो विशिष्ट बिंदुओं पर उच्च कोटि (high order) पर शून्य होता है।

$R(z)$ का निर्माण: इसे घातांकीयों के एक रैखिक संयोजन के रूप में परिभाषित किया गया है $R(x) = \sum \eta_i e^{\rho_i x}$ । गुणांक $\eta_i$ को उस शर्त से प्राप्त एक होमोजेनियस लीनियर सिस्टम को हल करके निर्धारित किया जाता है जहाँ $R(z)$ , पूर्णांक बिंदुओं पर उच्च बहुलता (high multiplicity) के साथ शून्य होता है।
वैश्विक फलन $S(z)$ (The Global Function $S(z)$ ): एक महत्वपूर्ण तकनीकी बाधा सहायक फलन $S(z)$ $S (z)$ को औपचारिक रूप देना थी, जिसमें $R(z)$ $R (z)$ को $(z-k)^r$ $(z - k)^{r}$ जैसे पदों द्वारा विभाजित किया जाता है।
- चुनौती: शास्त्रीय विश्लेषण में, $S(z)$ को हटाने योग्य विलक्षणताओं (removable singularities) वाले मेरोमॉर्फिक (meromorphic) फलन के रूप में माना जाता है। डिपेंडेंट टाइप थ्योरी (लीन) में, आंशिक फलन (मेरोमॉर्फिक फलन) को संभालना कठिन है क्योंकि उन्हें डोमेन को ट्रैक करने और हर लेम्मा में पोल्स (poles) से बचने की आवश्यकता होती है।
- समाधान: लेखकों ने $S(z)$ को एक पूर्ण, पीसवाइज होलोमॉर्फिक फलन (total, piecewise holomorphic function) के रूप में निर्मित किया। उन्होंने स्थानीय पावर सीरीज़ विस्तार (पैचिंग) का उपयोग करके विलक्षण बिंदुओं पर फलन के मानों को स्पष्ट रूप से परिभाषित किया और सिद्ध किया कि ये स्थानीय परिभाषाएँ मिलकर एक वैश्विक विश्लेषणात्मक फलन बनाती हैं। इससे आंशिकता (partiality) और ऑप्शन प्रकारों की जटिलता से बचाव हुआ।

स. विरोधाभास (The Contradiction)

प्रमाण एक विशिष्ट मान $\rho$ (एक $R(z)$ का सामान्यीकृत व्युत्पन्न) को दो तरह से सीमित करके विरोधाभास प्राप्त करता है:

बीजगणितीय निचली सीमा (Algebraic Lower Bound): चूंकि $\rho$ एक गैर-शून्य बीजगणितीय संख्या है, इसलिए इसके नॉर्म $|N(\rho)|$ को नीचे से सीमित किया जाना चाहिए (विशेष रूप से, डिनोमिनेटरों को हटाने के बाद $|N(\rho)| \geq 1$ )।
विश्लेषणात्मक ऊपरी सीमा (Analytic Upper Bound): एक बड़े कंटूर (contour) पर कॉची के इंटीग्रल फॉर्मूला का उपयोग करते हुए, लेखकों ने $|\rho|$ को ऊपर से सीमित किया।
परिणाम: पर्याप्त बड़े मापदंडों के लिए, विश्लेषणात्मक ऊपरी सीमा सुपर-एक्सपोनेंशियल रूप से घटती है, जबकि बीजगणितीय निचली सीमा स्थिर रहती है या धीमी गति से बढ़ती है, जिससे एक विरोधाभास उत्पन्न होता है ( $|N(\rho)| < 1$ )।

3. प्रमुख योगदान (Key Contributions)

प्रथम औपचारिककरण: यह किसी भी थ्योरम प्रूवर में गेलफ़ोंड-स्नाइडर प्रमेय का पहला औपचारिककरण है।
मैथलिब विस्तार (Mathlib Extensions): इस कार्य ने मैथलिब में महत्वपूर्ण नई परिभाषाएँ और लेम्मा जोड़े, जिनमें शामिल हैं:
- कैनोनिकल एम्बेडिंग्स के माध्यम से बीजगणितीय संख्या का "हाउस"।
- नंबर फील्ड्स में बीजगणितीय पूर्णांकों के लिए सामान्यीकृत सीगल का लेम्मा।
- हटाने योग्य विलक्षणताओं वाले अभिव्यक्तियों से पूर्ण विश्लेषणात्मक फलनों के निर्माण की तकनीकें।
स्पष्ट स्थिरांक प्रबंधन (Explicit Constant Management): शास्त्रीय प्रमाणों के विपरीत जो $O(\cdot)$ नोटेशन का उपयोग करते हैं, इस औपचारिककरण ने स्पष्ट रूप से स्थिरांकों के एक अनुक्रम ( $c_1$ से $c_{15}$ तक) को ट्रैक किया जो नंबर फील्ड की डिग्री और ज्यामितीय गुणों पर निर्भर करते हैं। इस अंतिम विरोधाभास को कठोरता से सिद्ध करने के लिए इस स्पष्ट ट्रैकिंग का होना आवश्यक था।
स्थिरांकों का सत्यापन: इस ढांचे का उपयोग $\sqrt{2}^{\sqrt{2}}$ की ट्रांसेंडेंस को औपचारिक रूप से सिद्ध करने के लिए किया गया था।

4. परिणाम (Results)

सिद्ध प्रमेय: लीन कोड सफलतापूर्वक सत्यापित करता है कि बीजगणितीय $\alpha \notin \{0, 1\}$ और अपरिमेय बीजगणितीय $\beta$ के लिए, $\alpha^\beta$ ट्रांसेंडेंटल है।
विशिष्ट अनुप्रयोग: औपचारिककरण ने पुष्टि की कि $\sqrt{2}^{\sqrt{2}}$ ट्रांसेंडेंटल है।
कोड उपलब्धता: सोर्स कोड मैथलिब की एक ब्रांच में एकीकृत है और सार्वजनिक रूप से उपलब्ध है।

5. महत्व और भविष्य का कार्य (Significance and Future Work)

क्षेत्रों को जोड़ना: यह कार्य आधुनिक प्रमाण सहायकों (proof assistants) की क्षमता को प्रदर्शित करता है कि वे बीजगणितीय संख्या सिद्धांत और जटिल विश्लेषण को जोड़ने वाले गहरे परिणामों को संभाल सकते हैं।
उन्नत प्रमेयों के लिए आधार: यह औपचारिककरण अधिक जटिल परिणामों के लिए आधार तैयार करता है:
- बेकर का प्रमेय (Baker's Theorem): लॉगारिदम के लीनियर फॉर्म्स में सामान्यीकरण।
- p-एडिक गेलफ़ोंड-स्नाइडर (p-adic Gelfond-Schneider): विश्लेषणात्मक लेम्मा को p-एडिक विश्लेषण (स्निरेलमैन इंटीग्रल्स) में अनुकूलित करना।
- स्नाइडर-लैंग प्रमेय (Schneider-Lang Theorem): बीजगणितीय अवकल समीकरणों को संतुष्ट करने वाले मेरोमॉर्फिक फलनों तक ट्रांसेंडेंस परिणामों का विस्तार करना।
- इलिप्टिक कर्व्स (Elliptic Curves): वीयेरस्ट्रॉस $\wp$ -फलन के लिए फ्रेमवर्क का सामान्यीकरण।
निर्णय प्रक्रियाएं (Decision Procedures): स्थिरांकों की स्पष्ट प्रकृति अंतराल अंकगणित (interval arithmetic) का उपयोग करके विशिष्ट वर्गों के ट्रांसेंडेंटल नंबरों के लिए स्वचालित निर्णय प्रक्रियाओं को लागू करने की क्षमता का सुझाव देती है।
शैनुएल का अनुमान (Schanuel's Conjecture): यह कार्य शैनुएल के अनुमान के परिणामों को सशर्त रूप से सत्यापित करने के लिए आवश्यक तथ्यों के पुस्तकालय में योगदान देता है।

संक्षेप में, यह शोध पत्र औपचारिक गणित में एक प्रमुख मील का पत्थर है, जो एक सदी पुराने, गैर-तुच्छ प्रमाण को सफलतापूर्वक मशीनाइज करता है जिसके लिए रचनात्मक प्रकार-सैद्धांतिक ढांचे (constructive type-theoretic framework) के भीतर विश्लेषणात्मक फलनों को संभालने के लिए महत्वपूर्ण नवाचार की आवश्यकता थी।