🔢 mathematics

A Kernel-Checked Exclusion Certificate for Erd\H{o}s Problem 647

यह शोध पत्र लीन 4 (Lean 4) में एक पूर्णतः सत्यापित, स्वयंसिद्ध-न्यूनतम (axiom-minimized) प्रमाण प्रस्तुत करता है जो गुणनखंड साक्ष्यों (factorization witnesses) को श्रृंखलाबद्ध करके $n > 24$ से $10^9$ तक के सभी मानों के लिए एर्दोश समस्या 647 (Erdős Problem 647) को हल करता है, और परिणाम की विश्वसनीयता को कई स्वतंत्र टूलचेन और आर्किटेक्चर के बीच बाइट-तुल्य (byte-identical) पुनरुत्पादन द्वारा सुदृढ़ किया गया है।

मूल लेखक: Ibrahim Mian, Shayaan Siddique

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

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

CC BY 4.0

मूल लेखक: Ibrahim Mian, Shayaan Siddique

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

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

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

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

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

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

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

तकनीकी सारांश: एर्डोस समस्या 647 के लिए एक कर्नेल-जांचा गया अपवर्जन प्रमाण-पत्र (Exclusion Certificate)

समस्या विवरण
एर्डोस समस्या 647, जिसे एर्डोस और सेल्फ्रिज ने प्रस्तुत किया था, यह पूछती है कि क्या कोई ऐसा पूर्णांक $n > 24$ मौजूद है जहाँ $\max_{m<n} (m + \tau(m)) \le n + 2$ हो, जहाँ $\tau(m)$ विभाजक-गणना फलन (divisor-count function) है। जबकि यह स्थिति $n=24$ के लिए सत्य है, और $n+2$ की सीमा सटीक (tight) है, यह अनुमान लगाया गया है कि इसके बाद और कोई समाधान मौजूद नहीं हैं। पिछले कम्प्यूटेशनल खोजों ने सेगमेंटेड सीव्स (segmented sieves) और मॉड्यूलर रिडक्शन का उपयोग करके $n \approx 9.17 \times 10^{18}$ तक समाधानों को बाहर कर दिया है। हालाँकि, ये गणनाएँ अनवेरिफाइड कोड, नेटिव decide टैक्टिक्स, या समस्या-विशिष्ट अभिगृयों (axioms) पर निर्भर करती हैं, जो उन्हें औपचारिक सत्यापन प्रणालियों (formal verification systems) के विश्वसनीय प्रमाण कर्नेल (trusted proof kernel) से बाहर रखती हैं।

कार्यप्रणाली और प्रमाण-पत्र डिज़ाइन
यह शोध पत्र $24 < n \le 10^9$ के लिए समाधानों को बाहर करने के लिए लीन 4 (Lean 4) में एक औपचारिक प्रमाण प्रस्तुत करता है। यह प्रमाण एक "विटनेस-चेन" (witness-chain) प्रमाण-पत्र प्रारूप पर आधारित है जिसे प्रत्येक संख्या के पूर्ण गुणनखंडन (full factorization) की आवश्यकता के बिना लीन कर्नेल द्वारा कुशलतापूर्वक जांचा जा सकता है।

