AI破解数学难题：30年悬案终见曙光

AI技术再度刷新人类认知边界，30年悬而未决的数学难题就这样被AI破解了？！

在当前的𝕏（前推特）平台上，一股热烈的讨论风潮正在席卷——

来自Harmonic的数学AI模型独立证明了Erdős问题#124，这一难题此前已被数学家们无奈搁置了近30年。

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

该解决方案100%由AI生成，总计耗时6小时。

连顶尖数学家陶哲轩也跑来围观讨论，他在对比了Gemini和ChatGPT的深度研究工具后，发现Harmonic模型对该问题的证明表现更佳。

那么这个被AI破解的问题究竟是什么呢？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模型证明#124简易版的Boris Alexeev也补充道：

在‘形式化猜想’项目中，原本有这个猜想的正式数学表述。但里面有个笔误：注释里写的是≥ 1，而对应的Lean程序代码里写的却是= 1。这个错误让原表述的条件变弱了，即只覆盖了等于 1 的情况，而漏掉了大于 1 的情况。

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

“Vibe证明时代已经到来”

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

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

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

顺着他的发言，我们也去扒了扒Harmonic模型背后的出品方。

根据公开资料，其背后公司名为Harmonic，目标也相当明确：

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

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

CEO Tudored Achim拥有卡内基梅隆大学计算机科学学士学位，同时也在斯坦福大学攻读计算机科学PhD，不过现处于“on leave”状态。

执行主席Vlad Tenev拥有斯坦福大学数学学士学位和加州大学洛杉矶分校数学硕士学位。除了担任Harmonic的联创和执行主席外，他目前还同时在金融公司Robinhood Markets兼任CEO。

根据官网公开资料，Harmonic在大约一周前完成了