Erdős problem 275

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.

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

275.lean

Retained formal statement1 of 1

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.

FormalConjectures/ErdosProblems/275.leanErdos275.erdos_2752 linesExact file

1∀ (r : ℕ) (a : Fin r → ℤ) (n : Fin r → ℕ),2  (∃ k, ∀ x ∈ Set.Ico k (k + 2 ^ r), ∃ i, x ≡ a i [ZMOD ↑(n i)]) → ∀ (x : ℤ), ∃ i, x ≡ a i [ZMOD ↑(n i)]

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.