Erdős problem 873
Let and let count the number of such that , where the left-hand side is the least common multiple. Is it true that, for every , there exists some such that ?
Sources
FormalConjectures/ErdosProblems/
873.lean
Retained formal statement
Let and let count the number of such that , where the left-hand side is the least common multiple. Is it true that, for every , there exists some such that ?
True ↔ ∀ (a : ℕ → ℕ), ∀ ε > 0, 0 < a 0 → StrictMono a → ∃ k, ∀ X > 0, ↑↑(Erdos873.F a X k) < ↑(X ^ ε)OpenStatement only, no proof