🔢 mathematics

The continuous functional calculus in Lean

यह शोध पत्र किसी भी प्रूफ़ असिस्टेंट (proof assistant) में निरंतर फलन कलन (continuous functional calculus) के पहले औपचारिककरण को प्रलेखित करता है, जिसमें लीन (Lean) की मैथलिब (Mathlib) लाइब्रेरी में इसके कार्यान्वयन, अंतर्निहित गणितीय सिद्धांत, और उन प्रमुख डिज़ाइन निर्णयों का विवरण दिया गया है जिन्होंने गणितीय समुदाय के लिए उपयोगिता सुनिश्चित की।

मूल लेखक: Anatole Dedecker, Jireh Loreaux

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

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

CC BY 4.0

मूल लेखक: Anatole Dedecker, Jireh Loreaux

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

कल्पना कीजिए कि आप एक बहुत ही जटिल, उच्च-तकनीकी रसोई में काम करने वाले एक मास्टर शेफ हैं। यह रसोई C-algebras* की गणितीय दुनिया का प्रतिनिधित्व करती है, जो ऑपरेटरों (जैसे डेटा को बदलने वाली मशीनें) से संबंधित एक शाखा है, जिन्हें सीधे समझना अविश्वसनीय रूप से कठिन हो सकता है।

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

यहाँ उन्होंने जो किया है, उसकी कहानी सरल शब्दों में दी गई है।

1. समस्या: "ब्लैक बॉक्स" मशीन

इस गणितीय रसोई में, आपके पास अक्सर एक विशेष मशीन (एक तत्व $a$ ) होती है जो कुछ जटिल कार्य करती है। आप उसके साथ कुछ नया करना चाहते हैं, जैसे उसका वर्गमूल (square root) निकालना, या उस पर कोई जटिल वक्र (curve) लागू करना।

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

2. समाधान: "जादुई लेबल"

कंटीन्यूअस फंक्शनल कैलकुलस एक जादुई लेबल है। मशीन को खोलने के बजाय, आप बस उस पर एक लेबल चिपका देते हैं जो कहता है, "मुझ पर यह फलन $f$ लागू करें।"

पुराना तरीका: "मुझे इस मशीन का वर्गमूल निकालना है। मुझे पहले यह सिद्ध करना होगा कि मशीन 'नॉर्मल' है, इसका आंतरिक स्पेक्ट्रम खोजना होगा, यह सिद्ध करना होगा कि वर्गमूल फलन उस स्पेक्ट्रम पर निरंतर (continuous) है, और फिर मशीन का पुनर्निर्माण करना होगा।"
नया तरीका: "मेरे पास एक मशीन $a$ है। मैं फलन $f(x) = \sqrt{x}$ लागू करना चाहता हूँ। मैं बस $f(a)$ लिख देता हूँ।"

यह पेपर बताता है कि कैसे लेखकों ने Lean में इस "जादुई लेबल" प्रणाली का एक डिजिटल संस्करण बनाया है, जो गणित की गलतियों की जाँच करने वाला एक 'प्रूफ असिस्टेंट' है। उन्होंने केवल गणित नहीं लिखा; उन्होंने इंटरफ़ेस को इस तरह से डिज़ाइन किया ताकि एक इंसान (या कंप्यूटर) तकनीकी विवरणों में फंसे बिना इसे आसानी से उपयोग कर सके।

3. डिज़ाइन: "पहले लिखें, सोचें बाद में"

गणित को प्रोग्राम करने की सबसे बड़ी चुनौतियों में से एक यह है कि कंप्यूटर बहुत सख्त होते हैं। यदि आप कंप्यूटर से $1/0$ की गणना करने के लिए कहते हैं, तो वह क्रैश हो जाता है। यदि आप किसी ऐसी मशीन पर फलन लागू करने के लिए कहते हैं जो "नॉर्मल" नहीं है, तो वह क्रैश हो सकता है।

लेखकों ने "जंक वैल्यूज़" (Junk Values) नामक एक रणनीति अपनाने का निर्णय लिया।

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

