🔢 mathematics

A Lean-Certified Proof of $K_8(4, 2) = 23$

यह शोध पत्र लीन 4 (Lean 4) में एक पूर्णतः औपचारिक प्रमाण प्रस्तुत करता है कि ऑक्टनरी कवरिंग कोड मान $K_8(4, 2)$ का मान 23 है, जो एक स्पष्ट 23-शब्दों वाले कोड के माध्यम से ऊपरी सीमा (upper bound) और फाइबर-गिनती तर्कों को LRAT-खंडित CNF इंस्टेंस के साथ संयोजित करके यह प्रदर्शित करने के माध्यम से निचली सीमा (lower bound) स्थापित करता है कि कोई भी 22-शब्दों वाला कवर अस्तित्व में नहीं हो सकता।

मूल लेखक: Andreas Florath

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

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

CC BY 4.0

मूल लेखक: Andreas Florath

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

कल्पना कीजिए कि आप लाखों बिंदुओं से भरे एक विशाल, चार-आयामी (four-dimensional) कमरे में "सुरक्षा जालों" (safety nets) का एक सेट पैक करने की कोशिश कर रहे हैं। लक्ष्य यह सुनिश्चित करना है कि कमरे का प्रत्येक बिंदु कम से कम एक सुरक्षा जाल से एक छोटी दूरी (मान लीजिए, दो कदम) के भीतर हो।

प्रश्न जो गणितज्ञों ने पूछा है वह यह है: पूरे कमरे को कवर करने के लिए आपको वास्तव में न्यूनतम कितने सुरक्षा जालों की आवश्यकता होगी?

एक विशिष्ट प्रकार के कमरे के लिए (जहाँ प्रत्येक आयाम में 8 संभावित मान हैं), उत्तर को एक बहुत ही संकीर्ण सीमा में सीमित कर दिया गया है: यह या तो 22 जाल या 23 जाल है। एंड्रियास फ्लोरथ द्वारा लिखा गया यह शोध पत्र निर्णायक रूप से सिद्ध करता है कि 23 ही वह जादुई संख्या है। आप 22 के साथ इसे नहीं कर सकते।

यह प्रमाण कैसे काम करता है, यहाँ सरल उपमाओं में दिया गया है:

1. दो-भाग वाला प्रमाण

यह सिद्ध करने के लिए कि उत्तर ठीक 23 है, लेखक को दो चीजें करनी पड़ीं, जैसे यह सिद्ध करना कि दरवाजा दोनों तरफ से बंद है:

ऊपरी सीमा (Upper Bound - यह दिखाना कि 23 काम करता है): लेखक ने बस 23 सुरक्षा जालों की एक विशिष्ट सूची बनाई और उन्हें कमरे के प्रत्येक बिंदु के विरुद्ध जांचा। यह ऐसा है जैसे कहना, "यहाँ 23 फायर स्टेशनों का एक नक्शा है; मैंने हर सड़क पर चलकर पुष्टि की है कि कोई भी घर किसी स्टेशन से दो ब्लॉक से अधिक दूर नहीं है।" इस भाग को सत्यापित करना आसान है क्योंकि लेखक ने केवल सूची दिखाई है।
निचली सीमा (Lower Bound - यह दिखाना कि 22 विफल रहता है): यह कठिन हिस्सा है। उन्हें यह सिद्ध करना था कि केवल 22 जालों से कमरे को कवर करना असंभव है। आप 22 जालों के हर संभव संयोजन को नहीं देख सकते क्योंकि वे बहुत अधिक हैं (ब्रह्मांड के परमाणुओं से भी अधिक)। इसके बजाय, उन्होंने एक चतुर तर्क का उपयोग किया जिससे यह सिद्ध हुआ कि 22 जालों का कोई भी प्रयास अनिवार्य रूप से एक छेद छोड़ देगा।

2. "लापता जोड़ी" का जासूसी कार्य (The "Missing Pair" Detective Work)

22 जालों को पर्याप्त सिद्ध करने के लिए, लेखक ने सीधे जालों को नहीं देखा। इसके बजाय, उन्होंने उस पर ध्यान दिया जो लापता था।

