Erdős Problem 1139

Reference: erdosproblems.com/1139

theorem Erdos1139.erdos_1139 : sorry ↔ Filter.limsup (fun (k : ℕ) => (↑↑(Nat.nth (fun (n : ℕ) => 0 < n ∧ ArithmeticFunction.cardFactors n ≤ 2) (k + 1)) - ↑↑(Nat.nth (fun (n : ℕ) => 0 < n ∧ ArithmeticFunction.cardFactors n ≤ 2) k)) / ↑(Real.log (↑k + 1))) Filter.atTop = ⊤

Let $1\leq u_1 < u_2 < \cdots$ be the sequence of integers with at most $2$ prime factors. Is it true that $$\limsup_{k \to \infty} \frac{u_{k+1}-u_k}{\log k}=\infty?$$