Erdős problem 486
For each choose some . Let . Must have a logarithmic density?
Sources
FormalConjectures/ErdosProblems/
486.lean
Retained formal statement
For each choose some . Let . Must have a logarithmic density?
True ↔ ∀ (X : (n : ℕ) → Set (ZMod n)), ∃ d, {m | ∀ (n : ℕ), ↑m ∉ X n}.HasLogDensity dOpenStatement only, no proof