🔢 mathematics

Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case

यह शोध पत्र लीन 4 (Lean 4) प्रूफ़ असिस्टेंट और मैथलिब (Mathlib) का उपयोग करते हुए समतल में शास्त्रीय समक्षेत्रीय असमानता (isoperimetric inequality) का एक औपचारिक सत्यापन प्रस्तुत करता है, जो एडोल्फ हर्ट्ज़ के विश्लेषणात्मक दृष्टिकोण का अनुसरण करता है ताकि यह सिद्ध किया जा सके कि दिए गए परिधि वाले सभी सरल बंद वक्रों में, वृत्त अद्वितीय रूप से घेरे गए क्षेत्र को अधिकतम करता है।

मूल लेखक: Miraj Samarakkody

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

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

CC BY 4.0

मूल लेखक: Miraj Samarakkody

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

मुख्य विचार: "बाड़ और मैदान" की समस्या

कल्पना कीजिए कि आपके पास रस्सी की एक निश्चित लंबाई है (मान लीजिए 100 मीटर)। आप इस रस्सी को ज़मीन पर बिछाकर घास का एक हिस्सा घेरना चाहते हैं। आप रस्सी से एक वर्ग (square), एक त्रिभुज (triangle), एक टेढ़ी-मेढ़ी सांप जैसी आकृति, या एक आदर्श वृत्त (circle) बना सकते हैं।

प्रश्न: कौन सी आकृति आपको सबसे बड़ा घास का मैदान देगी?

उत्तर: एक वृत्त। आप अपनी रस्सी को चाहे कितनी भी तरह से घुमा लें, आप एक पूर्ण वृत्त से अधिक घास प्राप्त नहीं कर सकते। यह आइसोपेरिमेट्रिक इनइक्वलिटी (Isoperimetric Inequality) है। यह ब्रह्मांड का एक नियम है: दिए गए परिधि (perimeter) के लिए, वृत्त सबसे कुशल आकृति है।

मिशन: एक रोबोट को इसे सिद्ध करना सिखाना

इस शोध पत्र के लेखक, मिराज समरक्कोडी (Miraj Samarakkody) केवल यह कहना नहीं चाहते थे कि वृत्त सबसे अच्छा है; वे इसे एक कंप्यूटर को इतनी सटीकता से सिद्ध करना चाहते थे कि कंप्यूटर उसमें एक भी तार्किक त्रुटि न ढूंढ सके।

उन्होंने Lean 4 नामक एक टूल का उपयोग किया, जो एक अत्यंत सख्त 'रोबोट वकील' की तरह है। सामान्य गणित में, एक मानव प्रमाण (proof) एक छोटा सा कदम छोड़ सकता है क्योंकि "यह स्पष्ट है।" लेकिन Lean 4 एक ऐसे वकील की तरह है जो कहता है, "मुझे परवाह नहीं कि यह स्पष्ट है। मुझे वह सटीक नियम दिखाएं जो आपको वह कदम छोड़ने की अनुमति देता है, अन्यथा मैं आपके प्रमाण को खारिज कर दूंगा।"

लक्ष्य गणितज्ञ एडोल्फ हर्टविज़ (Adolf Hurwitz) (1902 के) द्वारा दिए गए एक प्रसिद्ध प्रमाण को कोड में अनुवादित करना था जिसे रोबोट वकील स्वीकार कर सके।

रणनीति: "संगीत" वाला दृष्टिकोण

हर्टविज़ का प्रमाण चतुर है क्योंकि यह ज्यामिति (जैसे आकृतियाँ बनाना) का उपयोग नहीं करता है। इसके बजाय, यह संगीत का उपयोग करता है।

आपकी रस्सी के घुमाव की कल्पना एक गीत के रूप में करें।

