AI 中文总结
该研究改进了 Choi、Erdős 和 Szemerédi 关于集合包含四个不同正整数两两之和的基数下界，证明常数 C 可从 3166 优化至最优值 4，并借助 AI 与形式推理智能体完成证明。
AI 中文摘要
Choi、Erdős 和 Szemerédi 证明了存在一个绝对常数 $C$，使得对于所有满足至少 $n+C$ 个元素的子集 $A \subseteq \{1, 2, \ldots, 2n\}$，都存在四个不同的正整数，其两两之和全部包含在 $A$ 中。第一作者最近概述了一个证明，表明可以取 $C = 3166$，而在此我们证明对于所有 $n \ge 6$，实际上有 $C = 4$，这是最优的。我们给出的证明最初由人工智能构思，最终结果由 Harmonic 开发的形式推理智能体 Aristotle 证明并形式化。
英文摘要
Choi, Erdős and Szemerédi showed that there exists an absolute constant $C$ such that for all subsets $A \subseteq \{1, 2, \ldots, 2n\}$ with at least $n+C$ elements, there exist four distinct positive integers whose pairwise sums are all contained in $A$. A proof that one can take $C = 3166$ was recently sketched by the first author, and here we show that we actually have $C = 4$ for all $n \ge 6$, which is optimal. The proof we present was originally conceived of by AI, with the final result proved and formalized by Aristotle, the formal reasoning agent developed by Harmonic.
Comments10 pages
