Erdős Problem 1137

Reference: erdosproblems.com/1137

theorem Erdos1137.erdos_1137 : sorry ↔ Filter.Tendsto (fun (x : ℕ) => ↑((Finset.range x).sup fun (n : ℕ) => primeGap n * primeGap (n - 1)) / ↑((Finset.range x).sup primeGap) ^ 2) Filter.atTop (nhds 0)

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