Erdős–Pomerance: asymptotics of the window $(n,n+f(n))$ holding distinct multiples of $1,\ldots,n$ (Erdős #710)
Statement
Let $f(n)$ be minimal such that the interval $(n,n+f(n))$ contains distinct integers $a_1,\ldots,a_n$ with $k\mid a_k$ for all $1\leq k\leq n$. Obtain an asymptotic formula for $f(n)$.
Acceptance. FULLY RESOLVES (proof-shaped): a complete rigorous proof — a Lean/Coq formalisation preferred, otherwise a full written proof — of an asymptotic formula for $f(n)$, determining the correct order (including the power of $\log n$) and ideally the leading constant. ADVANCES: (a) improve the upper bound stated in the background (currently $f(n)\leq(1.7398\ldots+o(1))\,n(\log n)^{1/2}$) with proof; (b) improve the lower bound stated in the background (currently $f(n)\geq(2/\sqrt e+o(1))\,n(\log n/\log\log n)^{1/2}$) with proof; or (c) compute $f(n)$ exactly for a new record range of $n$ via a reproducible matching-based program with an optimality certificate, extending OEIS A390246. Deliver the proof, the improved-bound argument, or the search code plus certified values.
Background
A problem of Erdős and Pomerance [ErPo80], listed as open on erdosproblems.com/710 (fetched 2026-07-21, status 'open'). They proved $$\big(\tfrac{2}{\sqrt e}+o(1)\big)\,n\Big(\tfrac{\log n}{\log\log n}\Big)^{1/2}\leq f(n)\leq (1.7398\ldots+o(1))\,n(\log n)^{1/2},$$ leaving the precise growth undetermined — in particular the correct power of $\log n$ and the leading constant. In [Er92c] Erdős offered 2000 rupees (about $78 at 1992 rates) for an asymptotic formula. The values of $f(n)$ are tabulated in OEIS A390246. See also Erdős #711 (erdosproblems.com/711). Attacker's tool: bipartite-matching / system-of-distinct-representatives computation of $f(n)$ for large $n$ to extend A390246, empirically separating the $(\log n)^{1/2}$ and $(\log n/\log\log n)^{1/2}$ scalings and pinning the constant, backed by an analytic argument tightening one of the two bounds.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #710 (T. F. Bloom) | website |
| REF-02 | OEIS A390246 | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.