कल्पना कीजिए कि कमरा एक विशाल ग्रिड है। यदि आप किन्हीं दो निर्देशांकों (जैसे "फ्लोर" और "वॉल") को चुनते हैं, तो आप उन मानों की जोड़ियों को देख सकते हैं जो जालों में दिखाई देती हैं।

तर्क: यदि मानों की एक विशिष्ट जोड़ी (जैसे, "फ्लोर 3, वॉल 5") आपके किन्हीं भी 22 जालों में एक साथ कभी नहीं आती है, तो वह एक "लापता जोड़ी" (missing pair) है।
ग्राफ: लेखक ने प्रत्येक निर्देशांक के जोड़े के लिए एक मानचित्र (ग्राफ) बनाया, जिसमें "लापता" संयोजनों को चिह्नित किया गया।
विरोधाभास: प्रमाण यह दिखाता है कि यदि आपके पास केवल 22 जाल हैं, तो ज्यामिति के नियम इन "लापता जोड़ी" मानचित्रों को एक विशिष्ट, वर्जित आकार—एक "क्लिक" (clique - एक कसा हुआ गांठ जैसा संबंध)—बनाने के लिए मजबूर करते हैं। लेकिन यदि वह आकार मौजूद है, तो इसका मतलब है कि कमरे में एक ऐसा बिंदु है जो आपके किसी भी जाल से बहुत दूर है। इसलिए, 22 जाल कमरे को कवर नहीं कर सकते।

3. "ब्लॉक" पहेली

जब लेखक ने उस मामले का विश्लेषण किया जहाँ कोई व्यक्ति ठीक 22 जालों का उपयोग करने का प्रयास करता है, तो उन्होंने पाया कि जालों को एक बहुत ही कठोर, ब्लॉक जैसी संरचना (विशेष रूप से एक 3 + 3 + 2 पैटर्न) में व्यवस्थित होना होगा।

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

4. "लीन" (Lean) कंप्यूटर चेक

यहीं पर यह शोध पत्र उच्च-तकनीकी हो जाता है। क्योंकि "लापता जोड़ी" का तर्क हजारों छोटी संभावनाओं (जैसे लाखों सेल वाले सुडोकू पहेली) की जाँच करने से जुड़ा है, इसलिए लेखक ने लीन (Lean) नामक एक कंप्यूटर प्रोग्राम का उपयोग किया।

SAT सॉल्वर: लेखक ने एक शक्तिशाली कंप्यूटर प्रोग्राम (एक SAT सॉल्वर) का उपयोग किया ताकि संभावनाओं की विशाल सूची की जाँच की जा सके और यह कहा जा सके कि "यह विशिष्ट व्यवस्था असंभव है।"
प्रमाणपत्र (The Certificate): आमतौर पर, हमें कंप्यूटर पर भरोसा करना होता है। लेकिन यहाँ, कंप्यूटर ने केवल यह नहीं कहा कि "असंभव"। इसने एक प्रमाणपत्र (इसके तर्क की एक चरण-दर-चरण रसीद) भी तैयार किया।
सत्यापन: लीन प्रोग्राम ने फिर उस रसीद को पढ़ा और कंप्यूटर के तर्क के प्रत्येक चरण को स्वयं सत्यापित किया। इसका मतलब है कि यह प्रमाण मशीन-चेक किया गया (machine-checked) है। हमें कंप्यूटर के दिमाग पर भरोसा करने की आवश्यकता नहीं है; हमें केवल लीन प्रोग्राम की उस रसीद को पढ़ने की क्षमता पर भरोसा करना है, जो बहुत छोटी और सत्यापित करने में आसान है।

सारांश

यह शोध पत्र सिद्ध करता है कि इस विशिष्ट चार-आयामी कमरे के लिए (जिसमें प्रत्येक आयाम में 8 विकल्प हैं):

23 जाल पर्याप्त हैं (यहाँ सूची दी गई है)।
22 जाल पर्याप्त नहीं हैं (यहाँ एक तार्किक प्रमाण है कि 22 जालों का उपयोग करने का कोई भी प्रयास एक अपरिहार्य अंतराल पैदा करता है)।

