事件概述 - AI辅助人类数学家团队在48小时内攻克了已悬置50年的数学难题Erdos1026问题，并给出了正式证明 [1][4] - 该问题由传奇数学家保罗·埃尔德什于1975年提出，在2025年12月被快速解决 [5] 问题定义与转化 - 埃尔德什原问题较为模糊：给定一串不同的实数，定义S为所有单调子序列（递增或递减）的最大可能和，探讨该函数的性质 [7] - 问题被清晰化为一个游戏：Alice将N枚硬币分成n堆，Bob可选取一个单调的子序列拿走硬币，研究Bob至少能拿到总硬币数的比例c(n) [7] - 当n为平方数时，例如Alice将硬币分成k²堆并特定排列，Bob最多拿到1/k的比例，即c(k²) ≤ 1/k [10] - 已有研究给出下限：c(n) ≥ (1/√2) / √n，因此√n·c(n)的极限值在1/√2和1之间 [10] 关键进展与猜想 - 通过手算小n值得到：c(1)=1, c(2)=1, c(3)=2/3, c(4)=1/2, c(5)=1/2, c(6)=3/7 [11] - 基于数据，Stijn Cambie提出猜想：c(k²) = 1/k，这意味着当n很大时，Bob能保证拿到约1/√n的比例 [11] AI的介入与证明 - 2025年12月7日，Boris Alexeev使用AI工具Aristotle在证明辅助语言Lean中自动证明了c(k²)=1/k [12] - 几乎同时，Koishi Chan给出了一个优美的人类证明——“膨胀法” [12] - 随后发现，该结果其实已存在于2016年的一篇论文中，并引用了更早的“膨胀法”工作，只是未被链接到埃尔德什的原问题 [12] - 陶哲轩使用另一个AI工具AlphaEvolve探索c(n)，通过让AI尝试构造使S尽量小的序列，得到了n=1到16的数值结果 [13][15] - 从AI生成的看似杂乱的分数序列中，Boris Alexeev提炼出精确公式：c(k²+2a+1) = k / (k²+a)，其中 -k < a < k [17] - 该公式对应的1/c(n)图像，正是对√n的分段线性逼近 [19] 与经典问题的关联及最终证明 - Lawrence Wu指出，该问题等价于一个正方形填充问题（埃尔德什问题106） [21] - 他证明c(n) ≥ 1/f(n)，并展示了如何从AlphaEvolve给出的序列构造出正方形填充 [22] - 通过AI深度搜索，找到了2024年Baek、Koizumi、Ueoro的论文，其中证明f(k²+2c+1) ≤ k + c/k [24] - 结合Praton的嵌入论证，恰好给出c(k²+2a+1) ≤ k/(k²+a)，与之前得到的下界吻合，猜想完全得证 [24] 协作模式与影响 - 陶哲轩强调，此次成功依赖于汇聚了不同背景的人、文献和工具的协作网络，所有关键环节在48小时内完成 [24] - 传统模式下，一两位数学家凭借简单工具可能需要数周甚至数月才能完成 [4][24] - 此次协作遵循了“平衡的AI政策”，鼓励公开说明AI的使用情况并反对隐瞒，同时要求用户自行仔细核查AI生成的内容 [25][27] - 这标志着一个数学研究新范式的开始，即人机协作能极大加速研究进程 [1][25]