Erdős problem 12
Let be infinite with no distinct such that with . Can have positive lower limit? Must every such fall below infinitely often?
Sources
FormalConjectures/ErdosProblems/
12.lean
Retained formal statement
Erdős and Sárközy proved that such an must have density 0. [ErSa70] Erdős, P. and Sárközi, A., On the divisibility properties of sequences of integers. Proc. London Math. Soc. (3) (1970), 97-101
∀ (A : Set ℕ), Erdos12.IsGood A → A.HasDensity 0SolvedStatement only, no proof