4. "यूनिवर्सल एडेप्टर" (क्लासेस)

लेखकों ने महसूस किया कि इस "जादुई लेबल" उपकरण को विभिन्न प्रकार की रसोईओं में काम करने की आवश्यकता है:

कॉम्प्लेक्स नंबर्स (मानक रसोई)।
रियल नंबर्स (एक सरल रसोई)।
नॉन-नेगेटिव नंबर्स (एक ऐसी रसोई जहाँ नकारात्मक सामग्री नहीं हो सकती)।

तीन अलग-अलग, असंगत उपकरण बनाने के बजाय, उन्होंने एक यूनिवर्सल एडेप्टर (Lean में जिसे "क्लास" कहा जाता है) बनाया है। यह एडेप्टर जानता है कि किसी भी रसोई में कैसे फिट होना है। यदि आप वास्तविक संख्याओं (real numbers) के साथ काम कर रहे हैं, तो यह स्वचालित रूप से रियल-नंबर मोड में स्विच हो जाता है। यदि आप मैट्रिसेस (matrices) के साथ काम कर रहे हैं, तो यह मैट्रिक्स मोड में स्विच हो जाता है।

5. "नॉन-यूनिटल" चुनौती (मुख्य स्विच के बिना रसोई)

अधिकांश गणितीय उपकरण यह मानकर चलते हैं कि रसोई में एक "मुख्य स्विच" (एक आइडेंटिटी एलिमेंट) है। लेकिन कुछ गणितीय रसोईओं (नॉन-यूनिटल अल्जेब्रा) में यह नहीं होता है।

उपमा: एक लाइट स्विच की कल्पना करें जो पूरे कमरे को नियंत्रित करता है। एक "यूनिटल" रसोई में, स्विच मौजूद होता है। एक "नॉन-यूनिटल" रसोई में, स्विच गायब होता है।
समाधान: लेखकों ने यह पता लगाया कि उनका उपकरण कैसे काम करेगा भले ही मुख्य स्विच मौजूद न हो। उन्होंने ऐसा करने के लिए कि वे एक पल के लिए रसोई में एक स्विच होने का नाटक करें, काम करें, और फिर स्विच को हटा दें। यह उपकरण को किसी भी रसोई में काम करने की अनुमति देता है, चाहे उसमें स्विच हो या न हो।

6. यह क्यों महत्वपूर्ण है

इस पेपर से पहले, यदि किसी गणितज्ञ को इस उपकरण का उपयोग कंप्यूटर प्रमाण में करना होता था, तो उन्हें इतनी बाधाओं को पार करना पड़ता था कि कागज पर गणित करना और कंप्यूटर को अनदेखा करना अधिक आसान था।

लेखकों का लक्ष्य कंप्यूटर इंटरफ़ेस को कागज पर लिखने जितना आसान बनाना था।

पहले: आपको हर एक चरण के लिए प्रमाण प्रमाणपत्रों (proof certificates) का एक भारी बैकपैक लेकर चलना पड़ता था।
बाद में: कंप्यूटर के पास एक "स्मार्ट असिस्टेंट" (जिसे autoParam कहा जाता है) है जो उन प्रमाणपत्रों को आपके लिए स्वचालित रूप से खोज लेता है। यदि आप sqrt(a) लिखते हैं, तो कंप्यूटर स्वचालित रूप से जाँचता है कि क्या a वर्गमूल के लिए एक वैध उम्मीदवार है। यदि यह है, तो बहुत अच्छा! यदि नहीं, तो यह आपको बता देता है।

सारांश

यह पेपर जटिल गणितीय मशीनों को संचालित करने के लिए एक उपयोगकर्ता के अनुकूल, सार्वभौमिक और सुदृढ़ डिजिटल उपकरण के निर्माण का दस्तावेजीकरण करता है।

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

