Let $d_n=p_{n+1}-p_n$, where $p_n$ denotes the $n$th prime. Is it true that$$\frac{{\max }_{n<x}{d}_n{d}_{n-1}}{({\max }_{n<x}{d}_n{)}^2}\to 0$$as $x\to \infty$?

AMS 11 · open (literature)

theorem erdos_1137 :
    answer(sorry) ↔
     Tendsto (fun x ↦
        (((range x).sup (fun n ↦ (primeGap n) * (primeGap (n - 1))) : ℕ) : ℝ) /
        (((range x).sup primeGap : ℕ) : ℝ) ^ 2) atTop (𝓝 0)