Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 1188
claims/: The 2 claim pages of Problem 1188, one per claimant's result; the problem's standing derives from them.
Statement. Call a set of distinct integers with associated congruence classes a distinct covering system if every integer satisfies at least one of these congruences. A minimal distinct covering system is one such that no proper subset forms a covering system.
Let count the number of minimal distinct covering systems with all moduli in . Estimate .
Formulation. The site's question departs from Erdős's. The 1980 survey [Er80], printed p. 95, asks for the largest number of covering systems whose moduli are all distinct across the systems and below , and Erdős writes that he expects to tend to infinity very slowly; Hough's theorem [Ho15], that the least modulus of a covering system with distinct moduli is bounded, makes bounded, a negative answer to that expectation. A comment of 2026-04-17 by van Doorn on the discussion thread pointed this out, the curator agreed, and the site kept its reworded question about , whose commentary says that Erdős asked it without the minimality assumption. The standing below concerns the site's .
Status. Open. The site labels the problem OPEN (page last edited 17 April 2026, as of 2026-10-06). Its commentary records that , with the elementary bound from van Doorn's comment, the lower bound from the construction of Balister, Bollobás, Morris, Sahasrabudhe and Tiba, and the trivial upper bound ; the lower bound is an accepted partial claim on its claim page. The proof-claims tab carries one full claim, recorded without adoption on Snyder's claim page: , that is , placing near the trivial upper bound, with a Lean 4 proof in a downloadable bundle produced by the Star Fleet Math system running GPT 5.6 in a custom harness (accepted in Star Fleet Math's listing on 2026-07-12 and submitted to the site on 2026-07-15 by Colin Snyder). The standing is claimed through that pending full claim; this corpus has not built the Lean bundle, and no outside review is recorded.
Source. erdosproblems.com/1188 with its discussion thread (as of 2026-10-06: six comments in the discussion thread, one proof claim). Cite as: T. F. Bloom, Erdős Problem #1188, https://www.erdosproblems.com/1188.
References.
- [BBMST24] Balister, Paul and Bollobás, Béla and Morris, Robert and Sahasrabudhe, Julian and Tiba, Marius, The structure and number of Erd\H os covering systems. J. Eur. Math. Soc. (JEMS) (2024), 75-109.
- [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.
- [Ho15] Hough, Bob, Solution of the minimum modulus problem for covering systems. Ann. of Math. (2) (2015), 361-382.
Formalization. Statement in
formal-conjectures
(pinned to the commit of 2026-09-18), whose entry carries the category
research solved and a formal_proof attribute pointing to
starfleet/erdos-1188/Research/SparseAsymptotic.lean of Will Blair's
lean-proofs repository on GitHub at a pinned commit. That tree is a hosted
copy of Star Fleet Math's Lean proof, with the same final
theorem as the bundle linked on
Snyder's claim page,
where it is pinned; this corpus has built and audited none of it, so it
gives no formalized evidence and the problem stays claimed.
Current assessment
Open on the site; a pending claim fixes the scale of . The refereed lower bound , derived on the site from the construction of Balister, Bollobás, Morris, Sahasrabudhe and Tiba, is an accepted partial claim on its claim page. Snyder's claim that is pending on its claim page. Hough's theorem [Ho15] gets no claim page here: the site gives no derivation of from the minimum-modulus theorem, the curator called that theorem more than is needed in the discussion thread, and van Doorn's elementary bound on the thread already gives . No release item or lead names the problem.
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.