新智元报道

(资料图片)

编辑：桃子

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

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

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

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

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

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

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

30年难题告破，AI做到了

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

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

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

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正在点亮数学的「暗森林」。

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

参考资料：

秒追ASI

标签： 陶哲轩 ChatGPT Erd 问题 难题 Fin a_i