Erdős problem 281
Let be an infinite sequence such that, for any choice of congruence classes , the set of integers not satisfying any of the congruences has density . Is it true that for every there exists some such that, for every choice of congruence classes , the density of integers not satisfying any of the congruences for is less than ?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/281.leanTrue ↔ ∀ (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 d ∧ d < εProof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:281 - PLBY Lean proofs
ErdosProblems.Erdos281
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
AI alongside literature
- Machine
Formalization
- Machine
New proofs
argument
- Machine
- Reported outcome