erdős #275
If a finite system of congruences (the are not necessarily distinct) covers consecutive integers then it covers all integers.
Worked, still open.
number theory · solved · formalized (Lean) · 0 attempts
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsformal
AMS 11 · solved (literature)
theorem erdos_275 (r : ℕ) (a : Fin r → ℤ) (n : Fin r → ℕ)
(H : ∃ k : ℤ, ∀ x ∈ Ico k (k + 2 ^ r), ∃ i, x ≡ a i [ZMOD n i]) (x : ℤ) :
∃ i, x ≡ a i [ZMOD n i]formal-conjectures/275.lean ↗status
solved