Erdős Problem #7 — Covering systems with all moduli odd

Erdős and Selfridge asked whether the integers can be covered by finitely many residue classes with distinct, odd moduli greater than $1$. The unrestricted question remains unanswered.

Known results

• Hough and Nielsen proved that at least one modulus is divisible by $2$ or $3$.
• Balister, Bollobás, Morris, Sahasrabudhe, and Tiba ruled out the case of odd squarefree moduli.
• The same authors showed that any odd covering would have least common multiple divisible by $9$ or $15$.
• McNew and Setty classified covering numbers up to $10^6$.

2026 formalized exclusion

A Lean $4$ formalization proves that any such covering would have least common multiple exceeding $10^4$, via density and abundancy arguments plus checked exclusions below $10^4$. It verifies known partial mathematics and does not prove nonexistence. A separate repository claims a resolution, but its stated theorem only establishes the same lower bound and is contradicted by the official formalization and paper’s open status.

Current status (as of July 2026): The problem is open; the strongest supplied recent progress is a formally verified lower bound exceeding $10^4$ for the least common multiple of any hypothetical covering.