Let $A = \{a_1 0$, there exists some $k$ such that $F(A,X,k) < X^\epsilon$?

Erdős problem 873

Start work

Let $A = \{a_1 < a_2 < \dots\} \subseteq \mathbb{N}$ and let $F(A,X,k)$ count the number of $i$ such that $[a_i,a_{i+1}, \dots ,a_{i+k−1}] < X$ , where the left-hand side is the least common multiple. Is it true that, for every $\epsilon > 0$ , there exists some $k$ such that $F(A,X,k) < X^\epsilon$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

873.lean

Retained formal statement1 of 1

Let $A = \{a_1 < a_2 < \dots\} \subseteq \mathbb{N}$ and let $F(A,X,k)$ count the number of $i$ such that $[a_i,a_{i+1}, \dots ,a_{i+k−1}] < X$ , where the left-hand side is the least common multiple. Is it true that, for every $\epsilon > 0$ , there exists some $k$ such that $F(A,X,k) < X^\epsilon$ ?

FormalConjectures/ErdosProblems/873.leanErdos873.erdos_8731 lineExact file

1True ↔ ∀ (a : ℕ → ℕ), ∀ ε > 0, 0 < a 0 → StrictMono a → ∃ k, ∀ X > 0, ↑↑(Erdos873.F a X k) < ↑(X ^ ε)

OpenStatement only, no proof