AI数学推理新突破：Harmonic模型独立证明Erdős问题简易版，开启数学证明新范式

2025年12月1日下午1:17 • AI产业动态 • 阅读 433

近日，数学与人工智能交叉领域迎来一项里程碑式进展——AI研究公司Harmonic开发的数学推理模型Aristotle，独立证明了困扰数学家近30年的Erdős问题#124的简易版本。这一突破不仅展示了AI在复杂数学推理方面的强大能力，更可能预示着数学研究范式的深刻变革。

**数学难题的AI解法**

Erdős问题#124是一个典型的组合数论问题，其核心在于探讨“进制生成器”系统的覆盖能力。具体而言，给定k个不同的进制生成器（对应数字d₁, d₂, …, dₖ），游戏规则允许从每个生成器产生的数字列表中至多挑选一个数字，将这些数字相加，目标是判断是否能够凑出任意足够大的目标整数。问题的关键条件在于：当1/(d₁-1) + 1/(d₂-1) + … + 1/(dₖ-1) ≥ 1时，是否所有大整数都能被表示？

该问题自提出以来，数学家们取得了渐进式进展。在原版问题中，由于限制条件严格（禁止使用数字1且需满足gcd条件），仅对特定集合{3, 4, 7}证明了猜想成立。而当条件放宽后（允许使用数字1且无需额外gcd条件），问题演变为“简易版本”，这正是Harmonic模型成功攻克的对象。

**AI证明的技术细节**

Harmonic模型采用的证明方案被数学社区评价为“出乎意料的简单”。模型通过形式化方法，严谨地证明了当上述条件满足时，所有足够大的整数确实可以被表示。值得注意的是，在“形式化猜想”项目中，原表述存在一个关键笔误：注释中写的是≥1，而对应的Lean程序代码中却是=1。这个错误导致原表述只覆盖了等于1的情况，而漏掉了大于1的情况。

Harmonic的研究人员Boris Alexeev修正了这一错误，并删除了原表述中不必要的部分，最终使得AI成功证明了这个更简洁、更准确的版本。整个证明过程由AI独立生成，耗时仅6小时，并已通过Lean形式化验证，确保了数学严谨性。

**行业反响与意义**

这一成就引起了数学和AI社区的广泛关注。微软前AI副总裁、现OpenAI AGI研究员Sebastien Bubeck激动地分享了这一消息，强调该解决方案“100%由AI生成”。顶尖数学家陶哲轩也参与讨论，他在对比了Gemini和ChatGPT的深度研究工具后指出，Harmonic模型在该问题上的证明表现更优。

Harmonic联合创始人兼CEO Tudor Achim援引编程领域的“Vibe Coding”概念，激动地表示：“我们正处于数学领域深刻变革的边缘，Vibe证明时代已经到来。”这一表述凸显了AI驱动数学发现的潜在范式转变。

**Harmonic公司与Aristotle模型**

Harmonic是一家专注于数学推理引擎开发的AI公司，由Tudor Achim和Vlad Tenev联合创立。Achim拥有卡内基梅隆大学计算机科学学士学位，并在斯坦福大学攻读计算机科学博士学位（目前休学），此前曾担任自动驾驶辅助系统公司Helm.ai的联合创始人兼CTO。Tenev则拥有斯坦福大学数学学士和加州大学洛杉矶分校数学硕士学位，目前还兼任金融公司Robinhood Markets的CEO。

公司旗舰模型Aristotle（亦称“亚里士多德”模型）是首个在2025年国际数学奥林匹克竞赛中为五道题提供形式化验证解决方案的AI模型，达到了金牌级别的表现。该模型在保证准确性和消除幻觉的同时，展现了强大的数学推理能力。据Tenev透露，此次使用的Aristotle模型经过更新，具备了更强大的推理能力和自然语言界面。