Erdős Problem 8: monochromatic moduli in covering systems

### What is the conjecture

https://www.erdosproblems.com/8

Let a covering system be a finite collection of congruences
$a_i \pmod{d_i}$ covering all integers. For any finite colouring
of $\mathbb{Z}$, does there exist a covering system all of whose
moduli $d_i$ are monochromatic?

Erdős and Graham further ask a density analogue: if $A \subset \mathbb{N}$
satisfies $\sum_{a \in A, a > N} 1/a \gg \log N$, does $A$ contain
the moduli of a covering system?

Status: disproved. Hough [Ho15] established a uniform bound on the
minimum modulus in a covering system. In particular, colouring all
integers $<10^{18}$ distinctly and all others with a new colour
provides a counterexample to both versions.

**Sources:**
- https://www.erdosproblems.com/8
- [Er80, ErGr80, Er96b, Er97] as cited therein
- [Ho15] B. Hough, Solution of the minimum modulus problem for covering systems

### Prerequisites needed
Covering-system definitions, finite colourings/partitions, summability
and density lemmas. No Mathlib infrastructure for covering systems yet;
likely requires new definitions in `FormalConjecturesForMathlib/`.

### AMS categories
* ams-11

### Choose either option
- [X] I plan on adding this Erdős problem to the repository

Start by reviewing the existing structure under FormalConjecturesForMathlib/ and the stated prerequisites for covering systems, finite colourings, summability, and density. Define the needed concepts before formalizing the Erdős Problem 8 statement and its disproved status; done means the new Lean formalization is accepted by the repository checks.

Written by the indexing model from the issue text.