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?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

281.lean

Retained formal statement1 of 1

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?

The answer is yes; the linked Lean proof formalizes Somani's argument.

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.

Search problems.science

Find a Problem, Result, source, or page