🔢 mathematics

Formal Foundations and Proof-Carrying Certificates for q-ary Covering Codes in Lean 4

यह शोध पत्र Lean 4 में q-ary कवरिंग कोड के प्रारंभिक सिद्धांत (elementary theory) का एक औपचारिक रूप प्रस्तुत करता है, जो कवरिंग संख्याओं पर ऊपरी और निचली सीमाओं को सत्यापित करने के लिए प्रमाण-वहन प्रमाणपत्रों (proof-carrying certificates) के साथ एक पुन: प्रयोज्य, ऑडिट योग्य आधार स्थापित करता है।

मूल लेखक: Andreas Florath

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

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

CC BY 4.0

मूल लेखक: Andreas Florath

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

कल्पना कीजिए कि आप सीमित संख्या में "सुरक्षा जाल" (safety nets) का उपयोग करके एक विशाल, बहु-आयामी शतरंज के बोर्ड को कवर करने की कोशिश कर रहे हैं।

गणित की दुनिया में, यह कवरिंग कोड्स (Covering Codes) की समस्या है। आपके पास संभावित स्थानों का एक ग्रिड है (जैसे कि शतरंज का बोर्ड, लेकिन यह 3D, 4D या यहाँ तक कि उच्च आयामों वाला भी हो सकता है)। आप अपने ग्रिड पर कुछ "केंद्र" (centers) रखना चाहते हैं। नियम यह है कि बोर्ड का प्रत्येक वर्ग (square) कम से कम एक केंद्र से एक निश्चित दूरी (मान लीजिए, एक कदम) के भीतर होना चाहिए।

बड़ा सवाल यह है कि: पूरे बोर्ड को कवर करने के लिए आपको न्यूनतम कितने केंद्रों की आवश्यकता है?

एंड्रियास फ्लोरथ (Andreas Florath) द्वारा लिखा गया यह शोध पत्र एक नया रिकॉर्ड खोजने की कोशिश नहीं करता है, बल्कि यह एक डिजिटल, अटूट तिजोरी बनाता है ताकि यह सिद्ध किया जा सके कि जो संख्याएँ हम पहले से जानते हैं वे सही हैं।

यहाँ इस शोध पत्र के विचारों का सरल उपमाओं (analogies) का उपयोग करके विवरण दिया गया है:

1. "प्रमाण-वाहक प्रमाण पत्र" (The Golden Ticket)

आमतौर पर, जब कोई गणितज्ञ कहता है, "मैंने एक कोड खोजा है जिसमें 73 केंद्र हैं जो बोर्ड को कवर करते हैं," तो वे आपको संख्याओं की एक सूची दिखाते हैं। आपको उन पर विश्वास करना पड़ता है, या घंटों तक स्वयं गणित की जाँच करनी पड़ती है।

यह शोध पत्र एक "प्रमाण-वाहक प्रमाण पत्र" (Proof-Carrying Certificate) पेश करता है। इसे केवल संख्याओं की सूची के रूप में नहीं, बल्कि एक स्व-जाँच करने वाले जादू के साथ आए "गोल्डन टिकट" के रूप में समझें।

टिकट: यह कहता है, "यहाँ 73 केंद्रों का एक सेट है।"
जादुई ट्रिक: टिकट में एक छोटा, स्वचालित रोबोट (जो Lean 4 नामक भाषा में लिखा गया है) शामिल है जो तुरंत बोर्ड के हर एक वर्ग की जाँच करता है ताकि पुष्टि की जा सके: "हाँ, यह वर्ग कवर है। हाँ, वह वर्ग कवर है। हाँ, वे सभी कवर हैं।"
परिणाम: आपको लेखक पर भरोसा करने की आवश्यकता नहीं है। आप बस रोबोट चलाते हैं। यदि रोबोट "पास" कहता है, तो प्रमाण 100% गणितीय रूप से गारंटीकृत है।

2. "दो-भागों वाली पहेली" (The Two-Part Puzzle)

