Optimal bounds for an Erdős problem on matching integers to distinct multiples

Let $f(m)$ be the largest integer such that for every set $A=\{a_1<\cdots <a_m\}$ of $m$ positive integers and every open interval $I$ of length $2a_m$, there exist at least $f(m)$ disjoint pairs $(a,b)$ with $a\in A$ dividing $b\in I$. Solving a problem of Erdős, we determine $f(m)$ exactly, and show $$f(m)=\min (m,\lceil 2\sqrt{m}\rceil )$$ for all $m$. The proof was obtained through an AI-assisted workflow: the proof strategy was first proposed by ChatGPT, and the detailed argument was subsequently made fully rigorous and formally verified in Lean by Aristotle. The exposition and final proofs presented here are entirely human-written. [This paper solves Problem #650 on Bloom’s website “Erdős problems”.]