AI导读：

北京大学AI4Math团队用自主构建的AI框架解决了交换代数中的开放问题——安德森猜想，并完成了大规模的形式化验证。该成果不仅解决了具体数学问题，更验证了AI与数学融合的新研究范式。

6日，记者从北京大学北京国际数学研究中心了解到，该中心董彬教授课题组与合作者组建的AI4Math团队用自主构建的自动化AI框架解决了交换代数中一个开放问题——安德森猜想，并在用于形式化验证数学定理正确性的编程语言和定理证明器——Lean中完成了约19000行的形式化验证。此次解决安德森猜想，北京大学AI4Math团队搭建的双智能体协作框架功不可没。该框架由自然语言推理智能体Rethlas和形式化验证智能体Archon组成。研究中，Rethlas通过团队自研的Matlas自然语言语义检索系统，从上千万条数学陈述中精准定位到与猜想看似无关的整环完备化理论成果，以此构造反例。随后，Archon将证明转化为约19000行Lean代码，并在过程中自主发现初始方案存在隐含的逻辑漏洞，重新设计了形式化证明的整体技术路线，最终完成的代码覆盖6篇外部论文关键结果。