中国AI 80小时破解十年数学难题

据4月4日发布在arXiv预印本平台上的一篇论文，北京大学的研究团队开发了一套人工智能系统，该系统在无需任何人工数学判断的情况下，独立完成了一个悬而未决数学猜想的求解与验证——这一猜想由一位美国数学家于十余年前首次提出，而AI仅用约80小时便完成了全部工作。

这一问题被称为安德森猜想，由爱荷华大学教授丹·安德森于2014年提出。安德森于2022年辞世，享年73岁。这一源于交换代数领域的猜想，自提出以来多年悬而未决。

北京大学团队由数学家董斌领衔，构建了一个双智能体AI框架，通过整合数十年的数学文献积累，有效衔接了自然语言推理与形式化机器验证之间的鸿沟。该系统采用一个名为Rethlas的推理模块，并借助数学定理搜索引擎Matlas来探索解题策略，其工作流程与人类数学家的研究方式高度相似。

研究人员写道：“借助这一框架，我们成功解决了交换代数中的一个公开问题，并在几乎无需人工干预的情况下自动完成了证明的形式化。”南华早报

该AI系统在80小时的计算运行时间内完成了证明，完成了通常需要多个数学领域专家协作才能完成的任务。研究团队指出：“人工操作员无需作出任何数学判断。”不过他们也承认，如果让数学家参与其中，或许可以进一步加快进程。

这篇尚未经过同行评审的论文，将这一成果定位为AI驱动的数学研究自动化已发展到何种程度的有力佐证。研究人员写道：“这项工作提供了一个具体案例，证明利用AI可以在相当程度上实现数学研究的自动化。”

北京大学的这一突破，是人工智能系统攻克数学难题这一浪潮的最新成果。今年早些时候，OpenAI的GPT-5.4解决了FrontierMath基准测试中一道自2019年以来令研究人员束手无策的难题；与此同时，一家名为Axiom的AI初创公司也宣布于今年二月攻克了四道此前悬而未决的数学难题。这一系列进展令数学界既振奋又不安——数学家们正努力适应人工智能在这一领域日益扩大的影响力。