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

AMS 11 · open (literature)

theorem erdos_1139 :
    answer(sorry) ↔
      letI u := Nat.nth (fun n ↦ 0 < n ∧ Ω n ≤ 2)
      atTop.limsup (fun k : ℕ ↦ (((u (k + 1) : ℝ) - (u k : ℝ)) / Real.log (↑k + 1) : EReal)) = ⊤