Kernel-Checked Exclusions for the Erdős-Selfridge Odd Covering Problem: Any Odd Covering of ℤ Has lcm Exceeding 10000
यह शोधपत्र एक पूर्णतः कर्नेल-सत्यापित (kernel-verified) लीन 4 (Lean 4) औपचारिकीकरण प्रस्तुत करता है जो यह सिद्ध करता है कि 1 से बड़ी विशिष्ट विषम माड्यूली (odd moduli) द्वारा पूर्णांकों का कोई भी परिमित आवरण (finite covering) का लघुत्तम समापवर्त्य (least common multiple) 10,000 से अधिक होगा, जिससे अनवेरिफाइड कम्प्यूटेशनल सॉल्वर पर निर्भर किए बिना एर्डोस-सेल्फ्रिज ऑड कवरिंग समस्या (Erdős-Selfridge odd covering problem) के लिए एक यांत्रिक रूप से प्रमाणित अपवर्जन (mechanically certified exclusion) स्थापित होता है।