Erdős problem 680

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

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

680.lean

Retained formal statement1 of 2

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

FormalConjectures/ErdosProblems/680.leanErdos680.erdos_680.parts.i1 lineExact file

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

OpenStatement only, no proof