Erdős problem 281

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

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

281.lean

Retained formal statement1 of 1

Let $n_1<n_2<\cdots$ be an infinite sequence such that, for any choice of congruence classes $a_i\pmod{n_i}$ , the set of integers not satisfying any of the congruences $a_i\pmod{n_i}$ has density $0$ . Is it true that for every $\epsilon>0$ there exists some $k$ such that, for every choice of congruence classes $a_i$ , the density of integers not satisfying any of the congruences $a_i\pmod{n_i}$ for $1\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

1True ↔2  ∀ (n : ℕ → ℕ),3    StrictMono n →4      (∀ (i : ℕ), 0 < n i) →5        (∀ (a : Erdos281.ResidueChoice n), (Erdos281.avoidAll n a).HasIntDensity 0) →6          ∀ (ε : ℝ),7            0 < ε → ∃ k, ∀ (a : Erdos281.ResidueChoice n), ∃ d, (Erdos281.avoidPrefix n a k).HasIntDensity d ∧ d < ε

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.