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
Let be a set of natural numbers with the property that there are no distinct such that and . If all elements in are pairwise coprime then
∀ (A : Set ℕ), Erdos12.IsGood A → A.Pairwise Nat.Coprime → (fun N => ↑(A ∩ Set.Icc 1 N).ncard) =O[Filter.atTop] fun N => ↑N ^ (2 / 3) / Real.log ↑NSolvedStatement only, no proof