परिणामस्वरूप एक ऐसा सिस्टम है जहाँ गणितज्ञों का ध्यान विचारों (नुस्खे) पर केंद्रित होता है न कि सिंटैक्स (सब्जियाँ काटने) पर, जिससे प्रूफ़ असिस्टेंट में उन्नत ऑपरेटर थ्योरी का औपचारिककरण (formalization) संभव हो पाता है।

तकनीकी सारांश: लीन (Lean) में निरंतर फलन कलन (The Continuous Functional Calculus)

समस्या विवरण
निरंतर फलन कलन (continuous functional calculus) $C^*$ -बीजगणितों के सिद्धांत में एक मौलिक उपकरण है, जो क्रमविनिमेय (commutative) $C^*$ -उप-बीजगणितों को कॉम्पैक्ट हाउसडॉर्फ स्पेस पर निरंतर फलनों के बीजगणित के रूप में पहचानने की अनुमति देता है। हालांकि यह गणितीय रूप से अच्छी तरह से समझ में आया है, लेकिन लीन जैसे प्रूफ़ असिस्टेंट में इसका औपचारिककरण (formalization) महत्वपूर्ण चुनौतियाँ प्रस्तुत करता है। प्राथमिक कठिनाई गणितीय निष्ठा और उपयोगिता (usability) के बीच संतुलन बनाने में निहित है। एक "स्वाभाविक" गणितीय परिभाषा अक्सर आश्रित प्रकारों (dependent types) (जैसे, केवल एक तत्व के स्पेक्ट्रम पर परिभाषित फलन) और बंडल संरचनाओं (bundled structures) (जैसे, एक विशिष्ट प्रकार के रूप में निरंतर मानचित्र) पर निर्भर करती है। हालांकि ये कठोर हैं, लेकिन ये औपचारिक प्रमाणों में घर्षण पैदा करते हैं: पुनर्गठन (rewriting) कठिन हो जाता है क्योंकि प्रकार विशिष्ट तत्वों पर निर्भर करते हैं, और फलनों का संयोजन करने के लिए जटिल सबटाइप कोएर्शन (subtype coercions) और निरंतरता प्रमाणों का प्रबंधन करना आवश्यक होता है। लेखकों ने पहचाना कि एक सख्त गणितीय सरलता को प्राथमिकता देने वाला डिज़ाइन अक्सर मैथलिब (Mathlib) जैसी लाइब्रेरी के लिए आवश्यक व्यावहारिक उपयोगिता के "लिटमस परीक्षणों" में विफल रहता है।

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