यह सिद्ध करने के लिए कि आपके पास केंद्रों की सटीक (exact) संख्या है, आपको एक साथ दो अलग-अलग पहेलियों को हल करने की आवश्यकता है:

ऊपरी सीमा (The Construction): "मैं 73 केंद्रों के साथ बोर्ड को कवर कर सकता हूँ।" (आप सूची दिखाते हैं)।
निचली सीमा (The Impossible Task): "72 केंद्रों के साथ बोर्ड को कवर करना असंभव है।" (आप सिद्ध करते हैं कि आप चाहे कितनी भी कोशिश कर लें, हमेशा एक खाली जगह रह जाएगी)।

यह शोध पत्र एक ऐसी प्रणाली बनाता है जहाँ ये दोनों पहेलियाँ अलग-अलग हिस्से हैं। आपके पास "73" के लिए एक प्रमाण पत्र हो सकता है और "72 के साथ असंभव" के लिए एक अलग प्रमाण पत्र हो सकता है। जब वे मिलते हैं, तो वे एक सटीक उत्तर बनाने के लिए आपस में जुड़ जाते हैं।

3. गणित का "लेगो" (The "Lego" of Math)

लेखक ने लेगो ब्रिक्स (औपचारिक नियमों) की एक विशाल लाइब्रेरी बनाई है।

कुछ ब्रिक्स सरल हैं: "यदि आप एक छोटे बोर्ड को कवर करते हैं, तो आप कुछ और टुकड़े जोड़कर एक बड़े बोर्ड को कवर कर सकते हैं।"
कुछ ब्रिक्स जटिल हैं: "यदि आप दो अलग-अलग प्रकार के बोर्डों को मिलाते हैं, तो कवरिंग नियम बिल्कुल कैसे बदलते हैं।"

इस शोध पत्र की सुंदरता यह है कि ये ब्रिक्स परस्पर विनिमेय (interchangeable) हैं। यदि कोई अन्य व्यक्ति बोर्ड को कवर करने का एक नया तरीका खोजता है, तो वे बस अपने नए ब्रिक को इस मौजूदा लेगो संरचना में जोड़ सकते हैं, और पूरा सिस्टम स्वचालित रूप से उसे सत्यापित कर देगा।

4. "सत्य का डेटाबेस" (The "Database of Truth")

शोध पत्र में एक प्रमाण-वाहक डेटाबेस शामिल है। एक ऐसी लाइब्रेरी बुक की कल्पना करें जहाँ, उत्तर "7" प्रिंट करने के बजाय, पुस्तक में प्रमाण का एक वीडियो रिकॉर्डिंग शामिल है।

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

5. "फुटबॉल पूल" का उदाहरण

शोध पत्र समस्या को समझाने के लिए एक वास्तविक दुनिया की उपमा का उपयोग करता है: द फुटबॉल पूल (The Football Pool)।
कल्पना कीजिए कि आप 8 फुटबॉल मैचों पर दांव लगा रहे हैं। प्रत्येक मैच के 3 संभावित परिणाम हैं (जीत, ड्रॉ, हार)। आप टिकटों का एक सेट खरीदना चाहते हैं।

लक्ष्य: परिणाम चाहे जो भी हों, आप चाहते हैं कि आपके कम से कम एक टिकट "करीब" (शायद केवल 1 भविष्यवाणी गलत) हो।
गणित: यह गारंटी देने के लिए कि आपको कितने टिकट खरीदने की आवश्यकता है कि कम से कम एक टिकट सही हो?
शोध पत्र की भूमिका: यह शोध पत्र इस समस्या के लिए एक प्रसिद्ध, प्रकाशित समाधान (जहाँ किसी ने 486 टिकटों के सेट का समाधान खोजा था) को लेता है और उसे मशीन-जाँच योग्य प्रमाण में बदल देता है। यह सिद्ध करता है कि 486 टिकट काम करते हैं।

यह शोध पत्र वास्तव में क्या दावा करता है (और क्या नहीं करता)