परिणाम एक "लीन-प्रमाणित" (Lean-Certified) प्रमाण है, जिसका अर्थ है कि पूरा तर्क—बड़े तर्क से लेकर छोटे कंप्यूटर चेक तक—एक औपचारिक गणितीय सॉफ्टवेयर सिस्टम द्वारा सत्यापित किया गया है, जिससे मानवीय त्रुटि या संदेह की कोई गुंजाइश नहीं बचती। उत्तर ठीक 23 है।

तकनीकी सारांश: $K_8(4,2) = 23$ का लीन-प्रमाणित (Lean-Certified) प्रमाण

समस्या विवरण
यह शोध पत्र सटीक कवरिंग संख्या (covering number) $K_q(n,r)$ के निर्धारण को संबोधित करता है, जिसे $q$ -आरी हैमिंग स्पेस (q-ary Hamming space) में लंबाई $n$ के रेडियस- $r$ कवरिंग कोड के न्यूनतम आकार के रूप में परिभाषित किया गया है। विशेष रूप से, यह ऑक्टोनरी (octonary) मामले के लिए मान को हल करता जहाँ लंबाई 4 और रेडियस 2 है: $K_8(4,2)$ । इस कार्य से पूर्व, मौजूदा अंतराल (विशेष रूप से केरी (Kéri) की तालिकाएँ) इस मान को $[22, 23]$ के अंतराल में रखते थे। निचला मान रोडमिच रूक-डोमेन (Rodemich rook-domain) बाउंड से प्राप्त किया गया था, जबकि ऊपरी मान बड़े वर्णमाला (large-alphabet) बाउंड द्वारा समर्थित था। इसका उद्देश्य निचली सीमा को सिद्ध करके इस अंतराल को बंद करना था: $K_8(4,2) \ge 23$ ।

कार्यप्रणाली
प्रमाण को mathlib लाइब्रेरी का उपयोग करते हुए Lean 4 थ्योरम प्रूवर में औपचारिक रूप दिया गया है। यह एक "प्रमाण-वाहक" (proof-carrying) दृष्टिकोण अपनाता है जहाँ परिणाम को दो स्वतंत्र प्रमाणों के माध्यम से स्थापित किया जाता है: एक स्पष्ट ऊपरी सीमा (explicit upper bound) और एक संरचनात्मक निचली सीमा (structural lower bound)।

ऊपरी सीमा ( $K_8(4,2) \le 23$ ):
लेखक $(\text{Fin } 8)^4$ में 23 कोडवर्ड्स वाला एक स्पष्ट कोड प्रदान करते हैं। औपचारिक प्रमाण दो शर्तों को सत्यापित करता है: सेट का कार्डिनैलिटी (cardinality) 23 से अधिक नहीं है, और एम्बिएंट स्पेस (ambient space) का प्रत्येक शब्द (4096 शब्द) कम से कम एक कोडवर्ड के हैमिंग डिस्टेंस 2 के भीतर है। यह एक व्यापक परिमित जाँच (exhaustive finite check) है।
निचली सीमा ( $K_8(4,2) \ge 23$ ):
शोध पत्र का मुख्य भाग किसी भी काल्पनिक कवर $C^*$ के लिए एक संरचनात्मक गैर-अस्तित्व तर्क (non-existence argument) है, जहाँ $|C^*| \le 22$ हो। प्रमाण कटौती (reductions) की एक श्रृंखला के माध्यम से आगे बढ़ता है:

फाइबर काउंटिंग (Fiber Counting): एक काल्पनिक कवर के लिए, लेखक "फाइबर्स" $C^*_{i,a}$ (कोऑर्डिनेट $i$ पर सिंबल $a$ वाले कोडवर्ड्स) को परिभाषित करते हैं। वे सिद्ध करते हैं कि प्रत्येक फाइबर में कम से कम दो कोडवर्ड होने चाहिए। यह प्रति कोऑर्डिनेट 16 कोडवर्ड्स ( $8 \text{ symbols} \times 2$ ) का आधार स्थापित करता है, जिससे $|C^*|=22$ के मामले के लिए अधिकतम 6 अतिरिक्त कोडवर्ड का "बजट" (या $|C^*| \le 21$ के लिए 5) बचता है।
मिसिंग-पेयर ग्राफ (Missing-Pair Graphs): प्रमाण एक "विपरीत" दृष्टिकोण की ओर स्थानांतरित होता है, जो यह विश्लेषण करता है कि कोड के कोऑर्डिनेट जोड़ों पर प्रोजेक्शन से कौन से प्रतीक जोड़े गायब हैं। ये गायब जोड़े ग्राफ $E_{ij}$ बनाते हैं।
मामला $|C^*| \le 21$ : छोटे अतिरिक्त बजट का उपयोग करते हुए, लेखक यह प्रदर्शित करते हैं कि कॉम्बिनेटरियल काउंटिंग के माध्यम से मिसिंग-पेयर ग्राफ को एक "एक साथ चार-पार्टाइट क्लीक" (simultaneous four-partite clique) (चार प्रतीकों $a,b,c,d$ का एक सेट जहाँ सभी छह कोऑर्डिनेट जोड़े गायब हैं) को शामिल करना चाहिए। लेम्मा 7 सिद्ध करता है कि ऐसा क्लीक एक वैध रेडियस-2 कवर में मौजूद नहीं हो सकता, जिससे 21 या उससे कम आकार के कवर खारिज हो जाते हैं।
मामला $|C^*| = 22$ : शेष मामले के लिए, प्रमाण समस्या को मिसिंग-पेयर ग्राफ के "प्रोफाइल" (profile) के एक परिमित वर्गीकरण में बदल देता है। लेखक दिखाते हैं कि कोई भी वैध प्रोफाइल एक विशिष्ट "कॉमन $3+3+2$ ब्लॉक स्ट्रक्चर" प्रदर्शित करेगा।
SAT/LRAT एकीकरण: इन प्रोफाइल्स का वर्गीकरण मैन्युअल गणना के लिए बहुत बड़ा है। लेखक बाधाओं (रो/कॉलम डिग्री बाउंड और नो-क्लीक कंडीशन) को कंजंक्टिव नॉर्मल फॉर्म (CNF) इंस्टेंस में एनकोड करते हैं। वे अनट्रस्टेड (untrusted) SAT सॉल्वर का उपयोग करके लीनियर RAT (LRAT) रिफ्यूटेशन (असंतुष्टता के प्रमाण) उत्पन्न करते हैं।
औपचारिक सत्यापन (Formal Verification): Lean इन LRAT प्रमाणों को पार्स करता है और यांत्रिक रूप से रिफ्यूटेशन को फिर से चलाकर (replay) यह सिद्ध करता है कि 22-शब्दों वाले कवर के लिए कोई वैध प्रोफाइल मौजूद नहीं है।
अंतिम विरोधाभास (Final Contradiction): भले ही एक सामान्य ब्लॉक स्ट्रक्चर को माना जाए, लेखक संरचना के "2-सिंबल कंपोनेंट" में एक विरोधाभास निकालते हैं। इस कंपोनेंट को अधिकतम 4 पंक्तियों के साथ लंबाई 4 वाले बाइनरी स्ट्रेंथ-2 ऐरे (binary strength-2 array) की आवश्यकता होगी, जो गणितीय रूप से असंभव है।

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

सटीक मान: शोध पत्र सटीक मान $K_8(4,2) = 23$ स्थापित करता है, जिससे पहले से ज्ञात अंतराल $[22, 23]$ बंद हो जाता है।
औपचारिक निचली सीमा: यह 22-शब्दों वाले सभी कवर्स को बाहर करने के लिए Lean 4 में एक पूर्णतः औपचारिक प्रमाण प्रदान करता है। यह वॉल्यूम तर्कों के बजाय फाइबर काउंट और मिसिंग-पेयर ग्राफ से प्राप्त संरचनात्मक बाधाओं द्वारा प्राप्त किया गया है।
प्रमाण-वाहक आर्टिफैक्ट (Proof-Carrying Artifact): परिणाम को एक लीन आर्टिफैक्ट के रूप में पैकेज किया गया है जिसमें स्पष्ट कोड, संरचनात्मक लेम्मा, CNF इंस्टेंस और LRAT रिफ्यूटेशन शामिल हैं। महत्वपूर्ण रूप से, SAT सॉल्वर विश्वसनीय कंप्यूटिंग बेस (trusted computing base) का हिस्सा नहीं है; Lean आंतरिक रूप से LRAT प्रमाणों को सत्यापित करता है।
कंप्यूटेशनल लोअर बाउंड्स के लिए पैटर्न: शोध पत्र कवरिंग-कोड लोअर बाउंड्स के लिए प्रमाण-वाहक कम्प्यूटेशनल साक्ष्य जोड़ने के लिए एक पुन: प्रयोज्य पैटर्न पेश करता है। यह "डिस्कवरी" (अनट्रस्टेड सॉल्वर) को "सत्यापन" (ट्रस्टेड लीन कर्नेल) से अलग करता है, जिससे बड़े परिमित वर्गीकरण समस्याओं को औपचारिक शुद्धता बनाए रखते हुए कम्प्यूटेशनल रूप से हल किया जा सके।