गीत (The Song): किसी भी टेढ़ी-मेढ़ी रेखा को सरल संगीत नोट्स (साइन और कोसाइन तरंगों) के मिश्रण में तोड़ा जा सकता है। इसे फूरियर सीरीज़ (Fourier Series) कहा जाता है। एक जटिल आकृति बस कई अलग-अलग नोट्स से बना एक गीत है जो एक साथ बज रहे हैं।
ध्वनि का स्तर (The Volume - Parseval's Theorem): संगीत सिद्धांत में एक नियम है जो कहता है कि गीत की कुल "तेज़ी" (ऊर्जा) प्रत्येक व्यक्तिगत नोट की तेज़ी के योग के बराबर होती है।
तुलना (The Comparison - Wirtinger's Inequality): हर्टविज़ ने आकृति की स्थिति की "तेज़ी" (loudness) की तुलना उसके बदलने की गति (speed) की "तेज़ी" से करने का एक तरीका खोजा। उन्होंने सिद्ध किया कि गति हमेशा स्थिति से अधिक "तेज़" होती है, जब तक कि वह आकृति एक पूर्ण वृत्त न हो।

दो चरणों की यात्रा

यह शोध पत्र दो मुख्य चरणों का वर्णन करता है:

चरण 1: संगीतमय लाइब्रेरी बनाना

इससे पहले कि वे बाड़ वाली समस्या को सिद्ध कर सकें, उन्हें रोबोट को संगीत सिद्धांत के नियम सिखाने थे।

ऑर्थोगोनैलिटी (Orthogonality): उन्होंने सिद्ध किया कि अलग-अलग संगीत नोट्स (जैसे एक ऊँचा C और एक नीचा G) आपस में जुड़ने पर एक-दूसरे में हस्तक्षेप नहीं करते हैं।
यूनिफॉर्म कन्वर्जेंस (Uniform Convergence): उन्होंने सिद्ध किया कि यदि आप पर्याप्त नोट्स जोड़ते हैं, तो गीत का उतार-चढ़ाव रुक जाता है और वह एक सुरीली धुन बन जाता है।
डिफरेंशिएशन (Differentiation): उन्होंने रोबोट को अनंत नोट्स से बने एक गीत का "डेरिवेटिव" (गति) निकालना सिखाया।

उपमा: यह रोबोट को कविता लिखने के लिए कहने से पहले उसके लिए एक शब्दकोश और व्याकरण की किताब बनाने जैसा है।

चरण 2: स्वयं प्रमाण

एक बार जब रोबोट संगीत के नियमों को जान गया, तो उन्होंने इसे रस्सी पर लागू किया:

रस्सी को फिर से लपेटना: उन्होंने रस्सी (लंबाई $L$ ) को लिया और उसे ठीक 24 घंटे के चक्र (0 से $2\pi$ तक) में फिट होने के लिए फैला दिया।
क्षेत्रफल का सूत्र (The Area Formula): उन्होंने एक "शूलेस फॉर्मूला" (एक बहुभुज के क्षेत्रफल की गणना करने का तरीका) का उपयोग किया ताकि आकृति को एक गणितीय समीकरण में बदला जा सके।
लेन-देन (The Trade-Off): उन्होंने AM-GM के एक बुनियादी गणितीय नियम का उपयोग करके कहा, "क्षेत्रफल, स्थिति के वर्ग और गति के वर्ग के योग द्वारा सीमित है।"
अंतिम प्रहार (The Final Blow): उन्होंने "संगीत के नियमों" (विर्टिंगर इनइक्वलिटी) का उपयोग करके दिखाया कि समीकरण का "गति वाला हिस्सा" हमेशा "स्थिति वाले हिस्से" से बड़ा होता है, जब तक कि आकृति एक वृत्त न हो।
परिणाम: उन्होंने गणना की कि आप अधिकतम क्षेत्रफल $L^2 / 4\pi$ प्राप्त कर सकते हैं। यदि आप एक वर्ग या त्रिभुज बनाने की कोशिश करते हैं, तो आप इस संख्या से कम रह जाएंगे।

अड़चनें: यह कठिन क्यों था?

आप सोच सकते हैं, "यह तो सिर्फ गणित है, कंप्यूटर के लिए कठिन क्यों है?" शोध पत्र बताता है कि कंप्यूटर में "कॉमन सेंस" (सामान्य ज्ञान) की कमी होती है।

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

निष्कर्ष

यह शोध पत्र निश्चितता (certainty) की जीत है।

गणितज्ञों के लिए: यह सिद्ध करता है कि 100 साल पुराना प्रमाण पूरी तरह से ठोस है। भले ही हमने 1902 में कोई छोटी सी बारीकी छोड़ दी हो, कंप्यूटर ने हर एक कदम की जांच की और कोई त्रुटि नहीं पाई।
भविष्य के लिए: यह दिखाता है कि हम जटिल, स्नातक स्तर के गणित को सत्यापित करने के लिए कंप्यूटर का उपयोग कर सकते हैं। यह ब्रह्मांड के सबसे महत्वपूर्ण नियमों के लिए एक "स्पेल-चेकर" रखने जैसा है।

संक्षेप में: लेखक ने एक रोबोट को किसी आकृति के "संगीत" को सुनना सिखाया, यह सिद्ध किया कि वृत्त ही एकमात्र आकृति है जो एकदम सही सुर गाती है, और यह सब एक ऐसी भाषा में किया जिस पर रोबोट बहस न कर सके।

प्रदान किए गए शोध पत्र के आधार पर, द्वि-आयामी मामले में शास्त्रीय समपरिमित (isoperimetric) असमिका के औपचारिककरण का विस्तृत तकनीकी सारांश यहाँ दिया गया है।

1. समस्या विवरण

यह शोध पत्र यूक्लिडियन तल (Euclidean plane) में समपरिमित असमिका (Isoperimetric Inequality) को संबोधित करता है। प्रमेय बताता है कि किसी भी सरल बंद वक्र $C$ के लिए, जिसका परिमाप $L$ और अंतर्निहित क्षेत्रफल $A$ है, असमिका $L^2 \geq 4\pi A$ सत्य होती है। समानता (Equality) तभी प्राप्त होती है जब वक्र एक वृत्त हो।

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

2. कार्यप्रणाली

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

चरण I: फूरियर-विश्लेषणात्मक आधार

वक्र को संबोधित करने से पहले, लेखकों ने Mathlib के भीतर हार्मोनिक विश्लेषण से आवश्यक उपकरणों को औपचारिक रूप दिया:

लंबवत संबंध (Orthogonality Relations): $[-\pi, \pi]$ पर त्रिकोणमितीय फलनों ( $\sin(nx), \cos(nx)$ ) की लंबवतता को औपचारिक रूप दिया।
अभिसरण सिद्धांत (Convergence Theory): फूरियर आंशिक योगों के एकसमान अभिसरण (uniform convergence) को वेइरस्ट्रास एम-परीक्षण (Weierstrass M-test) का उपयोग करके स्थापित किया। यह सुनिश्चित करने के लिए महत्वपूर्ण था कि सीमा (limit) में निरंतरता और समाकलनीयता जैसे गुण संरक्षित रहें।
पद-दर-पद अवकलन (Term-by-Term Differentiation): उन शर्तों को सिद्ध किया जिनके तहत एक फूरियर श्रृंखला को पद-दर-पद अवकलित किया जा सकता है, जिसके लिए $n(|a_n| + |b_n|)$ की समाप्यता (summability) आवश्यक है।
पार्सवल का प्रमेय (Parseval's Theorem): फलन के $L^2$ मान (norm) और उसके फूरियर गुणांकों के $\ell^2$ मान के बीच संबंध बताने वाली पहचान को औपचारिक रूप दिया।
विर्टिंगर की असमिका (Wirtinger's Inequality): पार्सवल के प्रमेय से सीधे इस असमिका (जो शून्य-माध्य (zero-mean) वाले आवर्ती फलन के $L^2$ मान को उसके अवकलज से जोड़ती है) को व्युत्पन्न किया।

चरण II: ज्यामितीय प्रमाण (हर्टविज़ का तर्क)

लेखकों ने $\mathbb{R}^2$ में एक सरल बंद $C^1$ वक्र $\gamma$ का मॉडल तैयार किया और पाँच तार्किक चरणों में प्रमाण निष्पादित किया:

पुनः पैरामीट्रिकरण (Reparametrization): फूरियर विश्लेषण की सुविधा के लिए वक्र को चाप-लंबाई (arc-length) $s \in [0, L]$ से कोणीय पैरामीटर $\theta \in [0, 2\pi]$ में पुनः पैरामीट्रिक किया गया।
क्षेत्रफल सूत्र: अंतर्निहित क्षेत्रफल $A$ को शूलेस सूत्र (Shoelace formula) (ग्रीन का प्रमेय) का उपयोग करके व्यक्त किया गया: $A = \frac{1}{2} \int_0^L (x y' - y x') dt$ । पुनः पैरामीट्रिकरण और समाकलन-से-भाग (integration by parts) के बाद, यह सरल होकर $A = \int_0^{2\pi} f(\theta)g'(\theta) d\theta$ हो गया, जहाँ $f$ और $g$ निर्देशांक फलन हैं।
AM-GM असमिका: क्षेत्रफल को सीमित करने के लिए $2fg' \leq f^2 + (g')^2$ असमिका को लागू किया गया: $A \leq \frac{1}{2} \int_0^{2\pi} (f^2 + (g')^2) d\theta$ ।
विर्टिंगर का अनुप्रयोग: यह मानते हुए कि केंद्रक (centroid) मूल बिंदु पर है (अर्थात $f$ के लिए शून्य माध्य), विर्टिंगर की असमिका ( $\int f^2 \leq \int (f')^2$ ) को लागू किया गया। इसने सीमा को बढ़ाकर $A \leq \frac{1}{2} \int_0^{2\pi} ((f')^2 + (g')^2) d\theta$ कर दिया।
चाप-लंबाई प्रतिबंध: इस तथ्य का उपयोग करते हुए कि वक्र चाप-लंबाई द्वारा पैरामीट्रिक किया गया है, लेखकों ने दिखाया कि $(f')^2 + (g')^2 = (L/2\pi)^2$ । समाकल में इस स्थिरांक को प्रतिस्थापित करने से अंतिम सीमा प्राप्त हुई: $A \leq \frac{L^2}{4\pi}$ ।

3. प्रमुख योगदान

हर्टविज़ के प्रमाण का प्रथम पूर्ण औपचारिककरण: जबकि अन्य प्रणालियों (Coq, Isabelle) में आंशिक औपचारिककरण मौजूद हैं, यह Lean 4 में हर्टविज़ के विशिष्ट विश्लेषणात्मक दृष्टिकोण का एक पूर्ण, मशीन-सत्यापित प्रमाण है।
Mathlib का विस्तार: इस परियोजना ने शास्त्रीय वास्तविक विश्लेषण (classical real analysis) में Mathlib की क्षमताओं का विस्तार किया, विशेष रूप से:
- स्पष्ट गुणांक अनुक्रमों (अमूर्त $L^2$ सिद्धांत के बजाय) के साथ शास्त्रीय फूरियर श्रृंखलाओं को लागू करना।
- त्रिकोणमितीय श्रृंखलाओं के लिए वेइरस्ट्रास एम-परीक्षण और पद-दर-पद अवकलन प्रमेयों को औपचारिक रूप देना।
- अमूर्त यूक्लिडियन स्थान परिभाषाओं (EuclideanSpace) और निर्देशांक-वार कलन (coordinate-wise calculus) के बीच के अंतर को पाटना।
तकनीकी बारीकियों को संभालना: लेखकों ने जटिल औपचारिककरण चुनौतियों को सफलतापूर्वक पार किया, जिनमें शामिल हैं:
- योग और समाकलन का विनिमय: MeasureTheory.integral_tsum_of_summable_integral_norm के माध्यम से डोमिनेटेड कन्वर्जेंस थ्योरम (Dominated Convergence Theorem) को स्पष्ट रूप से आह्वान करना।
- इंडेक्सिंग परंपराएं (Indexing Conventions): फूरियर गुणांकों में उपयोग किए जाने वाले प्राकृतिक संख्या इंडेक्सिंग ( $\mathbb{N}$ ) और धनात्मक प्राकृतिक संख्या इंडेक्सिंग ( $\mathbb{N}^+$ ) के बीच के अंतर को हल करना।
- प्रक्षेपों का अवकलन (Differentiation of Projections): $\mathbb{R}^2$ में निर्देशांक फलनों को संभालने के लिए प्रक्षेपों के फ्रेट डेरिवेटिव्स (Fréchet derivatives) को वक्र के अवकलज के साथ सही ढंग से संयोजित करना।

4. परिणाम

औपचारिककरण ने मुख्य प्रमेय को सफलतापूर्वक सत्यापित किया:
$\text{किसी भी सरल बंद } C^1 \text{ वक्र } \gamma \text{ के लिए, } \quad \text{Area}(\gamma) \leq \frac{\text{Length}(\gamma)^2}{4\pi}$
प्रमाण GitHub पर सार्वजनिक रिपॉजिटरी IsoperimetricInequality पर उपलब्ध है। कोडबेस को दो मुख्य फाइलों में संरचित किया गया है:

IsoperimetricInequality.Basic: इसमें फूरियर विश्लेषण के आधार (लंबवतता, पार्सवल, विर्टिंगर) शामिल हैं।
IsoperimetricInequality.Adolf Hurwitz proof: इसमें ज्यामितीय व्युत्पत्ति और अंतिम असमिका शामिल है।

5. महत्व

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

संक्षेप में, यह शोध पत्र एक शास्त्रीय ज्यामितीय प्रमाण के कठोर, मशीन-जाँचे गए पुनर्निर्माण का प्रतिनिधित्व करता है, जो गणितीय विश्लेषण के तार्किक आधारों को मान्य करने के लिए आधुनिक प्रमाण सहायकों (proof assistants) की शक्ति को प्रदर्शित करता है।