यह दावा करता है: इसने एक ठोस, पुन: प्रयोज्य आधार (एक "औपचारिक आधार") बनाया है जहाँ कवरिंग कोड प्रमाणों को संग्रहीत, जांचा और स्वचालित रूप से संयोजित किया जा सकता है। इसने कई विशिष्ट, ज्ञात संख्याओं (जैसे 8-मैच वाली समस्या के लिए 486 टिकट) को इस नई प्रणाली का उपयोग करके सत्यापित किया है।
यह दावा नहीं करता: यह दावा नहीं करता कि इसने आवश्यक टिकटों की सबसे छोटी संख्या के लिए कोई नया रिकॉर्ड खोजा है। यह दावा नहीं करता कि इसने हर संभव परिदृश्य के लिए समस्या को हल कर दिया है। यह एक उपकरण-निर्माण (tool-building) वाला शोध पत्र है, न कि एक रिकॉर्ड-तोड़ने वाला (record-breaking) शोध पत्र।

व्यापक चित्र (The Big Picture)

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

तकनीकी सारांश: Lean 4 में q-ary कवरिंग कोड्स के लिए औपचारिक आधार और प्रमाण-वहन करने वाले प्रमाणपत्र (Proof-Carrying Certificates)

समस्या विवरण
परिमित हैमिंग स्पेस (finite Hamming spaces) में कवरिंग कोड्स, शब्दों (codewords) के सबसे छोटे ऐसे सेट की खोज करते हैं जिससे त्रिज्या $r$ के हैमिंग बॉल्स का संघ (union) संपूर्ण स्थान $A^n$ को कवर कर सके। केंद्रीय मात्रा $q$ -ary कवरिंग संख्या $K_q(n,r)$ है, जिसे ऐसे कोड के न्यूनतम आकार के रूप में परिभाषित किया गया है। हालाँकि परिभाषा अत्यंत सरल है, लेकिन $K_q(n,r)$ के सटीक मान या कड़े अनुमान (bounds) निर्धारित करने के लिए आमतौर पर स्पष्ट निर्माण (explicit constructions), गणना तर्क (counting arguments), पुनरावर्ती संबंध (recursive relations) और कंप्यूटर खोजों के मिश्रण पर निर्भर रहना पड़ता है। क्षेत्र में एक महत्वपूर्ण चुनौती यह है कि सटीक कथन $K_q(n,r) = k$ के लिए दो स्वतंत्र घटकों की आवश्यकता होती है: एक स्पष्ट निर्माण जो ऊपरी सीमा ( $K_q(n,r) \le k$ ) सिद्ध करता है, और एक प्रमाण कि इससे छोटा कोई कोड अस्तित्व में नहीं है (निचली सीमा $K_q(n,r) \ge k$ )। ये दोनों घटक अक्सर अलग-अलग स्रोतों से आते हैं, जिससे सटीक मानों का सत्यापन करना कठिन हो जाता है।

कार्यप्रणाली
यह शोध पत्र Lean 4 थ्योरम प्रूवर में प्रारंभिक कवरिंग कोड सिद्धांत के औपचारिकीकरण (formalization) को प्रस्तुत करता है। इसकी कार्यप्रणाली तीन मुख्य डिज़ाइन विकल्पों द्वारा लक्षित है:

शब्दों का प्रतिनिधित्व (Representation of Words): शब्दों को एक समन्वय प्रकार (coordinate type) से एक वर्णमाला प्रकार (alphabet type) तक के आश्रित फलनों (dependent functions) के रूप में मॉडल किया गया है। लंबाई $n$ के सामान्य $q$ -ary हैमिंग स्पेस को Fin n → Fin q के रूप में दर्शाया गया है। यह कार्यात्मक प्रतिनिधित्व अमूर्त समन्वय प्रकारों के लिए एक सामान्य इंटरफ़ेस बनाए रखता है जबकि $q$ -ary विशिष्टता को सरल बनाता है।
प्रमाणपत्र-शैली के विधेय (Certificate-Style Predicates): $K_q(n,r)$ $K_{q} (n, r)$ को एक गैर-कंप्यूटेबल मिनिमाइजेशन फंक्शन के रूप में परिभाषित करने के बजाय, यह औपचारिकीकरण कवरिंग संख्याओं के बारे में दावों को दर्शाने के लिए तार्किक विधेयों का उपयोग करता है।
- KUpper r k: अधिकतम $k$ आकार के एक परिमित कवरिंग कोड के अस्तित्व को प्रमाणित करता है (ऊपरी सीमा)।
- KLower r k: यह प्रमाणित करता है कि प्रत्येक परिमित कवरिंग कोड का आकार कम से कम $k$ है (निचली सीमा)।
- KSpec r k: दोनों को मिलाकर सटीक होने का दावा करता है ( $K_q(n,r) = k$ )।
  यह मॉड्यूलर दृष्टिकोण विभिन्न स्रोतों से प्राप्त ऊपरी और निचली सीमाओं को स्वतंत्र रूप से संयोजित करने की अनुमति देता है।
प्रमाण-वहन डेटाबेस (Proof-Carrying Database): यह शोध पत्र एक ऐसा डेटाबेस लागू करता है जहाँ संग्रहीत सीमाएँ केवल संख्यात्मक मान नहीं बल्कि "प्रमाण-वहन" (proof-carrying) वस्तुएं हैं। प्रत्येक प्रविष्टि में एक व्युत्पत्ति ट्रेस (derivation trace) शामिल है। इस ट्रेस को पुनः चलाने (replay) से Lean में संगत QaryKUpper या QaryKLower विधेय का एक औपचारिक प्रमाण पुनर्गठित होता है। प्रणाली हस्तलिखित गणितीय प्रमेयों (कर्नेल-चेक्ड) और जनरेट किए गए डेटा (अविश्वसनीय उत्पादक जिनका आउटपुट ट्रेस रिप्ले के माध्यम से मान्य किया जाता है) के बीच अंतर करती है।

प्रमुख योगदान
यह शोध पत्र मशीन-चेक्ड कवरिंग-कोड प्रमाणपत्रों के लिए एक पुन: प्रयोज्य, ऑडिट योग्य आधार स्थापित करता है। इसके विशिष्ट योगदान निम्नलिखित हैं:

औपचारिक बुनियादी ढांचा (Formal Infrastructure): परिमित हैमिंग स्पेस, हैमिंग दूरी, बंद बॉल्स (closed balls) और कवरिंग विधेयों के लिए एक पूर्ण Lean 4 फ्रेमवर्क, जो $q=0, n=0, r \ge n$ जैसे किनारों (edge cases) को अनौपचारिक परंपराओं के बजाय परिभाषाओं के भीतर कठोरता से संभालता है।
विश्लेषणात्मक परिणाम: $q$ -ary हैमिंग-बॉल वॉल्यूम फॉर्मूला और शास्त्रीय स्फीयर-कवरिंग निचली सीमा के औपचारिक प्रमाण। स्फीयर-कवरिंग बाउंड को एक कंप्यूट करने योग्य फंक्शन sphereLower के रूप में समाहित किया गया है जो प्रमाणित निचली-सीमा प्रमाणपत्र उत्पन्न करता है।
संरचनात्मक प्रमेय: प्रारंभिक सटीक मामलों (जैसे, $K_q(n,0) = q^n, K_q(n, n-1) = q$ ) का औपचारिकीकरण और संरचनात्मक निर्माण, जिसमें एक प्रोडक्ट कवरिंग प्रमेय और विभिन्न पड़ोसी संबंध (puncturing, lengthening, alphabet projection, और concatenation) शामिल हैं जो पैरामीटर ट्रिपल्स के बीच सीमाओं को स्थानांतरित करते हैं।
केस स्टडी (Van Laarhoven et al.): प्रकाशित स्पष्ट कोडों के औपचारिकीकरण का एक एंड-टू-एंड वर्कफ़्लो। लेखकों ने 1989 के एक पेपर (Van Laarhoven et al.) के कवरिंग कोड्स को Lean में ट्रांसक्राइब किया, उन्हें एलाबोरेशन सीमाओं से बचने के लिए पैक किए गए ऐरे (packed arrays) के रूप में एनकोड किया। प्रणाली ने कवरिंग गुण और कार्डिनैलिटी को सत्यापित किया, जिससे $K_3(6,1) \le 73, K_3(7,1) \le 186,$ और $K_3(8,1) \le 486$ के लिए मशीन-चेक्ड अपर-बाउंड प्रमाणपत्र उत्पन्न किए।
डेटाबेस कार्यान्वयन: 52,822 प्रविष्टियों वाला एक प्रमाण-वहन डेटाबेस, जिसमें $0 \le q \le 21, 0 \le n \le 48,$ और $0 \le r \le 48$ के लिए पैरामीटर्स हैं। इस डेटाबेस में छोटे मामलों के लिए सटीक प्रमाणपत्र (जैसे, $K_2(5,1)=7, K_3(3,1)=5$ ) और अंतराल (intervals) शामिल हैं जो ट्रेस रिप्ले से प्राप्त हुए हैं।

