1. FormalConjectures
  2. ErdosProblems
  3. «281»
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Erdős Problem 281

References:

    erdosproblems.com/281

    [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

    [DaEr36] Davenport, H. and Erdős, P., On sequences of positive integers. Acta Arithmetica (1936), 147-151.

    [HaRo66] Halberstam, H. and Roth, K. F., Sequences. Vol. I. (1966), xx+291.

open Filter Topology namespace Erdos281

Choices of congruence classes $a_i \pmod{n_i}$.

def ResidueChoice (n : ℕ → ℕ) := ∀ i : ℕ, ZMod (n i)

The integers avoiding all congruences $a_i \pmod{n_i}$.

def avoidAll (n : ℕ → ℕ) (a : ResidueChoice n) : Set ℤ := {m | ∀ i : ℕ, (m : ZMod (n i)) ≠ a i}

The integers avoiding the first $k$ congruences $a_i \pmod{n_i}$.

def avoidPrefix (n : ℕ → ℕ) (a : ResidueChoice n) (k : ℕ) : Set ℤ := {m | ∀ i : ℕ, i < k → (m : ZMod (n i)) ≠ a i}

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.

@[category research solved, AMS 11, formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos281.lean"] theorem declaration uses 'sorry'erdos_281 : answer(True) ↔ ∀ (n : ℕ → ℕ), StrictMono n → (∀ i, 0 < n i) → (∀ a : ResidueChoice n, Set.HasIntDensity (avoidAll n a) 0) → ∀ ε : ℝ, 0 < ε → ∃ k : ℕ, ∀ a : ResidueChoice n, ∃ d : ℝ, Set.HasIntDensity (avoidPrefix n a k) d ∧ d < ε := ⊢ True ↔ ∀ (n : ℕ → ℕ), StrictMono n → (∀ (i : ℕ), 0 < n i) → (∀ (a : ResidueChoice n), (avoidAll n a).HasIntDensity 0) → ∀ (ε : ℝ), 0 < ε → ∃ k, ∀ (a : ResidueChoice n), ∃ d, (avoidPrefix n a k).HasIntDensity d ∧ d < ε All goals completed! 🐙 end Erdos281