AI数学家亚里士多德6小时破解30年埃尔德什数学难题

昨夜，数学领域发生轰动性事件！人工智能数学家「亚里士多德」在仅仅六个小时内，成功解决了困扰学界三十年的数学难题简化版本，获得陶哲轩的高度赞扬。这标志着数学证明进入Vibe proving新时代。

经过三十年悬而未决，这一数学难题终于被攻克！

由HarmonicMath团队开发的AI数学家「亚里士多德」，完全独立地完成了埃尔德什问题#124的证明。

它在Lean证明系统中，仅耗费六小时进行推导，而验证过程只需一分钟。

全程无需任何人类干预，这一时刻堪称数学界的「里程碑」突破。

HarmonicMath创始人Vlad Tenev感慨道，「数学领域正经历巨大变革，vibe证明的时代，已经到来」！

就连菲尔兹奖得主陶哲轩，也对AI数学家「亚里士多德」给予了高度评价。

AI引领数学发现的时代，正式拉开序幕。

30年难题终告破解，AI实现重大突破

长期以来，数学家Erdős Pál的「问题列表」犹如知识界的珠穆朗玛峰，挑战着人类智慧的极限。

那些悬而未解的难题，悬赏金额从几十美元到上万美元不等。

其象征意义远超实际价值，成为无数数学家的精神追求。

三十年来，第124号问题（Erdős #124）在论文「Complete sequences of sets of integer powers」中提出后，一直无人能够解决。

E124核心内容是：给定k个自然数d_i ≥ 2，如果∑ 1/(d_i - 1) ≥ 1，那么对于任意自然数n，总存在a_i，使得n = ∑ a_i。

且每个a_i，在d_i下的「数字」表示仅限于{0,1}。

简单来说，它本质上是探究——在极端约束条件下，是否总能使用「二进制」方式表示任意大数，而不受基数影响？

这涉及「组合数学」的深层次领域，传统方法在gcd条件和边界案例上遇到阻碍。

直到昨夜，这一障碍被彻底打破。

Harmonic团队专门设计了「数学超级智能」原型——亚里士多德（Aristotle），融合了强化学习、蒙特卡洛树搜索以及Lean形式化语言。

输入问题后，它通过搜索上亿种证明策略，最终生成100%可验证的定理。

数学家Boris Alexeev表示，这是AI输出的三个定理中，自己最青睐的一个：

theorem erdos_124 : ∀ k, ∀ d : Fin k → ℕ, (∀ i, 2 ≤ d i) → 1 ≤ ∑ i : Fin k, (1 : ℚ) / (d i - 1) → ∀ n, ∃ a : Fin k → ℕ, ∀ i, ((d i).digits (a i)).toFinset ⊆ {0, 1} ∧ n = ∑ i, a i

地址：https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos124.md

值得一提的是，E124问题共有两个不同版本，均由埃尔德什提出。

目前，AI亚里士多德解决的是相对简单的版本。

在时间方面，Aristotle耗时六小时，而Lean验证仅用一分钟。

Erdős问题网站维护者指出，Aristotle的表现令人印象深刻！

ChatGPT、Gemini均未成功

陶哲轩对此评论道，据我所知，Gemini和ChatGPT的深度研究工具，均未找到关于该问题的任何新颖且有价值的文献。

Gemini提供了一个简单观察：若将数字1排除，gcd条件便成为必要；它还解释了条件

的重要性，并将其与一些关于Cantor集的平行研究联系起来，尤其是「Newhouse gap lemma」。

然而，它未能找到与该问题直接相关的新文献。

ChatGPT则大量依赖本网页作为主要权威来源，例如引用Aristotle的证明、本页引用的其他论文及相关问题页面。

因此，并未获得新信息，不过读者或许会觉得这些AI生成的总结颇具趣味。

陶哲轩：AI正在收割数学低垂果实

在mathstodon上，陶哲轩还分享了多年来的经验——

他表示，当前实际情况是：数学未解问题服从「长尾分布」，AI自动化「收割」恰恰集中在长尾最末端。

有大量问题其实相对容易证明或证伪，但由于真正投入研究的专家数学家有限，这些问题几乎未被关注。

换言之，这条「尾巴」中隐藏着许多触手可及的「低垂果实」：

若能大规模自动化攻克这些问题，便可能产出大量新数学结果。

去年，陶哲轩在Equational Theories Project中亲历类似情况。

该项目涉及普遍代数里2200万条可能的蕴涵关系，若全靠人类处理，将耗费极长时间。

于是，他们从一开始采用「低技术含量」的自动化方法，短短几天便解决大部分问题。

随后，又逐步使用复杂手段，处理前几轮未能解决的顽固难点。

最后，剩下几条特别棘手的，人类数学家花费数月时间才完成。

目前，Erdős问题网站收录了1108个曾在Erdős至少一篇论文中出现过的问题。

其中，既有像E3这类著名难题，也有众多更不起眼、几乎无人关注的问题，甚至连Erdős本人都未再回头研究。

最近几周，该网站「未解」标签突然减少近十个，全因在AI辅助下进行文献搜索发现——

实际上，这些问题早已被他人解决。

正在研究这些问题的人类数学家也结合使用AI工具和形式化证明助手：

有的在Lean中验证已有证明，有的生成与问题相关的整数序列项，还有的补全既有思路中缺失的证明步骤。

最近，又发现另一类落入自动化工具能力范围的「低垂果实」——那些因描述存在技术性瑕疵而意外变得易解的问题。

E124便是典型，该问题完整版本较难，曾在Erdős的三篇论文中出现。

但其中两篇遗漏了一个关键假设，使得这一版本其实仅是Brown判据的直接推论。

此事一直未被察觉，直到Boris Alexeev将问题交给自动化工具Aristotle，没想到AI在几小时内自主发现漏洞，并用Lean完成形式化证明。

可见，AI正在照亮数学的「暗森林」。

正如陶哲轩所言，「自动化工具先清理最容易的问题，将真正难啃的部分剥离出来，让人类数学家集中精力于值得之处。」

参考资料：

https://www.erdosproblems.com/forum/thread/124#post-1892

https://x.com/SebastienBubeck/status/1994946303546331508?s=20

https://mathstodon.xyz/@tao/115639983683442577

https://x.com/thomasfbloom/status/1995094668879462466?s=20