Erdős problem 681

Erdős problem 681. Is it true that for all large $n$ there exists $k$ such that $n + k$ is composite and $p(n+k) > k^2$ , where $p(m)$ is the least prime factor of $m$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

681.lean

Retained formal statement1 of 1

Erdős problem 681. Is it true that for all large $n$ there exists $k$ such that $n + k$ is composite and $p(n+k) > k^2$ , where $p(m)$ is the least prime factor of $m$ ?

FormalConjectures/ErdosProblems/681.leanErdos681.erdos_6811 lineExact file

1True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ k > 0, (n + k).Composite ∧ ∀ (p : ℕ), Erdos681.IsLPF p (n + k) → p > k ^ 2

OpenStatement only, no proof