2026/07/28 by Ibrahim Mian, Shayaan Siddique
Computer Science · Mathematics · #cs.LO #math.NT
The Erdős-Selfridge odd covering problem (Erdős problem #7) asks whether a covering system of ℤ 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 ℤ 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 ≤ σ1(N), so the lcm is abundant or perfect), a kernel-checked abundancy floor (no odd N < 945 qualifies), a family of Chinese-Remainder capacity certificates -- decidable per-N arithmetic inequalities each refuting every covering with distinct moduli > 1 dividing that N -- for all 23 odd abundant numbers below 104, and a kernel-checked enumeration establishing that those 23 are the only odd non-deficient candidates. The result is transported to the official StrictCoveringSystem ℤ formulation of Erdős #7 in google-deepmind/formal-conjectures, with a bidirectional periodicity bridge between coverings of ℤ and finite checks over ℤ/Nℤ suitable for consuming future SAT-style search output. All 63 published theorems depend on exactly propext, Classical.choice, and Quot.sound: no sorry, no nativedecide, no solver in the trusted base. The mathematical content is known -- the density argument is folklore, and far larger uncertified classifications of covering numbers exist -- so the contribution is epistemic rather than mathematical: these exclusions are theorems of the Lean kernel, with an axiom gate enforced mechanically in continuous integration.