昨晚，数学界炸了！AI 数学家「亚里士多德」竟在 6 个小时内，一键破解了 30 年难题的简版，引陶哲轩盛赞。数学领域 Vibe proving 时代来了。

30 年未解数学难题，终于告破！

由 HarmonicMath 开发的 AI 数学家「亚里士多德」（Aristotle），100% 独立完成了埃尔德什问题 #124。

它在 Lean 证明系统中，耗时仅 6 个小时，验证只需 1 分钟。

全程没有一丝人类的参与辅助，这一刻，堪称数学界的「登月」时刻。

HarmonicMath 创始人 Vlad Tenev 感慨道，「数学圈正迎来巨变，vibe 证明的时代，来了」！

就连菲尔兹奖得主陶哲轩，高度赞扬了 AI 数学家「亚里士多德」。

AI 发现数学的时代，正式开始了。

30 年难题告破，AI 做到了

一直以来，数学家 Erd ő s Pál 的「问题列表」，就像一座知识的珠穆朗玛峰，考验着人类的极限。

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

其象征意义远大于实际价值，成为了无数数学家的精神勋章。

30 年来，第 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

顺便提一句，E124 问题一共有两个不同版本，全部由埃尔德什提出。

目前，AI 亚里士多德解决的是一个比较简单的版本。

在时间方面，Aristotle 花了 6 小时，而 Lean 只花了 1 分钟。

Erd ő s 问题的网站维护者表示，Aristotle 的表现最令人深刻！

ChatGPT、Gemini 都失败了

陶哲轩对此点评道，就我所知，Gemini 和 ChatGPT 的深度研究工具，都没有找到关于这个问题的任何新的、有价值的文献。

Gemini 给出了一个简单的观察：如果把数字 1 排除掉，那么 gcd 条件就会变成必要的；它还解释了条件

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

不过，它没有找到与这个问题直接相关的新文献。

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

因此，并没有获得新的信息，不过读者可能会觉得这些 AI 生成的总结还是挺有意思的。

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

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

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

有大量问题其实相对容易证明或证伪，但因为真正能投入研究的专家数学家数量有限，这些问题几乎没得到过多少关注。

换句话说，这条「尾巴」里其实藏着不少触手可及的「低垂果实」：

如果有办法把这些问题进行大规模的自动化攻克，就可能产出相当多新的数学结果。

去年，陶哲轩在 Equational Theories Project 里亲历过一个类似的情况。

在这个项目中，他们面对的是普遍代数里 2200 万条可能的蕴涵关系（implication），如果全靠人类去做，必定花费非常多的时间。

于是，他们决定从一开始用比较「低技术含量」的自动化方法，短短几天就解决了大部分。

接下来，又不断上复杂手段，啃那些前几轮怎么都啃不动的顽固难点。

最后，剩下几条特别顽固的，又花费了人类数学家几个月的时间搞定。

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

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

最近几周，这个网站的「未解」标签突然少了近十个，全部在 AI 加持下文献搜索发现——

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

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

有的在 Lean 里验证已有证明，有的生成和这些问题相关的整数序列项，还有的补上某个既有思路里缺失的证明步骤。

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

E124 就是一个典型，这个问题完整版本有些难度，曾在 Erd ő s 的三篇论文中出现。

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

这事一直没有人发现，直到 Boris Alexeev 把问题丢给自动化工具 Aristotle，没想到 AI 在几小时内自主找到了漏洞，并用 Lean 完成了形式化证明。

可以看到，AI 正在点亮数学的「暗森林」。

正如陶哲轩所言，「自动化工具先清理掉最容易的问题，把真正难啃的那部分剥离出来，让人类数学家把精力花费在值得的地方」。