Erdős Problem 463

Reference: erdosproblems.com/463

theorem Erdos463.erdos_463 : (∃ (f : ℕ → ℕ) (_ : Filter.Tendsto f Filter.atTop Filter.atTop), ∀ᶠ (n : ℕ) in Filter.atTop, ∃ (m : ℕ), ¬Nat.Prime m ∧ n + f n < m ∧ m < n + m.minFac) ↔ sorry

Is there a function $f$ with $f(n)\to\infty$ as $n\to\infty$ such that, for all large $n$, there is a composite number $m$ such that $$ n + f(n) < m < n + p(m) $$ Here $p(m)$ is the least prime factor of $m$.