Erdős problem 208

In [Er79] Erdős says perhaps $s_{n+1} - s_n \ll \log s_n$ , but he is 'very doubtful'.

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

208.lean

Retained formal statement1 of 3

Let $s_1 < s_2 < \dots$ be the sequence of squarefree numbers. Is it true that for any $\epsilon > 0$ and large $n$ , $s_{n+1} - s_n \ll_\epsilon s_n^\epsilon$ ?

FormalConjectures/ErdosProblems/208.leanErdos208.erdos_208.parts.i4 linesExact file

1True ↔2  ∀ ε > 0,3    (fun n => ↑(Erdos208.erdos208.s (n + 1)) - ↑(Erdos208.erdos208.s n)) =O[Filter.atTop] fun n =>4      ↑(Erdos208.erdos208.s n) ^ ε

OpenStatement only, no proof