विटनेस परिभाषा: एक लक्षित $n$ के लिए एक "किल विटनेस" (kill witness) $m$ को एक ऐसे पूर्णांक के रूप में परिभाषित किया गया है जहाँ $m < n$ और $m + \tau(m) \ge n + 3$ है। ऐसा विटनेस अंतराल $[m+1, m + \tau(m) - 3]$ के लिए असमिका (inequality) को खंडित करता है।
स्मूथ पार्ट ऑप्टिमाइज़ेशन: कर्नेल वर्कलोड को कम करने के लिए, विटनेस पूर्ण गुणनखंडन को संग्रहीत नहीं करते हैं। इसके बजाय, वे $m$ $m$ को विभाजित करने वाले प्रत्येक अभाज्य $p < 1024$ $p < 1024$ की अधिकतम घात (maximal power) को संग्रहीत करते हैं।
- कर्नेल यह सत्यापित करता है कि संग्रहीत अभाज्य घातों का गुणनफल $m$ को विभाजित करता है।
- यह सत्यापित करता है कि प्रत्येक संग्रहीत घात अधिकतम है (अर्थात, $p^{e+1} \nmid m$ )।
- यह $\tau(m)$ के लिए एक निचला स्तर (lower bound) $\prod (e_i + 1)$ के रूप में कंप्यूट करता है।
- डबलिंग नियम (The Doubling Rule): यदि $m$ का शेष कोफैक्टर (वह भाग जो $1024 $से कम के अभाज्य भागों द्वारा विभाजित नहीं है)$ 1$ से अधिक है, तो बाउंड को दोगुना कर दिया जाता है। यह तर्कसंगत है क्योंकि कोफैक्टर स्मूथ भाग के सह-अभाज्य (coprime) है; यदि वह मौजूद है, तो वह कम से कम दो विभाजकों (1 और स्वयं को) में योगदान देता है।
- सूचीबद्ध अभाज्य संख्याओं की अभाज्यता (primality) को 31 तक के अभाजों द्वारा ट्रायल डिवीजन के माध्यम से सत्यापित किया जाता है, जिसके लिए किसी बाहरी अभाजता प्रमाण-पत्र की आवश्यकता नहीं होती।
ग्रीडी चेनिंग (Greedy Chaining): प्रमाण-पत्र विटनेस का एक अनुक्रम है जो ग्रीडी तरीके से उत्पन्न किया गया है। कवर स्थिति 24 से शुरू करते हुए, एल्गोरिदम एक ऐसा विटनेस $m \le C$ चुनता है जो नए कवर पद $m + \tau(m) - 3$ को अधिकतम करता है। यह 6,685,922 विटनेस की एक श्रृंखला पूरे अंतराल $(24, 10^9]$ को कवर करती है।
औपचारिकीकरण संरचना (Formalization Structure): लीन विकास "साउंडनेस लेयर" (जो चेकर के तर्क को सिद्ध करती है) और "डेटा लेयर" (जो विटनेस सूचियों को रखती है) को अलग करता है। डेटा को लीन सोर्स फाइलों में लिटरल्स (literals) के रूप में एनकोड किया गया है। कर्नेल चेन निरंतरता और बाउंड्स की वैधता को सत्यापित करने के लिए इन लिटरल्स का मूल्यांकन करता है।

मुख्य योगदान और सत्यापन
यह शोध पत्र सत्यापन के पांच विशिष्ट स्तर प्रदान करता है:

अक्सिओम क्लोजर (Axiom Closure): अंतिम प्रमेय को ठीक $\{ \text{propext}, \text{Classical.choice}, \text{Quot.sound} \}$ के अक्सिओम क्लोजर के साथ सिद्ध किया गया है। इसमें कोई sorry, कोई native decide, या कोई समस्या-विशिष्ट अभिगृहीत नहीं है।
स्वतंत्र रीप्ले (Independent Replay): जनरेटर स्क्रिप्ट को स्पष्ट रूप से अविश्वसनीय माना गया है। एक दूसरा, स्वतंत्र पायथन कार्यान्वयन, अभाजता, क्रम और डबलिंग नियम को सत्यापित करने के लिए प्रत्येक विटनेस को पुनः चलाकर (replay) देखता है। तीसरा कार्यान्वयन स्वतंत्र रूप से विभाजक फलन को पुन: कंप्यूट करता है और पुष्टि करता है कि समाधान सेट OEIS A087280 से मेल खाता है।
स्रोत-से-पुनरुत्पादन (From-Source Reproducibility): दो अलग-अलग x86 हार्डवेयर पर कंपाइल किए गए स्वतंत्र सत्यापन चरणों ने, gcc और clang का उपयोग करके लीन टूलचेन को स्रोत से बनाया, बिना कैश के mathlib और विकास को फिर से बनाया, और प्रमाण-पत्र फ़ाइलों को पुन: उत्पन्न किया। परिणामी .olean फ़ाइलें मूल ARM बिल्ड के बाइट-दर-बाइट समान थीं, जिनका SHA-256 डाइजेस्ट भी समान था।
स्टैंडअलोन चेकिंग: संकलित विकास को lean4checker का उपयोग करके पुनः टाइपचेक किया गया था, जिससे संकलित आर्टिफैक्ट्स की अखंडता की पुष्टि हुई।
दोषपूर्ण डिज़ाइन का सुधार: पेपर एक डिज़ाइन इटरेशन का दस्तावेजीकरण करता है जहाँ एक जनरेटर "गैप मिनिमम" पर रुक गया था क्योंकि वह यह ध्यान नहीं रख पाया कि एक बड़े अभाज ( $>1024$ ) द्वारा विभाजक गणना को आधा करने पर डबलिंग नियम कैसे लागू होता है। मैक्सिमलिटी-और-डबलिंग नियम के समावेश ने इसे हल कर दिया, जो साउंडनेस-प्रिजर्विंग स्ट्रेंथनिंग में "फेल-लाउड" जनरेशन के महत्व को प्रदर्शित करता है।

