Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 7

claims/: The 7 claim pages of Problem 7, one per claimant's result; the problem's standing derives from them.

Statement. Is there a distinct covering system all of whose moduli are odd?

Formulation. A distinct covering system is a finite family of congruence classes $a_i\pmod{n_i}$ with pairwise distinct moduli $n_i>1$ that covers every integer. This is how the site defines the term in Problem 1188 (“distinct integers $1<n_1<\cdots<n_k$ ”) and how the formal-conjectures statement encodes it. The question asks whether one exists with every $n_i$ odd. The bound $n_i>1$ matters, since the single class $0\pmod1$ covers every integer with an odd modulus.

Status. Verifiable, the site's label for this open question. The exact unrestricted question is not settled by the finite exclusions below. Two full disproof claims from the site's discussion thread are recorded on claim pages, one rejected and one conditional on an unproved axiom; four refereed exclusions of classes of odd coverings are accepted partial claims, by Berger, Felzenbaum and Fraenkel for at most five primes, by Hough and Nielsen and by Balister, Bollobás, Morris, Sahasrabudhe and Tiba for the square-free case and the period divisible by 9 or 15. The Mian–Siddique exclusion of periods up to $10000$ , with third-party Lean, is a pending partial claim. None settles the question, so the derived standing is open.

Source. erdosproblems.com/7, accessed 2026-09-05. Cite as: T. F. Bloom, Erdős Problem #7, https://www.erdosproblems.com/7.

References.

[BBMST22] Balister, Paul and Bollobás, Béla and Morris, Robert and Sahasrabudhe, Julian and Tiba, Marius, On the Erdős covering problem: the density of the uncovered set. Invent. Math. (2022), 377-414.
[FFK00] Filaseta, M. and Ford, K. and Konyagin, S., On an irreducibility theorem of A. Schinzel associated with coverings of the integers. Illinois J. Math. 44 (2000), no. 3, 633-643.
[HoNi19] Hough, Robert D. and Nielsen, Pace P., Covering systems with restricted divisibility. Duke Math. J. (2019), 3261-3295.
[Sc67] Schinzel, A., Reducibility of polynomials and covering systems of congruences. Acta Arith. 13 (1967), 91-101.

Formalization. Statement in formal-conjectures at the revision of 2026-10-06, which states the question as erdos_7 with answer(sorry) and a sorry body and carries no formal_proof attribute.

Current assessment

The site's formulation (page last edited 22 January 2026) asks whether a finite covering system with distinct odd moduli greater than one exists. The site's label is VERIFIABLE and its proof-claim listing for the problem is empty. The label is a note on an open problem, not a claim: a positive answer could be witnessed by a finite covering system with distinct odd moduli, checked over one period of its moduli, and no such covering has been found.

The problem's discussion thread holds two full claims of a negative answer, both posted as comments rather than on the proof-claim tab. The Lean development posted on 2026-01-11, generated with Archivara and Aristotle, derives the negative answer from the Hough–Nielsen theorem and an unproved axiom, and is the conditional claim on its claim page. The note and Lean development posted on 2026-05-02, audited by Aristotle, rested on an axiom shown false as encoded four days later; the author conceded and the site's curator closed technical discussion, so the claim is rejected on its claim page. Neither changes the standing.

The search covered the July 2026 Mian–Siddique preprint, a pending partial claim on its claim page, the source repository and public CI run pinned on its source record, the February 2026 McNew–Setty revision, and the Hough–Nielsen paper, and located no accepted resolution. The Mian–Siddique theorem is explicitly partial. Its background claim of a complete covering-number classification through one million is overstated: the actual McNew–Setty table leaves 773500 unresolved, as documented in the linked source digest.

The finite period exclusion, the square-free obstruction, the period restriction to multiples of 9 or 15 and the six-prime necessary condition below have complete ordinary proof chains. The square-free proof and the finite exclusion include reproducible arithmetic certificates. The Hough–Nielsen theorem is recorded at statement level. The finite exclusion's Lean development is third-party; this corpus has not built or audited it.

Known Results

