Erdős Problem 208

Reference: erdosproblems.com/208

noncomputable def Erdos208.erdos208.s : ℕ → ℕ

The sequence of squarefree numbers, denoted by s as in Erdős problem 208.

Equations

• Erdos208.erdos208.s = Nat.nth Squarefree

theorem Erdos208.erdos_208.i : (∀ ε > 0, (fun (n : ℕ) => ↑(erdos208.s (n + 1)) - ↑(erdos208.s n)) ≪ fun (n : ℕ) => ↑(erdos208.s n) ^ ε) ↔ sorry

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$?

theorem Erdos208.erdos_208.ii : (∃ (c : ℕ → ℝ), c =o[Filter.atTop] 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(erdos208.s (n + 1)) - ↑(erdos208.s n) ≤ (1 + c n) * (Real.pi ^ 2 / 6) * Real.log ↑(erdos208.s n) / Real.log (Real.log ↑(erdos208.s n))) ↔ sorry

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))$?

theorem Erdos208.erdos_208.variants.log_bound : (fun (n : ℕ) => ↑(erdos208.s (n + 1)) - ↑(erdos208.s n)) ≪ fun (n : ℕ) => Real.log ↑(erdos208.s n)

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

[Er79] Erdős, Paul, Some unconventional problems in number theory. Math. Mag. (1979), 67-70.