💻 computer science

From the Dirichlet Integral to Lobachevsky's Formula: A Formalization in Lean 4

यह शोध पत्र डिरिचलेट इंटीग्रल (Dirichlet integral) और लोबाचेव्स्की के सूत्र (Lobachevsky's formula) सहित इसके अनुप्रयोगों का लीन 4 (Lean 4) में एक औपचारिककरण प्रस्तुत करता है, जिसमें सशर्त अभिसरण (conditional convergence) को कठोरता से संभालने और विभिन्न त्रिकोणमितीय इंटीग्रल पहचानों को व्युत्पन्न करने के लिए पूर्णतः समाकलनीय वर्गाकार sinc फलन (absolutely integrable squared sinc function) और कोसाइन बहुपदों के घनत्व (density of cosine polynomials) का उपयोग करने वाली एक रणनीति नियोजित की गई है।

मूल लेखक: Daniel Goldberg, Antoine Vinciguerra

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

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

CC BY 4.0

मूल लेखक: Daniel Goldberg, Antoine Vinciguerra

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

गणित के विशाल परिदृश्य में, एक शांत कोना समर्पित है इस बात के अध्ययन के लिए कि चीजें समय के साथ कैसे जुड़ती हैं, विशेष रूप से तब जब वे आगे-पीछे डगमगाती हैं। यह वास्तविक विश्लेषण (real analysis) का क्षेत्र है, जहाँ गणितज्ञ उन फलनों (functions) के व्यवहार की जांच करते हैं जो निरंतर बदलते रहते हैं। इस क्षेत्र में एक प्रसिद्ध पहेली है जो एक विशिष्ट वक्र (curve) के बारे में है जो एक लहर की तरह ऊपर-नीचे होता है, और जैसे-जैसे यह अनंत की ओर बढ़ता है, यह छोटा और छोटा होता जाता है। प्रश्न सरल है लेकिन हल करने में कठिन है: यदि आप इस डगमगाते वक्र के नीचे का क्षेत्रफल उस शुरुआती बिंदु से लेकर सबसे दूर के बिंदु तक जोड़ते हैं जिसकी आप कल्पना कर सकते हैं, तो आपको कुल योग क्या प्राप्त होगा? एक सदी से अधिक समय से, गणितज्ञों को इसका उत्तर ज्ञात है, लेकिन बिना किसी छिपे हुए अनुमान के इसे कठोरता से सिद्ध करना हमेशा एक नाजुक कार्य रहा है। ऐसा इसलिए है क्योंकि यह वक्र मानक जोड़ के नियमों को सीधे लागू करने के लिए पर्याप्त तेजी से स्थिर नहीं होता है; यह एक परिमित योग (finite sum) तक पहुँचने के लिए धनात्मक और ऋणात्मक क्षेत्रों के सटीक विलोपन (cancellation) पर निर्भर करता है। इस व्यवहार को समझना न केवल शुद्ध गणित के लिए, बल्कि उस तकनीक के लिए भी महत्वपूर्ण है जो आधुनिक संचार का आधार है, क्योंकि इन्हीं डगमगाते पैटर्न का उपयोग कच्चे डेटा से संकेतों और छवियों को पुनर्गठित करने के लिए किया जाता है।

हाल ही में, डैनियल गोल्डबर्ग और एंटोनी विन्सिगुएरा ने एक कंप्यूटर प्रोग्राम का उपयोग करके इस शास्त्रीय समस्या को हल करने का निर्णय लिया, जिसे पूर्ण निश्चितता के साथ गणितीय प्रमाणों की जाँच करने के लिए डिज़ाइन किया गया है। उन्होंने केवल समाधान नहीं लिखा; उन्होंने 'लीन 4' (Lean 4) नामक एक सॉफ़्टवेयर सिस्टम के भीतर एक पूर्ण, चरण-दर-चरण तार्किक तर्क का निर्माण किया, जो एक अथक लेखा परीक्षक की तरह कार्य करता है जो किसी भी कदम को तब तक स्वीकार करने से इनकार करता है जब तक कि वह तर्क के नियमों द्वारा न्यायसंगत न हो। उनका लक्ष्य डिरिचलेट इंटीग्रल (Dirichlet integral) को औपचारिक रूप देना था, जो उस विशिष्ट डगमगाते क्षेत्रफल की गणना को नाम दिया गया है, और यह दिखाना था कि यह आवधिक फलनों (periodic functions) के व्यापक नियमों से कैसे जुड़ता है। उनके सामने चुनौती यह थी कि कंप्यूटर द्वारा क्षेत्रफल की गणना करने का मानक तरीका, जिसे लेबेग इंटीग्रल (Lebesgue integral) कहा जाता है, इस विशेष वक्र को सीधे संसाधित नहीं कर सकता क्योंकि इसके डगमगाते हिस्सों का कुल आकार अनंत है, भले ही शुद्ध क्षेत्रफल परिमित हो। इस समस्या से बचने के लिए, शोधकर्ताओं को एक चतुर मार्ग खोजना पड़ा जिसने अनंत की समस्या से बचते हुए भी सही उत्तर तक पहुँचाया।

मूल डगमगाते वक्र को सीधे कंप्यूटर के सामने प्रस्तुत करने के बजाय, टीम ने पहले इसके एक संशोधित संस्करण की ओर देखा जहाँ वक्र का वर्ग (square) किया गया था। यह वर्गाकार संस्करण बहुत अधिक सुव्यवस्थित व्यवहार करता है; इसका कुल क्षेत्रफल परिमित और सुव्यवस्थित है, जिससे कंप्यूटर मानक विधियों का उपयोग करके इसकी गणना कर सकता है। शोधकर्ताओं ने मूल डगमगाते वक्र के नीचे के क्षेत्रफल और इस वर्गाकार संस्करण के नीचे के क्षेत्रफल के बीच एक विशिष्ट संबंध को सिद्ध किया। वर्गाकार वक्र के क्षेत्रफल की गणना पहले करके, वे उस परिणाम को मूल समस्या पर गणितीय रूप से वापस स्थानांतरित कर सके। इस दृष्टिकोण ने उन्हें 'कंडीशनल कन्वर्जेंस' (conditional convergence) की कठिनाइयों से बचने और इस प्रसिद्ध परिणाम तक पहुँचने में मदद की कि कुल क्षेत्रफल ठीक से पाई (pi) का आधा है। यह कोई अनुमान या सिमुलेशन नहीं था; यह एक कठोर प्रमाण था कि क्षेत्रफल का सीमांत (limit), जैसे-जैसे सीमा दूर जाती है, इस विशिष्ट मान की ओर अभिसरित (converge) होता है।

मुख्य पहेली को हल करने के बाद, टीम ने अपने नए उपकरणों का उपयोग यह पता लगाने के लिए किया कि इससे और क्या निकाला जा सकता है। उन्होंने दिखाया कि यह इंटीग्रल कैसे एक फिल्टर के रूप में कार्य करता है जो एक चिकने, निरंतर तरंग को एक तीक्ष्ण, चरण-नुमा उछाल (step-like jump) में बदल सकता है, जो एक व्यवहार है जो डिजिटल संकेतों के प्रसंस्करण के लिए मौलिक है। उन्होंने उत्पादों के involving इन डगमगाते फलनों के अन्य पहचानों (identities) का एक संग्रह भी खोजा और सिद्ध किया, जो यह दिखाता है कि विभिन्न आवृत्तियाँ (frequencies) आपस में गुणा होने पर कैसे परस्पर क्रिया करती हैं। ये परिणाम केवल अमूर्त जिज्ञासाएँ नहीं हैं; वे यह समझने के लिए गणितीय आधार प्रदान करते हैं कि नमूनों (samples) से संकेतों का पुनर्निर्माण कैसे किया जा सकता है, जो डिजिटल ऑडियो और इमेज प्रोसेसिंग में उपयोग किए जाने वाले शैनन सैंपलिंग प्रमेय (Shannon sampling theorem) की एक केंद्रीय अवधारणा है। शोधकर्ताओं ने प्रदर्शित किया कि इन विशिष्ट इंटीग्रल के व्यवहार को समझकर, एक सटीक सूत्र प्राप्त किया जा सकता है कि कैसे विभिन्न तरंग पैटर्न आपस में मिलते हैं और एक-दूसरे को रद्द करते हैं।

उनका अंतिम और शायद सबसे आश्चर्यजनक उपलब्धि निकोलाई लोबाचेवस्की द्वारा खोजा गया एक सूत्र था, जो एक ऐसे गणितज्ञ हैं जिन्हें गैर-यूक्लिडियन ज्यामिति के उनके कार्य के लिए जाना जाता है। लोबाचेवस्की ने एक नियम खोजा था जो एक डगमगाते वक्र को एक दोहराते हुए पैटर्न के साथ गुणा करने के नीचे के क्षेत्रफल की गणना करने की अनुमति देता है, जिसे उस पैटर्न के एक छोटे से हिस्से को देखकर किया जा सकता है। शोधकर्ताओं ने सिद्ध किया कि यह नियम किसी भी निरंतर, दोहराने वाले फलन के लिए सत्य है जिसमें एक विशिष्ट प्रकार की समरूपता (symmetry) होती है, और कंप्यूटर का उपयोग करके यह सत्यापित किया कि डगमगाते हुए हिस्सों के अनंत योग को एक लघु अंतराल (interval) की सरल गणना में कैसे बदला जा सकता है। उन्होंने इसे यह दिखाकर हासिल किया कि ऐसे किसी भी दोहराने वाले फलन को सरल कोसाइन तरंगों (cosine waves) के योग द्वारा निकटता से अनुमानित किया जा सकता है, और चूंकि यह नियम प्रत्येक व्यक्तिगत तरंग के लिए काम करता है, इसलिए यह पूरे फलन के लिए भी काम करेगा। यह एक सामान्य पहचान का मशीन-चेक्ड प्रमाण प्रदान करता है जो पहले केवल मानवीय अंतर्ज्ञान और पारंपरिक कागज-पेंसिल विधियों के माध्यम से समझी गई थी।

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

तकनीकी सारांश: डिरिचलेट इंटीग्रल से लोबाचेव्स्की के फॉर्मूला तक

समस्या विवरण
यह शोध पत्र Mathlib लाइब्रेरी का उपयोग करते हुए Lean 4 प्रूफ़ असिस्टेंट के भीतर डिरिचलेट इंटीग्रल, $\lim_{T \to +\infty} \int_0^T \frac{\sin t}{t} dt = \frac{\pi}{2}$ , के औपचारिकीकरण (formalization) को संबोधित करता है। प्राथमिक चुनौती इंटीग्रेंड (integrand) की प्रकृति है, जो कि $\text{sinc}$ फलन ( $\sin t / t$ ) है, जो धनात्मक अर्ध-रेखा पर लेबेग समाकलनीय (Lebesgue integrable) नहीं है क्योंकि यह पूर्णतः समाकलनीय (absolutely integrable) नहीं है। मानक गणितीय अभ्यास में, $\int_0^{+\infty} \text{sinc}(t) dt$ के लिए $\text{sinc}$ नोटेशन का ढीले ढंग से उपयोग किया जाता है, लेकिन Mathlib जैसे औपचारिक प्रणालियों में, गैर-समाकलनीय फलन के बोchner इंटीग्रल को शून्य के रूप में परिभाषित किया जाता है। फलस्वरूप, इंटीग्रल के मान का सीधा औपचारिकीकरण असंभव है; इसके बजाय, समस्या को ट्रंकेटेड (truncated) इंटीग्रल्स के अभिसरण (convergence) के रूप में फ्रेम किया जाना चाहिए। "फेनमैन ट्रिक" (एक घातांक कारक $e^{-at}$ पेश करना और $a \to 0^+$ की सीमा लेना) पर आधारित शास्त्रीय प्रमाणों को औपचारिक बाधाओं का सामना करना पड़ता है: सीमाओं के आदान-प्रदान को न्यायसंगत बनाने के लिए यूनिफॉर्म टेल एस्टीमेट्स (uniform tail estimates) की आवश्यकता होती है जो सशर्त अभिसरण (conditional convergence) के औपचारिक ढांचे के भीतर समन्वय करने में कठिन हैं।

कार्यप्रणाली
लेखक एक ऐसी प्रमाण रणनीति अपनाते हैं जो $\text{sinc}^2(t)$ के पूर्णतः समाकलनीय वर्ग $\text{sinc}^2$ के माध्यम से मार्ग बनाकर सशर्त अभिसरण की कठिनाइयों को दरकिनार करती है।

$\text{sinc}^2$ का मूल्यांकन: औपचारिकीकरण पहले यह स्थापित करता है कि $\text{sinc}^2(t)$ , $(0, \infty)$ पर लेबेग समाकलनीय है। यह $I(x) = \int_0^\infty e^{-xt} \text{sinc}^2(t) dt$ नामक एक सहायक फलन पेश करके $\int_0^\infty \text{sinc}^2(t) dt$ का मूल्यांकन करता है। इंटीग्रल साइन के तहत दो बार अवकलन करके, लेखक $I(x)$ के लिए एक क्लोज्ड-फॉर्म अभिव्यक्ति प्राप्त करते हैं और डोमिनेटेड कन्वर्जेंस थ्योरम (DCT) का उपयोग करके $x \to 0^+$ के लिए सीमा लेते हैं, जो यहाँ मान्य है क्योंकि $\text{sinc}^2$ पूर्णतः समाकलनीय है।
डिरिचलेट इंटीग्रल की प्राप्ति: डिरिचलेट इंटीग्रल का मान $\text{sinc}$ और $\text{sinc}^2$ के ट्रंकेटेड इंटीग्रल्स के बीच एक पहचान (identity) के माध्यम से प्राप्त किया जाता है। इंटीग्रेशन बाय पार्ट्स का उपयोग करते हुए, लेखक सिद्ध करते हैं कि किसी भी $T > 0$ के लिए:
$\int_0^T \text{sinc}(t) dt = \int_0^{T/2} \text{sinc}^2(t) dt + \frac{T}{2}\text{sinc}^2\left(\frac{T}{2}\right)$
जैसे $T \to \infty$ , बाउंड्री टर्म शून्य हो जाता है, जिससे $\text{sinc}$ इंटीग्रल की सीमा को $\text{sinc}^2$ इंटीग्रल की सीमा के बराबर रखा जा सकता है।
औपचारिक संरचना: औपचारिकीकरण लेबेग इंटीग्रेशन (जो $\text{sinc}^2$ के लिए उपयोग किया जाता है) और ट्रंकेटेड इंटीग्रल्स के सीमा (limit) (जो $\text{sinc}$ के लिए उपयोग किया जाता है) की अवधारणाओं को सख्ती से अलग करता है। अभिसरण को Lean के Tendsto और atTop फिल्टर्स का उपयोग करके व्यक्त किया गया है।

प्रमुख योगदान और परिणाम
शोध पत्र वास्तविक विश्लेषण (real analysis) के तीन परस्पर जुड़े परिवारों के औपचारिकीकरण को प्रस्तुत करता है:

डिरिचलेट इंटीग्रल: लेखक एक मशीन-चेक्ड प्रमाण प्रदान करते हैं कि $\text{sinc}(t)$ के ट्रंकेटेड इंटीग्रल्स की सीमा $\pi/2$ की ओर अभिसरित होती है। यह स्वयं गैर-समाकलनीय फलन के लेबेग इंटीग्रल का आह्वान किए बिना प्राप्त किया गया है।
डिरिचलेट कटऑफ और हीविसाइड लिमिट: औपचारिकीकरण सामान्यीकृत प्रिमिटिव $D(x) = \frac{1}{2} + \frac{1}{\pi}\int_0^x \text{sinc}(t) dt$ के हीविसाइड फलन की ओर अभिसरण को व्युत्पन्न करता है। विशेष रूप से, यह सिद्ध करता है कि $\lim_{R \to \infty} D(Rx) = H(x)$ पॉइंटवाइज (pointwise)। इस परिणाम को एक इंटीग्रल कटऑफ फॉर्मूला में विस्तारित किया गया है, जो दिखाता है कि कैसे $D(R(a-t))$ , समाकलनीय फलनों के लिए एक अनुमानित पहचान (approximate identity) के रूप में कार्य करता है।
त्रिकोणमितीय इंटीग्रल पहचान: $\text{sinc}^2$ $sinc^{2}$ इंटीग्रल के मूल्यांकन का उपयोग करते हुए, लेखक कई द्विघात (quadratic) और द्विपद (bilinear) पहचानों को औपचारिक रूप देते हैं, जिनमें शामिल हैं:
- $\int_0^\infty \left(\frac{\sin(at)}{t}\right)^2 dt = \frac{\pi |a|}{2}$
- $\int_0^\infty \frac{1-\cos(at)}{t^2} dt = \frac{\pi |a|}{2}$
- $\int_0^\infty \text{sinc}(at)\text{sinc}(bt) dt = \frac{\pi}{2 \max(a,b)}$
लोबाचेव्स्की का इंटीग्रल फॉर्मूला: शोध पत्र निरंतर आवधिक फलनों $f$ के लिए लोबाचेव्स्की के फॉर्मूला को औपचारिक रूप देता है जो $f(x+\pi)=f(x)$ और $f(\pi-x)=f(x)$ की शर्तों को पूरा करते हैं। प्रमेय बताता है:
$\int_0^\infty \text{sinc}^2(x)f(x) dx = \int_0^{\pi/2} f(x) dx$
प्रमाण एडिटिव सर्कल $\mathbb{R}/\pi\mathbb{Z}$ पर निरंतर फलनों के स्पेस में कोसाइन पॉलिनोमिअल्स के घनत्व (density) का उपयोग करता है (एक परिणाम जो Mathlib के फूरियर विश्लेषण में उपलब्ध है)। लेखक पहले व्यक्तिगत कोसाइन मोड के लिए पहचान को सत्यापित करते हैं और फिर यूनिफॉर्म एप्रोक्सिमेशन और विरोधाभास तर्क (contradiction argument) के माध्यम से इसे सामान्य निरंतर फलनों तक विस्तारित करते हैं।

महत्व और दावे
लेखक दावा करते हैं कि यह कार्य एक प्रूफ़ असिस्टेंट में लोबाचेव्स्की के इंटीग्रल फॉर्मूला का पहला औपचारिकीकरण प्रदान करता है। जबकि डिरिचलेट इंटीग्रल को पहले फ्युबिनी के प्रमेय (Fubini's theorem) और $1/x$ के इंटीग्रल प्रतिनिधित्व का उपयोग करते हुए Isabelle/HOL (Avigad et al. द्वारा) में औपचारिक रूप दिया गया था, इस शोध पत्र का योगदान $\text{sinc}^2$ के माध्यम से इसके विशिष्ट मार्ग और लोबाचेव्स्की के फॉर्मूला पर इसके अनुप्रयोग में निहित है।

इस कार्य का महत्व दोतरफा है:

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

शोध पत्र यह नोट करते हुए समाप्त होता है कि विकसित इंफ्रास्ट्रक्चर भविष्य के विस्तारों का समर्थन करता है, जैसे कि $\text{sinc}$ फलन की उच्च सम घातों (higher even powers) के लिए लोबाचेव्स्की-प्रकार के फॉर्मूला और लाप्लास ट्रांसफॉर्म थ्योरी के अनुप्रयोग, हालांकि इन्हें पूर्ण कार्य के बजाय भविष्य की दिशाओं के रूप में प्रस्तुत किया गया है।

इसी तरह के और पेपर