परिणाम
औपचारिकीकरण सफलतापूर्वक सत्यापित करता है:

$q$ -ary बॉल वॉल्यूम फॉर्मूला और स्फीयर-कवरिंग निचली सीमा।
$K_2(5,1)=7, K_2(6,2)=4, K_3(3,1)=5,$ और $K_4(3,1)=8$ जैसे प्रारंभिक सटीक मान।
स्पष्ट कोडों से प्राप्त टर्नरी फुटबॉल-पूल समस्या के लिए ऊपरी सीमाएं, विशेष रूप से $K_3(6,1) \le 73, K_3(7,1) \le 186,$ और $K_3(8,1) \le 486$ ।
एक समान टू-ब्लॉक साइक्लिक निर्माण जो $K_q(3,1) \le \lceil q^2/2 \rceil$ सिद्ध करता है।

डेटाबेस क्लोजर प्रक्रिया ने इन मूल स्रोतों को प्रमाणित संबंध नियमों के माध्यम से प्रसारित करके सीमाओं की एक सुसंगत तालिका उत्पन्न की। प्रणाली दो प्रमाण मोडों का समर्थन करती है: एक "कर्नेल मोड" जो मजबूत रिप्ले गारंटी के लिए मानक decide का उपयोग करता है, और एक "नेटिव मोड" जो तेज़ विकास के लिए Lean के कंपाइल्ड इवैल्यूएटर का उपयोग करता है, जिसमें स्पष्ट विश्वास सीमाएं (trust boundaries) परिभाषित हैं।

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

यह कार्य शास्त्रीय कवरिंग-कोड साहित्य और भविष्य के कम्प्यूटेशनल प्रमाणपत्रों के बीच के अंतर को पाटता है। ऊपरी-सीमा गवाहों (witnesses), निचली-सीमा तर्कों और सटीकता विधेयों को अलग करके, यह औपचारिकीकरण स्पष्ट निर्माणों, कॉम्बिनेटरियल काउंटिंग और (संभावित रूप से) भविष्य के SAT या इंटीजर-प्रोग्रामिंग सॉल्वर से प्राप्त परिणामों को एक एकल विश्वसनीय ढांचे के भीतर जांचने और संयोजित करने की अनुमति देता है। "प्रमाण-वहन" प्रकृति वाला डेटाबेस यह सुनिश्चित करता है कि प्रत्येक रिपोर्ट की गई सीमा को मशीन-चेक्ड प्रमाण तक ट्रैक किया जा सकता है, जो इस क्षेत्र में अंतर्निहित पुनरुत्पादकता और सत्यापन चुनौतियों को संबोधित करता है। यह शोध पत्र स्वयं को एक ऐसे भविष्य की ओर एक मौलिक कदम के रूप में प्रस्तुत करता है जहाँ कम्प्यूटेशनल खोज परिणामों को निर्बाध रूप से औपचारिक गणितीय पुस्तकालयों में एकीकृत किया जा सके।