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

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

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

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

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

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形式化语言。

ChatGPT、Gemini都失败了

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

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

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

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

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

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

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

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

目前，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

本文来自微信公众号“新智元”，作者：新智元，编辑：桃子，36氪经授权发布。