अनबंडलिंग और "जंक वैल्यूज़" (Unbundling and "Junk Values"):
स्पेक्ट्रम $C(\sigma(a), \mathbb{C})$ पर निरंतर फलनों के प्रकार से बीजगणित तक एक मानचित्र को परिभाषित करने के बजाय, लेखकों ने एक फलन cfc को परिभाषित किया जो किसी भी फलन $f: \mathbb{C} \to \mathbb{C}$ और किसी भी तत्व $a$ को स्वीकार करता है। यदि $a$ सामान्य (normal) नहीं है या $f$ स्पेक्ट्रम पर निरंतर नहीं है, तो फलन एक "जंक वैल्यू" (आमतौर पर 0) लौटाता है।
- तर्क: यह उपयोगकर्ताओं को $a$ के सामान्य होने या $f$ के निरंतर होने का प्रमाण दिए बिना $f(a)$ जैसे व्यंजकों को लिखने की अनुमति देता है। यह अनौपचारिक गणित के "पहले लिखें, बाद में सोचें" दृष्टिकोण की नकल करता है, जिससे प्रमाण का बोझ तब तक टाल दिया जाता है जब तक कि किसी गैर-मामूली गुण की आवश्यकता न हो। यह सहज पुनर्गठन (rw) को भी सक्षम बनाता है क्योंकि तर्क के प्रकार अब $a$ के विशिष्ट गुणों पर निर्भर नहीं करते हैं।
क्लास-आधारित एब्स्ट्रैक्शन (Class-Based Abstraction):
विभिन्न स्केलर रिंगों ( $\mathbb{C}$ , $\mathbb{R}$ , और $\mathbb{R}_{\ge 0}$ ) और विभिन्न तत्व प्रकारों (सामान्य, स्व-संयोजक (self-adjoint), गैर-ऋणात्मक) को संभालने के लिए, लेखकों ने फलन कलन को एक टाइप क्लास ContinuousFunctionalCalculus के रूप में लागू किया।
- प्रेडिकेट सामान्यीकरण (Predicate Generalization): क्लास को बीजगणक तत्वों पर एक प्रेडिकेट $p$ (जैसे, IsStarNormal, IsSelfAdjoint, 0 ≤ a) द्वारा पैरामीटराइज किया गया है। यह एक ही इंटरफेस को कोड डुप्लिकेशन के बिना विभिन्न मामलों को कवर करने की अनुमति देता है।
- Prop-Valued बनाम Data: प्रारंभिक संस्करणों में $*$ -होमोमोर्फिज्म को डेटा के रूप में शामिल किया गया था। हालाँकि, डेफिनिशनल इक्वैलिटी (जहाँ एक ही मानचित्र के दो अलग-अलग निर्माण डेफिनिशनली समान नहीं होते) की समस्याओं से बचने के लिए, अंतिम डिज़ाइन इस क्लास को एक Prop बनाता है। यह विशिष्ट गुणों के साथ एक अद्वितीय $*$ -होमोमोर्फिज्म के अस्तित्व की पुष्टि करता है, न कि स्वयं मानचित्र को संग्रहीत करता है।
गैर-इकाई बीजगणकों (Non-Unital Algebras) को संभालना:
औपचारिककरण गैर-इकाई $C^*$ -बीजगणकों तक विस्तृत है। प्रत्येक परिभाषा के लिए मिनिमल यूनिटाइजेशन जैसे बाह्य निर्माणों पर निर्भर करने के बजाय, लेखकों ने क्वासिस्पेक्ट्रम (quasispectrum) की एक आंतरिक परिभाषा पेश की। गैर-इकाई फलन कलन को 0 पर विलुप्त होने वाले (या 0 को 0 पर मैप करने वाले) फलनों पर परिभाषित किया गया है, जिससे यूनिटल और गैर-इकाई संदर्भों के बीच बार-बार स्विच करने की आवश्यकता से बचा जा सके।
autoParam के माध्यम से ऑटोमेशन:
निरंतरता और सामान्यता के प्रमाणों को मैन्युअल रूप से पास करने की औपचारिकता को कम करने के लिए, लेखकों ने लीन की autoParam विशेषता का उपयोग किया। ऐसी परिकल्पनाएँ जैसे "f स्पेक्ट्रम पर निरंतर है", डिफ़ॉल्ट टैक्टिक्स से सुसज्जित हैं। यदि उपयोगकर्ता प्रमाण प्रदान नहीं करता है, तो लीन मौजूदा लेम्मा (जैसे, aesop, fun_prop) का उपयोग करके इसे स्वचालित रूप से संश्लेषित करने का प्रयास करता है।
विशिष्टता एक अलग क्लास के रूप में (Uniqueness as a Separate Class):
संयोजन गुण ( $g(f(a)) = (g \circ f)(a)$ ) सिद्धांत के केंद्र में है। लेखकों ने स्टोन-वेइरस्ट्रास प्रमेय (जो $\mathbb{R}_{\ge 0}$ के लिए विफल रहता है) का उपयोग करने के बजाय एक विशिष्टता तर्क (uniqueness argument) का उपयोग करके इसे सिद्ध किया। उन्होंने $*$ -होमोमोर्फिज्म की विशिष्टता को एक अलग क्लास ContinuousMap.UniqueHom में समाहित किया, जिससे विभिन्न स्केलर रिंगों में जेनेरिक रूप से संयोजन गुण को प्राप्त किया जा सका।

मुख्य योगदान और परिणाम

