Erdős Problem 275 #
References:
- erdosproblems.com/275
- [CrVE70] R.B. Crittenden and C.L. Vanden Eynden, Any n arithmetic progressions covering the first 2^n integers cover all integers, Proc. Amer. Math. Soc. 24 (1970), 475-481.
theorem
Erdos275.erdos_275
(r : ℕ)
(a : Fin r → ℤ)
(n : Fin r → ℕ)
(H : ∃ (k : ℤ), ∀ x ∈ Set.Ico k (k + 2 ^ r), ∃ (i : Fin r), x ≡ a i [ZMOD ↑(n i)])
(x : ℤ)
:
If a finite system of $r$ congruences $\{ a_i\pmod{n_i} : 1\leq i\leq r\}$ (the $n_i$ are not necessarily distinct) covers $2^r$ consecutive integers then it covers all integers.
This is best possible as the system $2^{i-1}\pmod{2^i}$ shows. This was proved independently by Selfridge and Crittenden and Vanden Eynden [CrVE70].
This was formalized in Lean by Alexeev using Aristotle.