AI数学家“亚里士多德”6小时攻克30年难题，陶哲轩盛赞：数学界迎来“vibe proving”时代

昨夜，数学界轰动！AI数学家「亚里士多德」仅用6小时，便一键破解了困扰数学界30年的难题的简化版本，赢得了菲尔兹奖得主陶哲轩的高度赞赏。数学领域正式迎来vibe proving时代。

30年未解数学难题，终于被攻克！

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

该AI在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

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

顺便一提，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正在点亮数学的“暗森林”。

正如陶哲轩所言：“自动化工具先清理掉最容易的问题，把真正难啃的部分剥离出来，让人类数学家将精力投入更有价值的地方。”

参考资料：

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