Every distinct nontrivial covering has a modulus divisible by 2 or 3, by Hough and Nielsen. Thus a hypothetical odd covering must involve a modulus divisible by 3. The library records the statement; the proof is not compiled. The result is an accepted partial claim on its claim page.
Every finite distinct cover with square-free moduli greater than one has an even modulus, by Balister, Bollobás, Morris, Sahasrabudhe and Tiba's Theorem 1.1 (2021). The paper notes on p. 625 that its proof needs square-freeness only at the primes up to $73$ (extension). So a hypothetical distinct odd cover must contain a modulus divisible by $p^2$ for some odd prime $p\le73$ . The complete geometric sieve proof includes exact finite certificates and settles the square-free special case of this problem, an accepted partial claim on its claim page.
The period of a distinct covering, the least common multiple of its moduli, is divisible by 2, 9 or 15, by Balister, Bollobás, Morris, Sahasrabudhe and Tiba's Theorem 1.4 (2022), whose Theorem 7.1 is a simpler proof of the Hough–Nielsen theorem. Thus a hypothetical distinct odd cover has period divisible by 9 or by 15; the alternative 15 may come from different moduli divisible by 3 and by 5. The result is an accepted partial claim on its claim page.
The least common multiple of the moduli of a hypothetical distinct odd cover must have at least six distinct odd prime divisors, by Berger, Felzenbaum and Fraenkel's six-prime corollary (1987). Its full proof uses the earlier prime-adic box correspondence and a forest correction to a union bound. The corollary excludes every distinct odd cover whose moduli involve at most five primes, so the period is at least $3\cdot5\cdot7\cdot11\cdot13\cdot17=255255$ ; it is an accepted partial claim on its claim page. Six is not asserted to be the best known lower bound.
Any hypothetical distinct odd covering has least common multiple greater than 10000. The complete finite-exclusion proof combines density, all 23 non-deficient odd candidate periods, and Chinese remainder capacity bounds. Mian and Siddique identify the mathematical bound as known and provide a Lean formalization. It is not a solution of this problem or a claim that 10000 is the best known necessary bound: the six-prime corollary above already gives period at least $255255$ . The result is a pending partial claim on its claim page; this corpus has not built the Lean.

Formalization evidence

The upstream link above formalizes the problem statement. Separately, Mian and Siddique's source record pins a public development of the finite exclusion and a successful public CI run. Its bridge uses a local mirror of the upstream ideal vocabulary. The ordinary mathematical equivalence is supplied here, but neither a fresh Lean build nor a checked port into the upstream project is asserted.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

Linked from (122)

Problem 2 Six distinct primes in the period of an odd covering Hough and Nielsen's modulus divisible by two or three The period of an odd covering is divisible by 9 or 15 The square-free case has no odd covering The Archivara and Aristotle candidate disproof under a good-fibre axiom Lee's sieve-monotonicity disproof with a false axiom Mian and Siddique's exclusion of odd periods up to 10000 problems/covering_systems/E0007/claims No covering system has a divisibility-free set of moduli Covering Systems additive_combinatorics/erdos_1957_unsolved_problems Problem 14 (p. 295): covering systems with distinct moduli above n_0, and with odd moduli Covering Systems covering_systems/balister_2018_erdos_covering_problem_density_uncovered_set Lemma 6.2: the one-step survival recurrence Prime-stage distortion measures Theorem 1.2 — Schinzel's divisibility conjecture Theorem 1.3: the external square-free obstruction Theorem 1.4 — a divisibility restriction on the covering period Theorem 3.1: noncoverage and uncovered density Theorem 6.1: a termination criterion for the covering sieve Theorem 7.1: a modulus divisible by two or three The Erdős–Selfridge problem with square-free moduli Corollary 5.2: the sufficient bound at the prime 73 Lemma 2.1: preservation and distortion of the sieve measure Lemma 3.3: measure of a specified hyperplane Lemma 3.4: expansion of the fibre moments Lemma 4.2: a sufficient product condition for a hyperplane cover Lemma 5.3: processing the primes from 13 through 73 Lemma 5.4: a probability measure after the first four odd primes Proposition 4.1: covers beyond every fixed initial segment Remark on page 625: square-freeness only at primes at most 73 Theorem 1.1: an even modulus in every distinct square-free cover Theorem 1.2: no nonparallel cover of an odd-prime box Theorem 1.3: Hough’s minimum-modulus theorem in geometric form Theorem 1.4: a fixed initial segment in linearly growing boxes Theorem 3.1: the moment criterion for noncoverage Theorem 3.2: first and second moment bounds Theorem 5.1: the imported large-prime termination criterion Necessary condition for odd incongruent coverings The first necessary condition for distinct odd coverings Theorem — the product-set covering obstruction Corollary — covers of finite nilpotent groups Prime-adic digit and coset correspondence Prime-factor consequences of the first obstruction Remark — comparison with Selfridge's condition Necessary condition for odd incongruent coverings II Block reduction — enlarging and saturating the family Forest lemma — a union bound with intersection savings

Graph