Erdős 问题 #786 的否定答案
A negative answer to Erdős Problem #786
浏览论文内容
中文总结 AI 辅助
本文证明对任意可容许正整数集合，其密度不能任意接近1，且存在绝对常数η使最大可容许子集大小小于(1-η)N，从而否定回答Erdős问题#786的两个子问题，并在Lean 4中形式化验证。
中文摘要 AI 辅助
称正整数集合 $A$ 为可容许的，如果每当 $a_1\cdots a_r=b_1\cdots b_s$ 且 $a_1,\dots,a_r$ 是 $A$ 中互不相同的元素，$b_1,\dots,b_s$ 也是 $A$ 中互不相同的元素时，必然有 $r=s$。Erdős 曾问：对于每个 $\varepsilon>0$，可容许集合是否都能具有密度 $1-\varepsilon$？以及 $\{1,\dots,N\}$ 是否总是包含一个大小为 $(1-o(1))N$ 的可容许子集？对于允许重复的变体，Erdős、Ruzsa 和 Sárközy 以及 Granville 和 Soundararajan 已经对这两个问题给出了否定回答；对于互不相同元素的乘积，第一个问题直到最近才被回答（密度上界为 $7/8$），而第二个问题仍然悬而未决。我们证明：每个可容许的 $A\subseteq\{1,\dots,N\}$ 都满足 $\sum_{a\in A}1/a\le\tfrac12\log N+(\log\log N+2)^2$，并且存在一个绝对常数 $\eta>0$，使得对所有足够大的 $N$，每个可容许的 $A\subseteq\{1,\dots,N\}$ 都有 $|A|<(1-\eta)N$。因此，这两个问题都有否定答案。证明是初等的；第二个证明依赖于一种耦合，该耦合替换由小素数组成的整数中的最大除数，从而避免了在乘法表中计数商时固有的除数函数损失。这两个否定答案都在 Lean 4 中针对 Formal Conjectures 项目的陈述得到了形式化验证。
英文摘要
Call a set $A$ of positive integers admissible if, whenever $a_1\cdots a_r=b_1\cdots b_s$ with $a_1,\dots,a_r$ distinct elements of $A$ and $b_1,\dots,b_s$ distinct elements of $A$, necessarily $r=s$. Erdős asked whether admissible sets can have density $1-\varepsilon$ for every $\varepsilon>0$, and whether $\{1,\dots,N\}$ always contains an admissible subset of size $(1-o(1))N$. For the variant in which repetitions are allowed both questions were answered negatively by Erdős, Ruzsa and Sárközy and by Granville and Soundararajan; for products of distinct elements, the first question was answered only recently (with density bound $7/8$), and the second has remained open. We show that every admissible $A\subseteq\{1,\dots,N\}$ satisfies $\sum_{a\in A}1/a\le\tfrac12\log N+(\log\log N+2)^2$, and that there is an absolute constant $η>0$ such that every admissible $A\subseteq\{1,\dots,N\}$ has $|A|<(1-η)N$ for all large $N$. Both questions therefore have negative answers. The proofs are elementary; the second rests on a coupling that replaces the largest divisor of an integer composed of small primes, which avoids the divisor-function losses inherent in counting quotients along a multiplication table. Both negative answers are formally verified in Lean 4 against the statements of the Formal Conjectures project.
