Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 2
claims/: The 4 claim pages of Problem 2, one per claimant's result; the problem's standing derives from them.
Statement. Can the smallest modulus of a covering system be arbitrarily large?
Statement (corrected). Can the smallest modulus of a covering system with distinct moduli be arbitrarily large?
Notes. The site's wording drops the condition, assumed by the problem's sources, that the moduli are distinct; the literature uses the bare term both ways. If repeated moduli are allowed, the answer is trivially yes: for every , the residue classes modulo any single cover the integers. This trivial cover is the corpus's own observation, and no result about the site's wording is recorded. The change inserts "with distinct moduli"; nothing else changes. The evidence is the literature's statement of the problem as Erdős's. Nielsen, A covering system whose smallest modulus is 40 ([[../library/covering_systems/nielsen_2009_covering_system_smallest_modulus_40/_index|J. Number Theory 129 (2009)]], abstract, p. 1 of the author version), a construction that settles nothing: "Paul Erdős, in 1950, asked whether for each positive integer there exists a finite set of congruence classes, with distinct moduli, covering the integers, whose smallest modulus is ." Hough [Ho15], §1, printed p. 361: "From [4], the minimum modulus problem asks whether there exist distinct covering systems for which the least modulus is arbitrarily large", where [4] is Erdős's 1950 paper and a distinct covering system is a finite collection of congruences with covering every integer. [BBMST22], abstract, printed p. 378: "Erdős asked if the moduli can be distinct and all arbitrarily large"; their §1 (printed p. 378) defines a covering system as any finite collection of arithmetic progressions that covers the integers, so in their usage the term alone does not carry distinctness. Hough and BBMST state the problem apart from their theorems' hypotheses, and the site's commentary, which credits Hough's bound , the bound and Owens's cover with minimum modulus , fits only the distinct reading. Erdős's 1950 paper also prints the distinctness: its conjecture on p. 120 concerns systems of congruences with that cover every integer (result page [[../library/primes/erdos_1950_integers_form_related_problems/conjecture_p120|Erdős 1950, p. 120]]). Whether the site's sources [Er55c] to [Er97e] print it is not recorded here.
Formulation. A covering system with distinct moduli is a finite family of residue classes with pairwise distinct moduli whose union is , as in the formal-conjectures statement; a modulus would make the smallest modulus . The question asks whether, for every natural number , such a system exists with smallest modulus greater than . Finiteness matters: enumerate the integers as , choose distinct primes , and the infinite family covers every integer; every source cited in the Notes defines a covering system as finite. No irredundancy condition is imposed on the finite covers in this question.
Status. DISPROVED (LEAN), the site's label: Hough's published theorem gives an absolute upper bound for the minimum modulus. The later published BBMST bound gives , equivalently . The largest achievable minimum modulus is unidentified in the literature search. The two proofs are recorded on their claim pages, Hough and Balister, Bollobás, Morris, Sahasrabudhe and Tiba, each accepted on its refereed publication and the site's credit. Two refereed results on restricted classes are accepted partial claims: Filaseta, Ford, Konyagin, Pomerance and Yu bound the minimum modulus when the reciprocal sum of the moduli is bounded, and Cummings, Filaseta and Trifonov bound it by when every modulus is squarefree. The site's Lean badge is qualified below.
Source. erdosproblems.com/2, accessed 2026-09-05. Cite as: T. F. Bloom, Erdős Problem #2, https://www.erdosproblems.com/2.
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. 228 (2022), 377–414.
- [FFKPY07] Filaseta, Michael and Ford, Kevin and Konyagin, Sergei and Pomerance, Carl and Yu, Gang, Sieving by large integers and covering systems of congruences. J. Amer. Math. Soc. 20 (2007), 495–517.
- [Ho15] Hough, Bob, Solution of the minimum modulus problem for covering systems. Ann. of Math. (2) 181 (2015), no. 1, 361–382.
- [Ow14] Owens, Tyler, A Covering System with Minimum Modulus 42. Master of Science thesis, Brigham Young University (2014).
- [KKL24] Klein, Jonah and Koukoulopoulos, Dimitris and Lemieux, Simon, On the j-th smallest modulus of a covering system with distinct moduli. Int. J. Number Theory 20 (2024), 471–479.
Formalization. The site's linked artifact is a catalog statement of the
qualitative answer whose theorem body is sorry; the development
behind the site's Lean label is a lean-proofs file formalizing the proof of
Balister, Bollobás, Morris, Sahasrabudhe and Tiba, linked at a pinned commit
on their claim page. See Formalization and verification scope below for the
pinned revisions and public-build limits. This corpus has built neither
file.
Current assessment
The site's wording (page last edited 5 April 2026) asks whether the smallest modulus of a covering system can be arbitrarily large; for covering systems with distinct moduli, the Statement judged here, the answer is no. The status rests on Hough's accepted Annals paper, not a site label. Its published version and actual arXiv v3 state ; v2 states , and v1 gives an unspecified absolute bound. The abstract in the arXiv record's metadata gives . The source digest distinguishes the four versions.
The BBMST paper appeared online in November 2021 and in the April 2022 Inventiones issue. Its published version has 38 pages and is canonical; the 2018 arXiv v1 has 30 pages. Owens's construction is a December 2014 Master of Science thesis at Brigham Young University.
The search covered primary papers and preprints, author material, later construction records and public formalization repositories. It located no later general improvement of the interval below. Sun's 6 May 2026 Graz lecture, slide 7, distinguishes the general threshold from the squarefree bound . The July 2026 Zhang–Zhang preprint records Owens's in its introduction; its new question concerns the smallest least common multiple at fixed minimum modulus . Other located 2026 work restricts prime support or optimizes the number of classes at a fixed small minimum. Those are different extremal questions. This search does not establish that no unpublished improvement exists.
The compiled proof scopes are detailed in Known results and proof routes below; Owens's construction is not verified in this corpus.
Known results and proof routes
Let be the largest minimum modulus attained by a finite distinct cover with moduli greater than one. The published upper bound and Owens's reported construction give
This is a maximum, since attainable minima are integers in a bounded, nonempty set. The interval records the best general bounds located in the search above; it does not identify . The lower construction's proof is not reconstructed in this corpus.
| Source | Contribution | Compiled proof scope |
|---|---|---|
| Filaseta–Ford–Konyagin–Pomerance–Yu (2007) | Theorem A: positive uncovered density when the reciprocal sum of the moduli, all greater than , is at most , so a bounded reciprocal sum forces a bounded minimum modulus; an accepted partial claim on its claim page. | Statement recorded, proof not compiled. |
| Hough (2015), Theorem 1 | Every finite distinct cover has . | Complete ordinary proof and finite numerical certificate, relative to the stated explicit prime estimate. |
| Owens (2014) | A finite distinct cover with . | Source construction recorded; the construction is not verified in this corpus. |
| Balister–Bollobás–Morris–Sahasrabudhe–Tiba (2022), Theorem 8.1 | Distinct moduli all at least cannot cover. | Complete ordinary computer-assisted proof with an independently replayed rational certificate, relative to the explicit Dusart prime bound. |
Hough filters the moduli by primes, uses a relative Lovász local lemma on surviving residue fibers, and controls how reweighting changes the bias statistics. The library's [[../library/covering_systems/hough_2015_solution_minimum_modulus_problem_covering_systems/qualitative_theorem_1|qualitative proof]], a compilation expansion of his self-contained method, already disproves the conjecture using elementary prime-counting bounds, without a numerical certificate. The explicit proof also uses [[../library/covering_systems/hough_2015_solution_minimum_modulus_problem_covering_systems/lemma_7|prime-band estimates]] and the [[../library/covering_systems/hough_2015_solution_minimum_modulus_problem_covering_systems/numerical_certificate|finite certificate]]. The full relative local lemma and essential same-paper deductions are compiled at their canonical pages as author-recorded proof coverage; no independent review of that compilation is recorded in this repository.
BBMST gives a different proof through controlled distortion of a probability measure. Its [[../library/covering_systems/balister_2018_erdos_covering_problem_density_uncovered_set/theorem_1_1|Theorem 1.1]] bounds the uncovered density for sufficiently large distinct moduli. The positive bound depends on the family through a weighted reciprocal sum; it is not a fixed positive density depending only on the minimum modulus. The explicit bound uses first moments through the prime , refined second moments through the -th prime, and a termination criterion. The [[../library/covering_systems/balister_2018_erdos_covering_problem_density_uncovered_set/numerical_bounds|exact numerical reconstruction]] uses a legal rational parameter schedule and proves a sufficient threshold. It does not claim to reproduce every unused printed digit in the paper's numerical table. The complete same-paper deductions, certificate reduction and checker are author-recorded; no independent review of that compilation is recorded in this repository. External inputs and source clarifications are stated on the result pages.
Related refinements
Klein–Koukoulopoulos–Lemieux prove that the -th smallest modulus of every minimal distinct cover with at least classes satisfies
for an absolute constant . Here minimal means no proper subfamily of the fixed residue classes still covers. Their [[../library/covering_systems/klein_2023_jth_smallest_modulus_covering_system/theorem_1|Theorem 1]] and its essential same-paper inputs are compiled as author-recorded proof coverage; no independent review of that compilation is recorded in this repository. The unspecified constant does not improve the explicit bound at . This rank restriction also bears on Problem 1188, without estimating the number of minimal covers.
Cummings–Filaseta–Trifonov prove the stronger minimum bound when every modulus is squarefree, Theorem 1.1 of arXiv 2211.08548v1, published in Acta Mathematica Hungarica 175 (2025), 1–25. The proof is not checked in this corpus. This restricted bound does not replace the general one; it is an accepted partial claim on its claim page. Similarly, Hough–Nielsen's divisibility theorem forces some modulus to be divisible by or , without requiring a modulus equal to either prime. It does not resolve the odd-cover question Problem 7.
Formalization and verification scope
The site's formalization link points to a formal-conjectures statement. At
the
revision
of 4 September 2026, the declaration Erdos2.erdos_2 expresses the qualitative negative answer
using StrictCoveringSystem ℤ, but its proof is a single sorry.
The definitions require a finite index, nonzero proper ideal moduli,
coverage of all integers and injective moduli. The positive generators
therefore give the intended pairwise distinct integer moduli greater
than one. No numerical upper bound occurs in that declaration.
The introducing PR
#4313, merged
on 26 August 2026, explicitly describes a statement formalization. The
successful public build of the
revision
on 4 September is compatible with the retained proof placeholder and does not
establish a formal proof. On 5 September 2026 the site's label was DISPROVED
(LEAN), but its linked artifact supports statement-only scope. The development
behind the label is the file src/latest/ErdosProblems/Erdos2.lean in Boris
Alexeev's lean-proofs repository, which declares itself a formalization of a
solution to Problem 2 with Balister, Bollobás, Morris, Sahasrabudhe and Tiba
as informal authors and Codex and GPT-5.6 Sol as formal authors, proves
erdos_2 by the distortion sieve with the bound , and is linked at a
pinned commit on
their claim page;
the repository's Problem 8 file builds on it. This corpus has not built or
kernel-checked it, so it gives no formalized evidence.
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.
- erdos_1957_unsolved_problems
- erdos_1957_unsolved_problems / problem_14
- balister_2018_erdos_covering_problem_density_uncovered_set
- balister_2018_erdos_covering_problem_density_uncovered_set / sieve_construction
- balister_2018_erdos_covering_problem_density_uncovered_set / theorem_10_1
- balister_2018_erdos_covering_problem_density_uncovered_set / theorem_1_1
- balister_2018_erdos_covering_problem_density_uncovered_set / theorem_3_1
- balister_2018_erdos_covering_problem_density_uncovered_set / theorem_5_1
- balister_2018_erdos_covering_problem_density_uncovered_set / theorem_8_1
- cochrane_1996_covering_congruences_higher_dimensions
- cochrane_1996_covering_congruences_higher_dimensions / odd_even_composite_cover
- cochrane_1996_covering_congruences_higher_dimensions / other_constructions_and_questions
- filaseta_2001_coverings_integers_schinzel_irreducibility
- filaseta_2001_coverings_integers_schinzel_irreducibility / open_problem_1
- harrington_2015_two_questions_covering_systems
- harrington_2015_two_questions_covering_systems / question_1_4
- harrington_2015_two_questions_covering_systems / section_4_construction
- hough_2015_solution_minimum_modulus_problem_covering_systems
- hough_2015_solution_minimum_modulus_problem_covering_systems / initial_stage
- hough_2015_solution_minimum_modulus_problem_covering_systems / lemma_2
- hough_2015_solution_minimum_modulus_problem_covering_systems / lemma_4
- hough_2015_solution_minimum_modulus_problem_covering_systems / lemma_5
- hough_2015_solution_minimum_modulus_problem_covering_systems / lemma_7
- hough_2015_solution_minimum_modulus_problem_covering_systems / numerical_certificate
- hough_2015_solution_minimum_modulus_problem_covering_systems / proposition_1
- hough_2015_solution_minimum_modulus_problem_covering_systems / proposition_3
- hough_2015_solution_minimum_modulus_problem_covering_systems / qualitative_theorem_1
- hough_2015_solution_minimum_modulus_problem_covering_systems / relative_local_lemma
- hough_2015_solution_minimum_modulus_problem_covering_systems / sieve_setup
- hough_2015_solution_minimum_modulus_problem_covering_systems / theorem_1
- hough_2015_solution_minimum_modulus_problem_covering_systems / theorem_2
- hough_2015_solution_minimum_modulus_problem_covering_systems / theorem_6
- klein_2023_jth_smallest_modulus_covering_system
- klein_2023_jth_smallest_modulus_covering_system / claim_2_1
- klein_2023_jth_smallest_modulus_covering_system / theorem_1
- klein_2023_jth_smallest_modulus_covering_system / theorem_2
- klein_2023_jth_smallest_modulus_covering_system / theorem_3
- nielsen_2009_covering_system_smallest_modulus_40
- nielsen_2009_covering_system_smallest_modulus_40 / arrow_finitization
- nielsen_2009_covering_system_smallest_modulus_40 / construction_ledger
- nielsen_2009_covering_system_smallest_modulus_40 / initial_primes_2_7
- nielsen_2009_covering_system_smallest_modulus_40 / later_signature_certificate
- nielsen_2009_covering_system_smallest_modulus_40 / main_theorem
- nielsen_2009_covering_system_smallest_modulus_40 / notation
- nielsen_2009_covering_system_smallest_modulus_40 / prime_11_template
- nielsen_2009_covering_system_smallest_modulus_40 / prime_13_template
- nielsen_2009_covering_system_smallest_modulus_40 / prime_17_template
- nielsen_2009_covering_system_smallest_modulus_40 / prime_19_template
- nielsen_2009_covering_system_smallest_modulus_40 / prime_23_template
- nielsen_2009_covering_system_smallest_modulus_40 / primes_29_37
- nielsen_2009_covering_system_smallest_modulus_40 / primes_41_67
- nielsen_2009_covering_system_smallest_modulus_40 / primes_71_103
- nielsen_2009_covering_system_smallest_modulus_40 / template_signature_certificate
- owens_2014_covering_system_minimum_modulus_42
- owens_2014_covering_system_minimum_modulus_42 / imported_templates_11_23
- owens_2014_covering_system_minimum_modulus_42 / main_theorem
- sun_2005_introduction_papers_covers
- sun_2005_introduction_papers_covers / result_p7
- filaseta_2007_sieving_large_integers_covering_systems_congruences
- filaseta_2007_sieving_large_integers_covering_systems_congruences / theorem_2
- filaseta_2007_sieving_large_integers_covering_systems_congruences / theorem_a
- filaseta_2007_sieving_large_integers_covering_systems_congruences / theorem_b
- dusart_1999_kth_prime_lower_bound
- dusart_1999_kth_prime_lower_bound / theorem_3
- erdos_1950_integers_form_related_problems
- erdos_1950_integers_form_related_problems / conjecture_p120