Maximum minimum modulus of a distinct covering system

Description of constant

A distinct covering system is a finite collection of residue classes

\[\mathcal C=\{a_i+n_i\mathbb Z:1\le i\le k\}, \qquad a_i\in\mathbb Z,\quad 1<n_1<\cdots<n_k, \qquad \bigcup_{i=1}^{k}(a_i+n_i\mathbb Z)=\mathbb Z.\]

The classes may overlap; distinctness refers to their moduli. Define

\[C_{90}:=\max_{\mathcal C}\min_{1\le i\le k}n_i =\max_{\mathcal C}n_1.\]

The family is nonempty: for example, the classes $0\pmod 2$, $0\pmod 3$, $1\pmod 4$, $1\pmod 6$, and $11\pmod {12}$ cover all integers. Hough’s theorem [H2015] bounds the minimum modulus uniformly, so the attainable minimum moduli form a nonempty bounded set of positive integers. Consequently the maximum exists and is attained.

As of October 2026, the strongest known bounds are

\[44\le C_{90}<616000, \qquad\text{equivalently}\qquad 44\le C_{90}\le615999.\]

The lower bound 44 is an unrefereed, machine-checked construction [M2026], marked with an asterisk below; the previous record is 42, from Owens’s MS thesis [O2014], which later literature cites as the best known construction [B2024, §2]. The exact value remains unknown. Erdős’s original minimum modulus problem asked whether the minimum could be arbitrarily large [E1950]. Hough settled that question negatively; determining the optimal finite bound remains open.

Known upper bounds

Bound Reference Comments
$\le 10^{16}$ [H2015], Theorem 1, p. 362 First universal finite bound. Uses a sieve and the Lovász local lemma, with numerical estimates. Preprint announced in 2013; published in 2015.
$<616000$ (hence $\le615999$) [BBMST2022], Theorem 8.1; open preprint §8 The theorem rules out a finite cover when every modulus is at least 616000. Distortion method with explicit moment estimates and numerical calculations. Preprint appeared in 2018; journal publication in 2022.

Known lower bounds

Bound Reference Comments
$2$ Elementary example above All classes are periodic modulo 12. The even residues are covered modulo 2; the odd residues 1, 3, 5, 7, 9, 11 are covered by the remaining four classes.
$9$ [Ch1968]; history in [N2009], §1 Churchhouse’s construction. Historical attribution checked through Nielsen’s introduction; original chapter not inspected.
$18$ [K1971], Chapter V, Example 5.6, pp. 68–73; history in [N2009], §1 Krukenberg’s construction, with $N=2^7\cdot3^3\cdot5^2\cdot7^2\cdot11^2\cdot13^2\cdot17^2\cdot19$ (p. 73). Many congruences are carried over or generated from Example 5.5 (pp. 43–68). Original dissertation inspected; the covering itself has not been independently verified.
$20$ [Choi1971], Theorems 4–13, pp. 886–895; history in [N2009], §1 Choi’s construction, obtained independently of Krukenberg’s work. Not an explicit list: Theorems 5–13 (pp. 888–890, proofs tabulated on pp. 890–895) build a $\mathbb Z$-good set of index 20, and Theorem 4 (pp. 886–888) converts it into a covering with distinct moduli. Original paper inspected; the covering itself has not been independently verified.
$24$ [M1981a], §2, pp. 1–3; [M1981b], Theorem 5, pp. 8–9; history in [N2009], §1 Morikawa’s construction. [M1981a] tabulates a skeleton covering with least modulus 24 generated by $\langle 2,3,5,7,11,13,17,19,23\rangle$; [M1981b], Theorem 5, guarantees a finite covering set with the same generators. Theorem 5 is an existence result, so the papers give no explicit list of congruences for the final covering. Original papers inspected; the covering has not been independently verified.
$25$ [G2006]; [G2009], §6, Theorem 1, p. 1143 Computer-assisted construction reported in Gibson’s 2006 dissertation and published in 2009. Propositions 1 and 2 (§§2–3) convert almost covers into covers; §§4–6 describe the computer search and its result. The published paper was inspected; the dissertation was checked only through its institutional abstract.
$40$ [N2009], §§3–4 Finite construction encoded with prime trees and up-arrow notation; §3 supplies the covering principle and §4 the construction.
$42$ [O2014], Chapter 3, pp. 2–17 Owens’s MS thesis improves the record from 40 to 42. Construction extends Nielsen’s method and uses Nielsen’s notation (Chapter 2, pp. 1–2). Chapter 3 builds the covering prime by prime, §§3.1–3.20, using the primes from 2 through 89 (Figure 4.1, p. 19). Original thesis inspected; the covering has not been independently verified.
$44$* [M2026], theorem UC85.minimumModulus44 Lean 4 proof that a covering system with distinct moduli and least modulus exactly 44 exists. The construction starts from a variant of Owens’s system, extends it to least modulus 43 and then 44, and has 618,413 families of congruences on 47 primes, completed to a finite system with the fresh prime 223. The axioms used are only propext, Classical.choice and Quot.sound. Coverage was also checked by two independent SAT encodings with checked unsatisfiability proofs. Asterisked: the proof is about 8,000 Lean files (roughly 250 CPU-hours to build), is available only in a personal GitHub repository, and is neither refereed nor registered with a verification service. Commit c904210.

The rows preserve the history of the claims; the 2006 thesis date places Gibson’s construction before Nielsen’s 2009 publication. Source inspection is distinguished from independent verification: the large constructions and numerical upper-bound calculations have not been independently replayed for this page.

References

Contribution notes

Prepared with assistance from OpenAI Codex and Claude Opus 5.5 for literature searches, citation checks against the original sources, and drafting. The human contributor has reviewed and verified the references and the statements attributed to them against the original sources, except for [Ch1968], which was unavailable.

← Back to the table of constants