परिणाम
प्राथमिक परिणाम प्रमेय $K_8(4,2) = 23$ है।

ऊपरी सीमा: एक स्पष्ट 23-शब्दों वाले कोड द्वारा सिद्ध।
निचली सीमा: यह दिखाकर सिद्ध कि 22-शब्दों वाला कवर एक विरोधाभास की ओर ले जाता है, जो एक मजबूर "कॉमन $3+3+2$ ब्लॉक सिस्टम" की ओर ले जाता है जो एक असंभव बाइनरी ऐरे की उपस्थिति को दर्शाता है।
प्रदर्शन: औपचारिक सत्यापन के लिए महत्वपूर्ण कम्प्यूटेशनल संसाधनों की आवश्यकता होती है। मुख्य प्रूफ फ़ाइल के कर्नेल-मोड रीप्ले के लिए लगभग 143 GiB RAM की आवश्यकता थी, जबकि नेटिव मोड ने इसे घटाकर लगभग 5.5 GiB कर दिया। कर्नेल मोड में LRAT चेकिंग चरण में लगभग 17 मिनट लगे।

महत्व और दावे
यह शोध पत्र मुख्य रूप से औपचारिक गणित और कम्प्यूटेशनल प्रमाणों के साथ कॉम्बिनेटरियल तर्क को संयोजित करने की कार्यप्रणाली के क्षेत्र में अपनी महत्ता का दावा करता है।

मेथोडोलॉजिकल शिफ्ट: यह प्रदर्शित करता है कि संरचनात्मक कॉम्बिनेटरिक्स को "प्रूफ-कैरिंग" कम्प्यूटेशनल साक्ष्य के साथ कैसे जोड़ा जा सकता है। SAT सॉल्वर का उपयोग परिमित बाधाओं की खोज के लिए किया जाता है, लेकिन गणितीय सेतु और सॉल्वर के आउटपुट का सत्यापन पूरी तरह से थ्योरम प्रूवर द्वारा किया जाता है।
ट्रस्ट बाउंड्री (Trust Boundary): यह कार्य SAT सॉल्वरों वाले औपचारिक प्रमाणों में विश्वास की सीमा को स्पष्ट करता है। सॉल्वर अनट्रस्टेड है; लीन कर्नेल LRAT प्रमाणों और उस तार्किक निष्कर्ष की जांच करता है जो इन प्रमाणों को कवरिंग कोड कथन से जोड़ता है।
स्केलेबिलिटी: यह परिणाम उन कवरिंग-कोड समस्याओं को संभालने के लिए एक टेस्ट केस के रूप में कार्य करता है जो मैन्युअल प्रमाण के लिए बहुत बड़ी हैं लेकिन SAT सॉल्वर द्वारा हल की जा सकने वाली परिमित वर्गीकरण समस्याओं के रूप में पर्याप्त छोटी हैं।
कोई नया अनुप्रयोग नहीं: शोध पत्र $K_8(4,2)=23$ के स्वयं के नए अनुप्रयोगों का दावा नहीं करता है, न ही कोई नए प्रायोगिक प्रोटोकॉल प्रस्तावित करता है। इसका योगदान कोडिंग थ्योरी तालिकाओं में एक विशिष्ट खुली समस्या के समाधान और ऐसी समस्याओं के लिए एक औपचारिक सत्यापन वर्कफ़्लो के प्रदर्शन में निहित है।

1. दो-भाग वाला प्रमाण

2. "लापता जोड़ी" का जासूसी कार्य (The "Missing Pair" Detective Work)

3. "ब्लॉक" पहेली

4. "लीन" (Lean) कंप्यूटर चेक

सारांश

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