Skip to content

Erdős problem 281

Let n1<n2<n_1<n_2<\cdots be an infinite sequence such that, for any choice of congruence classes ai(modni)a_i\pmod{n_i}, the set of integers not satisfying any of the congruences ai(modni)a_i\pmod{n_i} has density 00. Is it true that for every ϵ>0\epsilon>0 there exists some kk such that, for every choice of congruence classes aia_i, the density of integers not satisfying any of the congruences ai(modni)a_i\pmod{n_i} for 1ik1\leq i\leq k is less than ϵ\epsilon?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/281.lean

Formal Conjectures

FormalConjectures/ErdosProblems/281.leanErdos281.erdos_2817 linesExact file
True  ∀ (n : ℕ → ℕ),    StrictMono n      (∀ (i : ℕ), 0 < n i) →        (∀ (a : Erdos281.ResidueChoice n), (Erdos281.avoidAll n a).HasIntDensity 0) →          ∀ (ε : ℝ),            0 < ε → ∃ k, ∀ (a : Erdos281.ResidueChoice n), ∃ d, (Erdos281.avoidPrefix n a k).HasIntDensity dd < ε
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:281
  • PLBY Lean proofsErdosProblems.Erdos281

Reported activity

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

Continue

Search problems.science

Find a Problem, Result, source, or page