Let $x_1,x_2,\dots \in [0,1]$ be an infinite sequence. Is it true that$$\underset{n}{\inf }\underset{m\to \infty }{\mathrm{liminf}}n|x_{m+n}-x_m|\le 5^{-1/2}\approx 0.447?$$

AMS 11 · solved (literature)

theorem erdos_480 : answer(True) ↔ ∀ (x : ℕ → ℝ), (∀ n, x n ∈ Set.Icc 0 1) →
    ⨅ (n : ℕ+), atTop.liminf (fun m => (n : ℕ) * |x (m + (n : ℕ)) - x m|) ≤ 1 / √5