---

Claim. The answer to Problem 8 is no: there is a finite coloring of the integers such that no covering system has all its moduli of one color. The site credits the disproof to Hough's theorem that every finite covering system with pairwise distinct moduli greater than one has least modulus at most $10^{16}$, and gives the coloring: each integer from $1$ to $10^{16}$ receives its own color and every larger integer one further color, finitely many colors in all (the site's commentary writes $10^{18}$, the bound of Hough's arXiv v2; the published $10^{16}$ serves the same way). A covering system with monochromatic moduli would either have a single modulus $>1$, whose one residue class misses integers, or have all its moduli above the bound, which Hough's theorem forbids. The same theorem answers no to the density version that Erdős and Graham asked, whether $\sum_{a\in A,\,a>N}1/a\gg\log N$ forces $A$ to contain the moduli of a covering system: the set of all integers above the bound has a divergent reciprocal sum and contains no such moduli. The site's convention, and Hough's hypothesis, is that a covering system has finitely many pairwise distinct moduli greater than one.

Depends on. Hough's theorem supplies the whole content: it is the accepted disproof of Problem 2, and the coloring step above is the only addition.

Acceptance. Refereed: the theorem the disproof rests on is Hough's paper in the Annals of Mathematics (2) 181 (2015), no. 1, 361--382, doi:10.4007/annals.2015.181.1.6; the coloring deduction itself appears in no publication. Reviewed: the site's curator, Thomas Bloom, labels the problem disproved, names Hough's result as the reason and states the coloring in the problem's commentary (page last edited 5 April 2026, read 2026-10-07; the proof-claim tab is empty), and the community database records the problem disproved. Not listed as formalized: the site's label reads DISPROVED (LEAN) and the database carries formal status Lean as of that field's last update on 2026-08-24, without recording when that state was set; the catalog (google-deepmind/formal-conjectures) has no statement file for this problem, and the development behind the label is the file src/latest/ErdosProblems/Erdos8.lean in Boris Alexeev's lean-proofs repository, pinned above at the commit of 2026-09-15, which declares itself a formalization of a solution to Problem 8 with Hough as informal author and Codex and GPT-5.6 Sol as formal authors. It proves not_erdos_8, the negative answer, by the cutoff coloring from the minimum-modulus bound Erdos2.uniformMinimumBound of the repository's Problem 2 file, the formalization of the proof of Balister, Bollobás, Morris, Sahasrabudhe and Tiba linked on their claim page, and ends with #print axioms not_erdos_8; the file entered the repository on 2026-08-17 and its record page on 2026-08-22. Nothing was built or audited by this project, so the file gives no formalized evidence.

Not covered. The smallest number of colors that defeats every covering system. The site's thread (comments of 2026-01-31 and 2026-02-01) asks for it and reaches seven colors by combining the bound $616000$ of Balister, Bollobás, Morris, Sahasrabudhe and Tiba, on their claim page, with classes of reciprocal sum below one and divisor-free classes; these are thread posts, not a manuscript, and get no claim page.