Factor $n!$ into distinct parts $>n$: does $f(n)-2n\sim c\,n/\log n$? (Erdős #390)

Let $f(n)$ be the least integer $m$ for which the factorial $n!$ can be written as a product of distinct integers all exceeding $n$, with $m$ as the largest factor: $$n!=a_1 a_2\cdots a_k,\qquad n<a_1<a_2<\cdots<a_k=m.$$ Is there a constant $c$ such that $$f(n)-2n\sim c\,\frac{n}{\log n}\qquad(n\to\infty)?$$ If so, determine the value of $c$.

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean/Coq preferred, otherwise a full written proof) that establishes whether the limit $c=\lim_{n\to\infty}(f(n)-2n)\big/(n/\log n)$ exists — giving its exact value if it does, or proving it does not exist (e.g. distinct liminf and limsup, refuting the $\sim$ asymptotic). ADVANCES: sharpen the Erdős–Guy–Selfridge result $f(n)-2n\asymp n/\log n$ to explicit constants, i.e. prove $c_1\,n/\log n\leq f(n)-2n\leq c_2\,n/\log n$ for large $n$ with a strictly smaller ratio $c_2/c_1$ than currently known, with proof; OR compute $f(n)$ exactly over a substantially larger range than the published data, with a reproducible search and a certificate that each computed value is optimal, and report the empirical trend of $(f(n)-2n)(\log n)/n$. Deliver the proof file, the improved-constant proof, or the search code plus the extended table of optimal values and certificate.