Bound $f(n,m)$ for distinct multiples $k\mid a_k$: is $\max_m f(n,m)\le n^{1+o(1)}$? (Erdős #711)

Let $f(n,m)$ be the least integer such that the interval $(m,\,m+f(n,m))$ contains distinct integers $a_1,\ldots,a_n$ with $k\mid a_k$ for every $1\le k\le n$. Erdős and Pomerance asked to prove both $$\max_m f(n,m)\le n^{1+o(1)}$$ and $$\max_m\big(f(n,m)-f(n,n)\big)\to\infty\quad(n\to\infty).$$ The second was answered affirmatively by van Doorn (2026); the first — that the worst-case window is at most $n^{1+o(1)}$ — remains open.

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean/Coq preferred, else a full written proof) that $\max_m f(n,m)\le n^{1+o(1)}$ — i.e. for every $\epsilon>0$ there is $N$ with $\max_m f(n,m)\le n^{1+\epsilon}$ for all $n\ge N$ — or a disproof (an explicit family $n,\,m(n)$ with $f(n,m)\ge n^{1+c}$ for a fixed $c>0$, with proof). ADVANCES: improve the best proven upper bound, currently $\max_m f(n,m)\ll n^{3/2}$ (Erdős–Pomerance, stated in the background), to $\max_m f(n,m)\ll n^{3/2-\delta}$ for an explicit $\delta>0$, with proof; or a new proven lower bound on $\max_m f(n,m)$ exceeding the current best lower bound $\max_m f(n,m)\gg (\log n/\log\log n)n$ (van Doorn, stated in the background); or a reproducible exact computation of $\max_m f(n,m)$ over a certified range of $n$ with the search code and a fitted growth-exponent estimate. Deliver the proof, the improved bound with proof, or the computation code plus certified values and exponent fit.