陶哲轩谈AI攻克数学难题：自动化工具推动数学研究新突破

近期，数学领域传来一则振奋人心的消息：Erdos问题#124的一个弱化变体被成功攻克。这项成果由普林斯顿大学数学博士Boris Alexeev完成，他借助Harmonic公司开发的数学智能体Aristotle，对这一猜想展开了深入的探索并取得了重要突破。

Erdos问题#124的源头可以追溯到1984年，当时发表在《算术杂志》上的论文《整数幂集的完备序列》首次提出了这一难题。在随后的近三十年里，该问题一直悬而未决，成为数学界公认的硬骨头。虽然Boris Alexeev此次证明的只是该问题的弱化形式，但仍然引发了学术圈的广泛关注。值得注意的是，此前曾有报道声称AI独立解决了该问题的完整版本，这一说法实际上并不准确，还引发了不少争议，为此Boris Alexeev还专门作出了澄清说明。

在Formal Conjectures项目中，这一猜想虽有正式声明，但声明中存在拼写错误——注释在显示方程里呈现为“≥1”，而对应的Lean声明却是“=1”，这使得声明的强度被削弱。Boris Alexeev对此进行了修正，不仅给出了修正后声明的完整证明，还删除了他认为冗余的声明部分。而Aristotle也验证了这些删除内容的正确性。有学者指出，涉及幂次1（对应个位数）的问题意味着[BEGL96]中的猜想与当前情形有所不同，而Boris Alexeev则认为[Er97]中的版本与当前陈述相符，不过目前他尚无法获取[Er97e]来核实这一细节。

尽管此次证明过程中存在一些微妙之处，Erdos问题#124目前仍然是一个开放课题，但数学智能体能够独立证明其简化版本，已经展现出强大的数学推理能力。若想了解Erdos问题#124的具体内容，可以通过最新的学术论坛查看相关链接。

数学智能体Aristotle实际上是一个用于自动形式化验证的API工具。据Harmonic公司介绍，它具备利用国际数学奥林匹克竞赛金牌级引擎解决复杂推理问题的能力，能够自动将英语陈述和证明转换为经过验证的Lean4证明，还能无缝集成到项目中，自动调用用户整个定理库、定义、依赖项以及Mathlib资源。

在关于Erdos问题#124的讨论中，有学者简要介绍了Aristotle针对该问题的证明方法，称其“简洁而巧妙”。对详细证明过程感兴趣的读者，可以参考开源仓库中的相关文件。

著名数学家陶哲轩对AI在数学领域的应用一直保持高度关注，在Erdos问题#124的讨论中也能看到他的精彩点评。陶哲轩认为，数学中的未解难题就像真实世界中的分布情况一样，呈现出典型的“长尾”结构。其中有很多相对容易、却未得到足够关注的问题，借助AI强大的自动化和推理能力，系统化地尝试攻克这些问题，就能收获许多“低垂的果实”。

陶哲轩在去年运作Equation Theories项目时就有过类似体验。该项目针对普遍代数中的2200万个蕴含式展开研究，利用简单自动化方法进行最初几轮扫描，在几天内就解决了相当大部分问题；随后采用越来越复杂的方法，逐步攻克早期扫描中顽固残留的实例，最后少数几个蕴含式则花费了数月的人类努力才得以解决。陶哲轩以个人日志形式完整记录了该项目的详细过程、方法、结果和个人思考。

Erdos问题的情况与此类似，目前收录了1108个在至少一篇埃尔德什论文中提出过的问题，其中既有极其困难的经典难题，也有大量冷门、连Erdos本人都没怎么关注过的问题。如今，陶哲轩开始采用自动化方法，集中清理这些“低垂果实”。几周前，上一批标记为未解决的问题突然被划为“已解决”，原因是AI驱动的文献搜索工具发现答案早已存在于文献中。研究这些问题的数学家们也结合使用AI工具和形式化证明助手，用Lean验证已有证明、生成问题关联的整数序列项或补充推理步骤。

具体到Erdos问题#124，该问题在三篇论文中被提出，但其中两篇遗漏了关键假设，导致问题在那两种表述下成为已知结果（Brown判别法）的推论，这一点直到Boris Alexeev使用Aristotle工具处理问题时才被发现。Aristotle在数小时内就自主找到并用Lean形式化了该弱化版本的解答。目前，研究者正在系统性扫描剩余问题，寻找更多类似误述或快速解决方法，短期内主要聚焦“长尾”末端。随着自动化工具能力不断增强，它们不仅能帮助人类数学家清理容易部分，还能让真正困难的问题更加清晰地显现出来。