Erdős 整数匹配至不同倍数问题的最优界

设 $f(m)$ 为满足以下条件的最大整数：对任意 $m$ 个正整数的集合 $A = \{a_1 < \cdots < a_m\}$ 和任意长度为 $2a_m$ 的开区间 $I$，存在至少 $f(m)$ 对不相交的数对 $(a, b)$，其中 $a \in A$ 整除 $b \in I$。通过解决 Erdős 的一个问题，我们精确地确定了 $f(m)$，并证明了 $$f(m)=\min\bigl(m,\lceil 2\sqrt{m}\,\rceil\bigr)$$ 对所有 $m$ 成立。该证明通过 AI 辅助工作流获得：证明策略首先由 ChatGPT 提出，随后详细的论证由 Aristotle 在 Lean 中完全严格化并形式化验证。此处给出的阐述和最终证明完全由人工撰写。[该论文解决了 Bloom 网站上编号为 #650 的 Erdős 问题。]