AI“数学家”首秀：北大团队破解十年数学谜题

数学猜想就像一座座没有地图的迷宫。以前，只能靠数学家一步一步摸索。目前，AI不仅能自己找到出口，还把整个探路的过程变成了精准的图纸。

近日，北京国际数学研究中心董教授课题组与合作者组建的AI4Math团队，在国际数学界投下一枚“重磅炸弹”。他们用自主构建的自动化AI框架，成功解决了交换代数中一个开放了十余年的难题——安德森猜想，并在定理证明器Lean中完成了约19000行的形式化验证。这是国内首次实现AI自主解决数学开放问题并完成大规模形式化验证，标志着中国在“AI for Math”这一前沿领域跻身第一梯队。

安德森猜想由美国数学家安德森于2014年提出，关注的是交换代数中“准完备局部环”的性质。通俗来说，它尝试用代数语言来准确描述几何对象在某一点附近的“微观结构”。该猜想提出后，十余年间无人给出完整证明，属于典型的“开放问题”——而非已知答案的习题。

与以往AI辅助人类证明不同，此次北大团队搭建的AI框架独立完成了从思路生成、逻辑推导、到代码验证的全流程。过程中，AI自主发现初始方案的逻辑漏洞并重构了技术路线，最终完成的代码覆盖了6篇外部论文的关键结果，同等规模的形式化工作效率较经验丰富的Lean专家提升至少10倍。

该成果的背后是团队三年的技术积累与跨学科协作。2023年，北京大学AI4Math团队正式组建，它由一群对这个方向有共同判断的人逐步自然汇聚而成，团队成员来自代数与数论、优化、机器学习与人工智能等方向。

理解这项技术，可以将其比作从“盲目翻书”到“全自动推理流水线”的跨越。

传统数学家面对一个难题，需要从海量文献中寻找关联线索，再手动推导、验证。这就像在图书馆里盲目地翻阅每一本书，靠直觉和运气寻找灵感。北大团队的AI框架由两位“AI研究员”搭档协作：

第一是Rethlas（推理智能体）：相当于一位“文献猎手”。它通过自研的Matlas语义检索系统，从上千万条数学陈述中精准定位到一条与安德森猜想看似毫不相关的“整环完备化”理论成果，并以此成功构造反例。这就像它从一堆看似无关的积木中，发现了能卡住关键结构的那一块。

其次是Archon（验证智能体）：相当于一位“代码精算师”。它将Rethlas找到的思路转化为约19000行准确的Lean代码。在此过程中，它甚至自主发现了人类初始方案中的逻辑漏洞，并在Lean数学库缺失某些概念时，自主找到等价替代路径，重新设计了整套形式化证明的技术路线。

为了让这两位AI能够高效工作，团队还打造了双引擎检索架构——LeanSearch和Matlas。LeanSearch用自然语言描述需求即可语义检索出相关定理，现已被Lean官方社区广泛使用；Matlas则覆盖上千万条数学陈述，支持命题级语义检索。

长期以来，数学研究依赖个人天赋和长期积累，进展缓慢。北大AI4Math团队的成果，首次验证了AI能够自主解决前沿开放问题，标志着数学研究正从“人类孤军奋战”迈入“人机协同共进”的新阶段。

当前，全球科技巨头都在争相布局“AI for Math”。2026年2月，谷歌DeepMind发布了数学研究智能体Aletheia，在数学研究领域取得了实质性成果，包括独立撰写6篇学术论文和解决4项开放问题。2026年1月，谷歌Gemini已证明了一个代数几何领域的新定理。在这场激烈的全球竞赛中，北大团队的突破表明国家已跻身第一梯队，具备与国际巨头同台竞技的实力。

董教授强调，让AI做严肃数学推理，检索最为关键。北大团队自主研发的LeanSearch和Matlas检索系统，实现了从底层算法到应用工具的全链条自主可控。

这打破了国外在高端数学研究工具上的技术壁垒，为我国科研工作者提供了自主可控的“智能研究助手”。从“手工推演”到“智能协同”，AI正在重塑数学。

另外，你可能不知道，AI解决数学问题的速度远超想象：北大AI4Math团队完成19000行形式化验证的效率，较经验丰富的Lean专家提升至少10倍。谷歌DeepMind的Aletheia在国际数学奥林匹克基准测试中，以91.9%的成绩刷新了最新技术标准。2026年3月，DeepMind的AlphaEvolve系统以每秒处理40亿种可能性的速度，远超人类数学家的大脑神经处理速率。

最后，当AI能自主证明定理后，未来的数学家该做什么？——是设计问题、解释结果，还是与AI“共舞”？