中国AI首次攻克数学未解难题并完成形式化证明

近日，北京大学北京国际数学研究中心传来消息，董彬教授率领的AI4Math研究团队依托自主研发的人工智能框架，成功破解了交换代数领域一项悬而未决的猜想——安德森猜想，并在Lean编程语言与定理证明环境中完成了近19000行的形式化论证工作。此举标志着我国首次利用人工智能框架解决交换代数开放难题并完成大规模形式化验证，为数学与人工智能的深度融合开拓了新路径。

该猜想由美国学者安德森在2014年首次提出，其核心研究对象是“准完备局部环”的某些特性。此类环主要用于代数化描述几何体在局部区域（例如某个点的邻域）的无穷小形态及其形变规律。此后十余年间，该猜想一直未能取得实质性进展。

本次突破的关键，在于北大AI4Math团队独创的双智能体协同架构。该架构包含两大核心组件：负责自然语言推理的智能体Rethlas，以及专司形式化验证的智能体Archon。

在具体研究过程中，Rethlas借助团队自主研发的Matlas语义检索引擎，从海量数学命题中准确识别出表面关联性较弱的整环完备化理论，并基于此构建出反例。紧接着，Archon将上述证明转译为近19000行Lean代码，期间自主侦测到原始方案中潜藏的逻辑缺陷，进而重构了形式化证明的完整技术路径。面对Lean形式化数学库未收录必要概念的情况，自主探寻出等效替代方案，最终生成的代码涵盖了6篇外部文献的核心结论。相较资深Lean专家，其完成同等量级形式化工作的效率提升逾10倍。

这一突破得益于团队长达三年的技术沉淀与多学科协同攻关。北大AI4Math团队于2023年正式成立，该团队由一批对该研究领域具有共识的学者自发集结而成，队伍成员涵盖代数数论、优化理论、机器学习与人工智能等多个专业背景。

董彬在接受采访时表示，团队坚信，对于AI进行严谨的数学推理而言，检索能力至关重要。为此，团队构建了LeanSearch与Matlas双引擎检索体系。其中LeanSearch支持通过自然语言描述实现定理的语义级检索，目前已获Lean官方社区普遍采纳。Matlas则收录了上千万条数学命题，可实现命题层面的语义检索。基于这些底层技术支撑，团队成功开发出上述两大AI智能体。

中国科学院院士、北京大学数学科学学院院长刘若川评价道，此次研究不仅攻克了具体数学难题，更印证了人工智能与数学交叉融合的全新科研范式。中国科学院院士田刚对此呼吁，应当激励青年科研人员勇于创新，深化AI与数学的交叉研究，使之在国家重大科技攻关中发挥关键效能。（记者张盖伦）