问题——长期开放猜想对数学理论体系提出更高要求。安德森猜想是交换代数中备受关注的开放问题之一，涉及整环完备化等核心结构的性质判定，并与代数几何、数论等方向的多种理论工具涉及的。这类问题通常需要大量文献和多条技术路线之间反复比对、拼接与校核：证明链条长、依赖结论多，任何细小的逻辑缺口都可能让整体推进受阻，成为研究中的关键难点。 原因——双智能体协作与检索体系提升推理与校核能力。团队介绍，此次工作基于自主研发的双智能体协作框架：一端负责自然语言推理与线索发现，另一端负责形式化证明与机器可检验的逻辑闭合。自然语言推理智能体Rethlas依托自研的Matlas语义检索系统，从上千万条数学陈述与知识片段中定位与猜想相关的关键结果，为证明路径提供可直接落地的参考。随后，形式化验证智能体Archon将整体证明转写为约19000行Lean代码，在严格的形式系统中逐条核验推演关系，并在验证过程中发现初始方案的逻辑漏洞，进而调整技术路线、补齐关键环节。针对形式化数学库尚未覆盖的概念与引理，Archon通过寻找等价表述与替代构造完成补全，最终形成覆盖6篇外部论文关键结果的可检验证明链条。团队表示，在相近规模的形式化工作量下，该自动化框架的效率较经验丰富的Lean专家提升至少一个数量级。团队三年来的技术积累，以及代数与数论、优化与机器学习等方向的交叉协作，为此次突破提供了方法与工程支撑；由LeanSearch与Matlas组成的“双引擎检索架构”，也强化了“找得到、用得上、验得过”的闭环能力。 影响——为数学证明的可复核与可复用提供新路径。业内人士指出，此次成果的价值不仅在于推进单个猜想，更在于展示了“自然语言发现线索—形式化系统封装证明”的工作流程：一上——借助大规模检索与推理辅助——缩短从问题到可行思路的探索周期；另一方面，通过形式化验证把证明过程转化为可重复、可审计、可复用的代码资产，降低复杂证明出错风险，提升学术结果的透明度与可复用性。北京大学数学科学学院院长、中国科学院院士刘若川表示，此类探索验证了数学研究的新范式；中国科学院院士田刚指出，应深入支持青年学者大胆创新，国家亟需的重大科技问题上增强基础研究供给能力。 对策——完善平台、人才与开放生态，夯实基础研究“底座”。受访专家认为，要推动这类方法规模化应用，需要在三上协同发力：其一，持续建设高质量数学知识库、语义检索与形式化库，推动重要定理与经典工具以可检验形式沉淀；其二，完善交叉学科培养与评价机制，让数学、计算与工程人才围绕同一研究目标高效协作；其三，推动更开放的工具链与数据共享，在确保学术规范与安全合规的前提下，降低研究门槛，形成可持续的科研基础设施。 前景——从“辅助计算”迈向“可验证发现”，科学研究组织方式或将重塑。随着形式化数学库扩展、检索与推理算法持续进步，未来在更多数学分支乃至物理、材料、生命科学等领域，机器可检验的推理链条有望更深度嵌入科研流程：既帮助研究者从海量信息中提炼关键线索，也在成果发布前提供更严格的逻辑校核。专家同时提示，这个趋势也会带来新的边界与治理议题，包括代码化证明的标准化、成果署名与贡献度衡量、工具可靠性评估等，需要学界与管理部门提前研判并开展。
基础研究的每一次突破，都是对人类认知边界的推进；此次我国科研团队在数学领域的创新实践，不仅推动了一个具体问题的解决，也展示了技术赋能科研的新路径。在建设科技强国的进程中，这种面向前沿、敢于突破的探索，有望催生更多高质量成果，为全球知识体系贡献中国方案。