परिणाम
प्राथमिक परिणाम प्रमेय 1.1 है: कोई भी पूर्णांक $n$ के साथ $24 < n \le 10^9$ इस शर्त को संतुष्ट नहीं करता है कि $\max_{m<n} (m + \tau(m)) \le n + 2$ ।

यह प्रमाण $6,685,922 $विटनेस की एक श्रृंखला का उपयोग करके अंतराल$ (24, 10^9]$ को कवर करता है।
$10^9$ के लिए प्रमाण-पत्र लगभग 260 MB का सोर्स कोड है, जिसे वर्ज़न्ड रिलीज़ आर्टिफैक्ट के रूप में भेजा गया है।
$10^7$ और $10^8$ रेंज को निरंतर एकीकरण (CI) में लागू किया गया है; $10^9$ रेंज को clang टूलचेन के तहत एक बार कर्नेल-चेक किया गया और स्वतंत्र रीप्ले पाइपलाइन के माध्यम से सत्यापित किया गया।

महत्व और दायरा
पेपर स्पष्ट रूप से कहता है कि यह एर्डोस समस्या 647 को बंद नहीं करता है, न ही यह उन शोधकर्ताओं (Idén, Hughes, bentrd) के कम्प्यूटेशनल फ्रंटियर्स तक पहुँचने का दावा करता है, जो $10^{18}$ तक विस्तृत हैं।

ट्रस्ट बनाम रेंज: योगदान ट्रस्ट बेस (विश्वास आधार) है, न कि रेंज। यह परिणाम $(24, 10^9]$ की सीमा में गैर-अस्तित्व के सत्यापन को अनवेरिफाइड कम्प्यूटेशन से एक कर्नेल-चेक किए गए प्रमाण में स्थानांतरित करता है।
परिमित बनाम अनंत (Finite vs. Asymptotic): यह कार्य एक जनवरी 2026 के वापस लिए गए दावे के विशिष्ट अंतर को संबोधित करता है। वह दावा "डोमिनेशन इंटरवल्स" के माध्यम से सभी $n > 24$ को कवर करने का प्रयास करता था, लेकिन यह सिद्ध करने में विफल रहा कि अंतराल अनंत रूप से ओवरलैप होते हैं। यह पेपर दर्शाता है कि उस तर्क का परिमित रूप (एक सीमित सीमा को कवर करना) एक ऐसा तथ्य है जिसे एक प्रमाण कर्नेल हल कर सकता है।
भविष्य की सीमाएँ: लेखक नोट करते हैं कि यह विधि प्रमाण-पत्र के आकार और कर्नेल समय से सीमित है, न कि गणित से। $10^{10}$ तक विस्तार करने के लिए ~2 GB सोर्स की आवश्यकता होगी, और $10^{12}$ इस प्रतिनिधित्व के साथ अव्यवहार्य होगा। भविष्य के कार्यों के लिए संरचनात्मक तर्कों के बजाय मॉड्यूलर रिडक्शन को प्रमाणित करने की आवश्यकता होगी।

संक्षेप में, यह पेपर प्रमाणित खोज के लिए एक नया मानक स्थापित करता है: एक परिमित, पूरी तरह से सिद्ध अपवर्जन जो केवल लीन कर्नेल और मानक अभिगृयों पर निर्भर करता है, जो जनरेटर की विश्वसनीयता से स्वतंत्र है।

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