30年未解的数学难题被AI证明了？
此时此刻，（原推特）正刮起一阵讨论之风——
Harmonic 的数学AI 模型独立证明了Erds 问题#124，该问题已被数学家们无奈地搁置了近30 年。
微软前AI 副总裁、目前在OpenAI 研究AGI 的Sebastien Bubeck 兴奋地分享了这一消息并表示：
该解决方案100% 由AI 生成，总共花费了6 个小时。
连陶哲轩这样的顶尖数学家都来观看讨论。在比较了Gemini 和ChatGPT 的深入研究工具后，他发现Harmonic 模型在证明这个问题上表现更好。
那么这到底是一个什么样的问题呢？ Harmonic模型如何“大显身手”？
我们来看看——
AI证明了Erd?s问题#124简易版首先需要提醒大家的是，在听了各位专家的讨论后，我们意识到——
事实证明，Harmonic 模型证明的并不是原始的Erds 问题#124，而是一个简化版本。
Erd 的问题#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，但相应的精益程序代码却说=1。这个错误削弱了原表达式的条件，即只覆盖了等于1的情况，而漏掉了大于1的情况。
因此，我纠正了这个错误，并删除了原语句中我认为不必要的部分。最终，人工智能成功证明了这个更简单、更准确的版本。
综上所述，Harmonic 证明了问题#124 的简单版本，而困难版本仍然开放。
“Vibe证明时代已经到来”尽管如此，大佬们还是肯定了AI模型证明数学问题的潜力。
提及编程领域Vibe Coding的概念（由AI大师Kapasi首次提出），Harmonic联合创始人兼CEO兴奋地说：
我们正处于数学领域深刻变革的边缘，Vibe 证明时机已经到来。
听完他的演讲，我们还去了解了Harmonic模型背后的制造商。毕竟，在陶哲轩眼中，这一次击败了ChatGPT和Gemini。
公开资料显示，其背后的公司名为Harmonic，其目标相当明确：
构建世界上最先进的数学推理引擎。
两位联合创始人是Tudor Achim 和Vlad Tenev。
CEO Tudor Achim 拥有卡内基梅隆大学计算机科学学士学位，同时也在斯坦福大学攻读计算机科学博士学位，但目前正在“休假”。
2023 年，他与Vlad Tenev 共同创立了Harmonic，希望打造世界上最先进的推理引擎。
此前，他曾担任自动驾驶辅助系统开发公司（Helm.ai）的联合创始人兼首席技术官。
执行主席Vlad Tenev 拥有斯坦福大学数学学士学位和加州大学洛杉矶分校数学硕士学位。
除了担任Harmonic 联合创始人兼执行董事长外，他目前还担任金融公司Robinhood Markets 的首席执行官。
官网公开信息显示，大约一周前，哈雷完成了1.2亿美元（约合人民币8.5亿元）C轮融资。
本轮融资由Ribbit Capital领投，估值达到14.5亿美元（约合人民币103亿元）。
Harmonic的旗舰模型是这次使用的亚里士多德模型（也称“亚里士多德”）。据悉，它是第一个为2025年国际数学奥林匹克竞赛中的5道题提供形式化验证解的模型。
亚里士多德在确保准确性并消除幻想的同时实现了金牌级别的表现。
据Vlad Tenev介绍，这次使用的亚里士多德进行了一些更新，拥有更强大的推理能力和自然语言界面。
可以预见，随着人工智能解决复杂数学问题的能力不断突破，越来越多被“搁置”的百年难题将重见天日，有望一一攻克。
无论如何，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
