Is there $f(n)\to\infty$ with a composite $m$ satisfying $n+f(n)<m<n+p(m)$? (Erdős #463)

Let $p(m)$ denote the least prime factor of $m$. Is there a function $f$ with $f(n)\to\infty$ as $n\to\infty$ such that, for all large $n$, there exists a composite number $m$ with $$n+f(n)<m<n+p(m)?$$ Equivalently, writing $F(n)=\min_{m>n}\,(m-p(m))$, Erdős [Er92e] asks about the size of $F(n)$ and in particular whether $$n-F(n)\sim c\,n^{1/2}$$ for some constant $c>0$; the two formulations concern how far above $n$ one must look to find a composite integer whose least prime factor overshoots the gap back down to $n$.

Acceptance. FULLY RESOLVES: a complete proof — a Lean/Coq formalisation matching the DeepMind formal-conjectures statement for #463 is preferred, otherwise a full written proof — that either exhibits such a function $f$ (with a proof that $f(n)\to\infty$ and the composite-$m$ condition holds for all large $n$) or proves that no such $f$ exists; a rigorous resolution of the companion asymptotic $n-F(n)\sim c\,n^{1/2}$ (proving it with the constant, or refuting it) likewise settles the [Er92e] question. ADVANCES: prove the existence for a specific explicit slowly growing $f$ (e.g. $f(n)=\log\log n$), unconditionally or under a stated hypothesis; or determine the correct order of $n-F(n)$ by proving matching upper and lower bounds $n-F(n)\asymp n^{1/2}$; or, computationally, tabulate $F(n)$ over a large stated range, report the best-fit constant $c$ for $n-F(n)\sim c\,n^{1/2}$ with residuals and the range covered. Deliver the proof artifact or the computation code with its fitted data.