प्रथम औपचारिककरण: यह कार्य किसी भी प्रूफ़ असिस्टेंट में निरंतर फलन कलन का पहला औपचारिककरण है।
मैथलिब एकीकरण: यह कार्यान्वयन मैथलिब में मर्ज किया गया है, जो जटिल, वास्तविक और गैर-ऋणात्मक वास्तविक फलन कैलकुलाई के लिए एक एकीकृत इंटरफेस प्रदान करता है।
उपयोगिता सत्यापन: डिज़ाइन को विशिष्ट "लिटमस टेस्ट" के विरुद्ध मान्य किया गया था, जिनमें शामिल हैं:
- उन फलनों का उपयोग करके व्युत्क्रम ( $f(a^{-1})$ ) को परिभाषित करना जो हर जगह निरंतर नहीं हैं (जैसे, $x \mapsto x^{-1}$ )।
- स्व-संयोजक और गैर-ऋणात्मक तत्वों के लिए धनात्मक/ऋणात्मक भाग और वर्ग मूल (square roots) का निर्माण करना।
- $\mathbb{R}$ पर मैट्रिसेस (matrices) पर फलन कलक को लागू करना (जिनमें मैथलिब में वैश्विक मीट्रिक संरचना का अभाव है)।
ऑटोमेशन: इंटरफेस उच्च-स्तरीय ऑटोमेशन का समर्थन करता है, जिससे उपयोगकर्ता न्यूनतम मैन्युअल हस्तक्षेप के साथ $f(-a) = (x \mapsto f(-x))(a)$ जैसे गुणों को सिद्ध कर सकते हैं।
अनुप्रयोग: इंटरफेस का उपयोग पहले से ही उन्नत परिणामों को औपचारिक बनाने के लिए किया गया है, जिसमें शामिल हैं:
- गैर-इकाई $C^*$ -बीजगणकों में अनुमानित इकाइयों (approximate units) का अस्तित्व।
- दोनों चरों में फलन कलन की निरंतरता।
- मानचित्र $a \mapsto |a|$ , $a \mapsto a^p$ , और $a \mapsto \log(a)$ के गुण।
- यूनिटरी तत्वों और प्रोजेक्शन के संबंध में परिणाम।

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

लेखक वर्तमान स्थिति के बारे में विनम्र हैं, कई सीमाओं को स्वीकार करते हैं:

सिम्प लेम्मा (Simp Lemmas): autoParam को ट्रिगर करने के लिए स्पष्ट तर्कों की आवश्यकता के कारण, कई लेम्मा को मैन्युअल हस्तक्षेप के बिना simp नियमों के रूप में उपयोग नहीं किया जा सकता है, जिससे कुछ प्रमाण वांछित से अधिक विस्तृत हो जाते हैं।
$\mathbb{R}_{\ge 0}$ की जटिलताएं: स्केलर रिंग के रूप में गैर-ऋणात्मक वास्तविकों का उपयोग विशिष्ट तकनीकी बाधाएं (जैसे, ट्रंकेटेड घटाव, रिंग संरचना का अभाव) पेश करता है जिन्हें अलग प्रमेय कथनों की आवश्यकता होती है।
रियल $C^*$ -बीजगणक: हालांकि फ्रेमवर्क को रियल $C^*$ -बीजगणकों का समर्थन करने के लिए डिज़ाइन किया गया है, वास्तविक बीजगणकों के लिए जटिल (complex) पर आधारित फलन कलन का विशिष्ट मामला (जिसके लिए फलनों का अलग डोमेन आवश्यक है) अभी तक पूरी तरह से एकीकृत नहीं हुआ है और भविष्य के कार्य के लिए नियोजित है।

निष्कर्षतः, यह पेपर एक गहरे ऑपरेटर बीजगणक सिद्धांत को एक उपयोगी औपचारिक प्रणाली में अनुवाद करने के सफल प्रयास का दस्तावेजीकरण करता है, जो एक बड़े पैमाने के इंटरैक्टिव थ्योरम प्रूवर के संदर्भ में गणितीय लालित्य और व्यावहारिक उपयोगिता के बीच के समझौतों को उजागर करता है।