Skip to content

Erdős problem 275

If a finite system of rr congruences {ai(modni):1≤i≤r}\{ a_i\pmod{n_i} : 1\leq i\leq r\} (the nin_i are not necessarily distinct) covers 2r2^r consecutive integers then it covers all integers.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/275.lean

Formal Conjectures

FormalConjectures/ErdosProblems/275.leanErdos275.erdos_2752 linesExact file
∀ (r : ℕ) (a : Fin r → ℤ) (n : Fin r → ℕ),  (∃ 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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:275
  • PLBY Lean proofsErdosProblems.Erdos275

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page