Erdős Problem 680

Reference: erdosproblems.com/680

theorem Erdos680.erdos_680 : (∀ᶠ (n : ℕ) in Filter.atTop, ∃ (k : ℕ), k ≠ 0 ∧ (n + k).minFac > k ^ 2 + 1) ↔ sorry

Is it true that, for all sufficiently large $n$, there exists some $k$ such that [ p(n+k)>k^2+1, ] where $p(m)$ denotes the least prime factor of $m$?

theorem Erdos680.erdos_680.variant : (∀ ε > 0, ∃ C > 0, ¬∀ᶠ (n : ℕ) in Filter.atTop, ∃ (k : ℕ), k ≠ 0 ∧ ↑(n + k).minFac > Real.exp ((1 + ε) * √↑k) + C) ↔ sorry

Can one prove this is false if we replace $k^2+1$ by $e^{(1+\epsilon)\sqrt{k}}+C_\epsilon$, for all $\epsilon>0$, where $C_\epsilon>0$ is some constant?