近日，数学界传来一则引人关注的消息：Erdos问题#124的一个弱化版本被成功证明。这一成果由普林斯顿大学数学博士Boris Alexeev完成，他借助Harmonic公司开发的数学AI智能体Aristotle，对问题展开了深入研究并取得突破。
Erdos问题#124的提出可追溯到1984年，当时在《算术杂志》发表的论文《整数幂集的完备序列》中首次提出该问题，此后近30年一直悬而未决，成为数学领域的一大难题。此次Boris Alexeev的证明，虽只是弱化版本，但仍引发了广泛关注。不过，此前一些报道称AI独立解决了该问题的完整版本，这一说法并不准确，还引发了不少争议，Boris Alexeev为此专门进行了修正说明。
在Formal Conjectures项目中，该猜想有正式声明，但声明中存在拼写错误，注释在显示式方程里显示为“≥1”，而相应的Lean声明为“= 1”，这使得声明变弱。Boris Alexeev对此进行了修正，并给出了修正后声明的证明，还删除了他认为不必要的声明部分，而Aristotle也证明了这些删除内容的正确性。有学者指出存在涉及幂次1（对应个位数）的问题，意味着[BEGL96]中的猜想与当前情况不同，Boris Alexeev认为[Er97]中的版本与当前陈述相符，不过目前他无法获取[Er97e]来核实。
尽管此次证明存在一些微妙情况，Erdos问题#124目前仍是一个开放问题，但数学智能体独立证明其较简单版本，已然展现出强大的数学证明能力。Erdos问题#124的具体内容，可在其官方论坛查看相关链接。
数学AI智能体Aristotle是一个用于自动形式化和形式验证的API。据Harmonic公司介绍，它具备利用IMO金牌级引擎解决复杂推理问题的能力，能够自动将英语陈述和证明转换为经过验证的Lean4证明，还能无缝集成到项目中，自动利用用户的整个定理库、定义、依赖项以及Mathlib。
在Erdos问题#124的讨论中，有学者简要介绍了Aristotle针对该问题的证明方法，称其“出奇的简单”。对详细证明过程感兴趣的读者，可参考相关开源仓库中的文件。
著名数学家陶哲轩对AI在数学领域的应用一直保持高度关注，在Erdos问题#124的讨论中也能看到他的评论。陶哲轩认为，数学中的未解决问题如同许多真实世界中的分布一样，呈现出典型的“长尾”结构。其中有很多相对容易、未得到足够关注的问题，借助AI强大的自动化和推理能力，规模化地尝试攻克这些问题，就能收获许多“低垂的果实”。
陶哲轩在去年运行Equational Theories Project时就有过类似体验。该项目针对普遍代数中的2200万个蕴含式展开研究，利用简单自动化方法的最初几轮扫描，在几天内就解决了相当大一部分问题；随后采用越来越复杂的方法，逐步攻克早期扫描中顽固抵抗的剩余实例，最后少数几个蕴含式则花费数月人类努力才解决。陶哲轩以个人日志形式完整记录了该项目的详细过程、方法、结果和个人思考。
Erdos问题网站的情况与之类似，目前收录了1108个在至少一篇埃尔德什论文中提出过的问题，其中既有极其困难的经典难题，也有大量偏门、连Erdos本人都没怎么关注过的问题。如今，陶哲轩开始采用自动化方法，集中清理这些“低垂果实”。几周前，网站上一批原本标注为未解决的问题突然被划为“已解决”，原因是AI驱动的文献搜索工具发现解答早已存在于文献中。研究这些问题的数学家们也结合使用AI工具和形式化证明助手，用Lean验证已有证明、生成问题关联的整数序列项或补全推理步骤。
具体到Erdos问题#124，该问题在三篇论文中被提出，但其中两篇漏掉关键假设，导致问题在那两种表述下成为已知结果（Brown判别法）的推论，这一点直到Boris Alexeev使用Aristotle工具处理问题时才被发现。Aristotle在数小时内就自主找到并用Lean形式化了该弱化版本的解答。目前，研究者正系统性扫描网站上剩余问题，寻找更多类似误述或快速解决方法，短期内主要聚焦“长尾”末端。随着自动化工具能力不断增强，它们不仅能帮助人类数学家清除容易部分，还能让真正困难的问题更加清晰地呈现出来。
