# 热门搜索 #
大模型
人工智能
openai
融资
chatGPT
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
地址：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
文章来自于微信公众号 “新智元”，作者 “新智元”
