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 statement2 of 3

Let $s_1 < s_2 < \dots$ be the sequence of squarefree numbers. Is it true that $s_{n + 1} - s_n \le (1 + o(1)) \cdot (\pi^2 / 6) \cdot \log (s_n) / \log (\log (s_n))$ ?

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

1True ↔2  ∃ c,3    c =o[Filter.atTop] 1 ∧4      ∀ᶠ (n : ℕ) in Filter.atTop,5        ↑(Erdos208.erdos208.s (n + 1)) - ↑(Erdos208.erdos208.s n) ≤6          (1 + c n) * (Real.pi ^ 2 / 6) * Real.log ↑(Erdos208.erdos208.s n) /7            Real.log (Real.log ↑(Erdos208.erdos208.s n))

OpenStatement only, no proof

Sources

Search problems.science