Erdős problem 208 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

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

Sources

Search problems.science