AI攻克30年数学难题：Erdős问题#124简易版获证明，数学界震动

一个困扰数学界长达30年的难题，如今被人工智能成功攻克！

消息一出，立刻在社交媒体平台X（原推特）上引发了热烈讨论。

来自美国的Harmonic公司开发的数学AI模型，独立证明了著名的Erdős问题#124，而这个问题此前已被数学家们搁置了近三十年，无人能解。

微软前AI副总裁、目前在OpenAI研究AGI的Sebastien Bubeck激动地分享了这一消息，并表示：

该解决方案完全由AI自主生成，整个证明过程仅耗时6小时。

甚至连著名数学家陶哲轩也加入讨论，他在对比了Gemini和ChatGPT的深度研究工具后指出，Harmonic模型对该问题的证明表现更为出色。

那么，这究竟是一个怎样的数学难题？Harmonic模型又是如何“大显身手”的呢？

让我们一探究竟——

AI成功证明Erdős问题#124的简化版本

首先需要澄清，经过多方讨论，我们才明白——

原来Harmonic模型所证明的并非原版Erdős问题#124，而是该问题的一个简易版本。

原版Erdős问题#124需要证明的命题如下：

通俗解释即为：

假设你有k个不同的“进制生成器”，分别对应数字d1, d2, …, dk。

游戏规则是：1）你可以从每个生成器所产生的数字列表中，至多挑选一个数；2）然后将挑选出的所有数字相加；3）最后判断能否正好得到目标整数。

问题的核心在于——

只要这套“进制生成器”满足一个特定条件，即1/(d1-1) +1/(d2-1)+…+1/(dk-1)≥ 1，那么是否所有足够大的整数都能通过这种规则凑出来？

截至目前，该问题的研究进展可总结如下：

也就是说，这个问题在几十年间逐渐分化出难易两个版本。

在原版[BEGL96]中，挑战者不允许使用数字1，且需额外满足gcd条件（各进制之间没有“重复周期”），最终仅发现对于特定集合 {3, 4, 7} 猜想成立。

而当条件放宽后（允许使用数字1且无需满足gcd条件），Harmonic模型成功证明只要满足上述特定条件，就一定能凑出所有大整数，且相关证明已通过Lean形式化验证。

Harmonic模型的证明方案如下，众多专家纷纷表示，这个方案出人意料地简洁。

不过，此次用Harmonic模型证明#124简易版的Boris Alexeev也补充道：

在“形式化猜想”项目中，原本包含该猜想的正式数学表述。但其中有一个笔误：注释里写的是≥1，而对应的Lean程序代码里写的却是=1。这一错误导致原表述的条件变弱，仅覆盖了等于1的情况，而遗漏了大于1的情形。

因此，我修正了这个错误，并删除了原表述中我认为不必要的部分。最终，AI成功证明了这个更简洁、更准确的版本。

总结来说，Harmonic证明了问题#124的简易版本，而原版难题仍悬而未决。

“Vibe证明时代已经到来”

尽管如此，学界大佬们对AI模型证明数学难题的潜力给予了高度肯定。

参考编程领域的Vibe Coding概念（最早由AI大神卡帕西提出），Harmonic联合创始人兼CEO激动地表示：

我们正处在数学领域深刻变革的边缘，Vibe证明时代已经来临。

顺着他的发言，我们也深入探究了Harmonic模型背后的团队，毕竟在陶哲轩眼中，它此次表现超越了ChatGPT和Gemini。

根据公开资料，其背后公司名为Harmonic，目标十分明确：

打造世界上最先进的数学推理引擎。

两位联合创始人分别为Tudor Achim和Vlad Tenev。

CEO Tudor Achim，拥有卡内基梅隆大学计算机科学学士学位，同时在斯坦福大学攻读计算机科学PhD（目前休学中）。

2023年，他与Vlad Tenev共同创立Harmonic，旨在打造全球最先进的推理引擎。

此前，他还曾担任自动驾驶辅助系统开发公司Helm.ai的联合创始人兼CTO。

执行主席Vlad Tenev，拥有斯坦福大学数学学士学位和加州大学洛杉矶分校数学硕士学位。

除了在Harmonic担任联合创始人兼执行主席，他目前还兼任金融公司Robinhood Markets的CEO。

根据官网公开信息，Harmonic在大约一周前完成了1.2亿美元（约合人民币8.5亿）的C轮融资。

本轮融资由Ribbit Capital领投，公司估值达到14.5亿美元（约合人民币103亿）。

Harmonic的旗舰模型正是本次使用的Aristotle模型（也称“亚里士多德”），据悉它是第一个在2025年国际数学奥林匹克竞赛中为其中五道题提供形式化验证解决方案的模型。

Aristotle在确保准确性和消除幻觉的同时，达到了金牌级别的表现。

据Vlad Tenev透露，此次使用的Aristotle经过更新，具备更强大的推理能力和自然语言界面。

可以预见，随着AI解决复杂数学问题能力的不断突破，越来越多曾被束之高阁的百年难题将重见天日，并有望被逐一攻克。

无论如何，AI浪潮已然开启，开弓没有回头箭。

参考链接：

[1]https://x.com/i/trending/1994986636623724980

[2]https://www.erdosproblems.com/forum/thread/124#post-1892

[3]https://x.com/thomasfbloom/status/1995094668879462466