Is it true that for every $ϵ,\eta >0$ there exists a $k$ such that the density of $n$ for which$$P(n(n+1)\cdots (n+k))>n^{1-ϵ}$$is at least $1-\eta$ (where $P(m)$ is the greatest prime divisor of $m$)?

AMS 11 · open (literature)

theorem erdos_1201 :
    answer(sorry) ↔
      ∀ ε > 0, ∀ η > 0, ∃ k : ℕ,
        atTop.liminf (fun x : ℕ ↦
          (((count (Erdos1201Set ε k) x : ℝ) / (x : ℝ)) : EReal)) ≥ (1 - η : EReal)