国内首次实现AI自主解决数学开放问题

来源：科技日报

6日，记者从北京大学北京国际数学研究中心了解到，该中心董彬教授课题组与合作者组建的AI4Math团队用自主构建的自动化AI框架解决了交换代数中一个开放问题——安德森猜想，并在用于形式化验证数学定理正确性的编程语言和定理证明器——Lean中完成了约19000行的形式化验证。这是国内首次以AI框架攻克交换代数开放问题并实现大规模形式化验证，开辟了数学与AI深度融合的更多可能。

安德森猜想由美国数学家安德森于2014年提出，它关注的是“准完备局部环”的一类性质——这类环旨在用代数工具刻画几何对象局部（如某点附近）的无穷小结构与变形。该猜想提出后十余年始终无人突破。

此次解决安德森猜想，北京大学AI4Math团队搭建的双智能体协作框架功不可没。该框架由自然语言推理智能体Rethlas和形式化验证智能体Archon组成。

研究中，Rethlas通过团队自研的Matlas自然语言语义检索系统，从上千万条数学陈述中精准定位到与猜想看似无关的整环完备化理论成果，以此构造反例。随后，Archon将证明转化为约19000行Lean代码，并在过程中自主发现初始方案存在隐含的逻辑漏洞，重新设计了形式化证明的整体技术路线，还在所需数学概念于Lean形式化数学库中尚未收录时，自主找到等价替代路径，最终完成的代码覆盖6篇外部论文关键结果，完成同等规模形式化工作的效率较经验丰富的Lean专家提升至少10倍。

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

董彬告诉科技日报记者，团队认为，让AI做严肃数学推理，检索最为关键。他们打造了双引擎检索架构——LeanSearch和Matlas。LeanSearch用自然语言描述需求即可语义检索出相关定理，现已被Lean官方社区广泛使用。Matlas则覆盖上千万条数学陈述，支持命题级语义检索。在这些基础设施之上，他们搭建了前述两个AI智能体。

北京大学数学科学学院院长、中国科学院院士刘若川指出，此次探索不仅解决了具体数学问题，更验证了AI与数学融合的新研究范式。中国科学院院士田刚由此呼吁，应鼓励和支持青年学者大胆创新，进一步推动AI与数学的深度融合，并在国家急需解决的重大科技问题中发挥关键作用。