{"id":"arxiv/2607.25628","url":"https://arxiv.org/abs/2607.25628","tags":["cs.LO","math.NT"],"score":0,"title":"Kernel-Checked Exclusions for the Erdős-Selfridge Odd Covering Problem: Any Odd Covering of $\\mathbb{Z}$ Has lcm Exceeding 10000","domain":"cs.LO","source":"arxiv","authors":["Ibrahim Mian","Shayaan Siddique"],"reviews":0,"subject":"cs.LO","summary":"The Erdős-Selfridge odd covering problem (Erdős problem #7) asks whether a covering system of $\\mathbb{Z}$ exists whose moduli are all odd, distinct, and greater than 1. The problem is open. We present a Lean 4 formalization, checked end to end by the proof kernel, of the exclusion: any covering of $\\mathbb{Z}$ by finitely many congruence classes with distinct odd moduli > 1 has lcm of the moduli exceeding 10000. The proof composes a formalized density argument (a covering by divisors of $N$ exceeding 1 forces $2N \\le σ_1(N)$, so the lcm is abundant or perfect), a kernel-checked abundancy…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-07-28","reactions":{}}