7月6日，中国科学院数学与系统科学研究院（以下简称数学院）发布基于大语言模型的数学研究智能体“数学机械化智能体（MechMath Agent Team，简称MMAT）”，该智能体搭建起了覆盖数学研究全流程的研究框架，是数学家的全新智能研究助手，这标志着我国大模型驱动的定理证明技术实现前沿科研级突破。

经过两个月内部测试验证，MMAT独立或与数学家交互攻克了代数计算理论、微分代数、数论领域8项长期公开问题，比如稀疏多项式计算复杂性与最优算法、广义艾里算子等价问题，以及BSD猜想重要研究内容等。其中2项问题由MMAT全自动独立解决，6项问题的核心关键引理由MMAT完成证明。同时，MMAT还给出了2项难题证明过程的形式化验证，验证结果严谨可靠。

研发团队负责人、数学院研究员高小山介绍，MMAT采用分层多智能体协同的核心设计思路，构建了系统、完整的大模型推理框架。他们首先将数学家的研究思路和环节进行模块化，打造出二十个左右具备专项能力的子智能体；其次，针对不同类型的数学问题，系统可智能调度各子智能体分工协作，自主生成求解方案、完成问题解答，并通过多层迭代机制完成结果核验。

在框架的基础上，研究团队融合子智能体与外部工具，构建了MMAT的三个智能体，实现自主规划定理证明全流程、可自动生成Lean形式化代码，并进行自然语言与形式化语义对齐，以及描绘面向研究对象的数学知识图谱。

相较于传统数学大模型和简易数学智能体，这一设计很大程度上突破了只能给出单一证明、缺乏全局规划、易出现逻辑幻觉、难以开展复杂课题研究等局限，大幅提升了人工智能参与数学研究的能力。

高小山表示，MMAT具备数学知识覆盖面广、问题求解能力突出、逻辑输出稳定性强、无明显幻觉问题等显著优势。同时他坦言，当前，智能体在面对超高难度数学难题时，无法一次性输出完整严谨证明的局限，数学家在研究问题提炼、证明准确性校验、创新思路开拓、全新数学概念引入等环节，依然发挥着不可替代的核心主导作用。

中国科学院院士、数学院研究员田野认为，数学机械化智能体整合大语言模型、知识管理、自然语言证明、形式化验证、符号计算、人机协同等多项技术，构建起了覆盖数学研究全过程的一体化智能系统。这一成果代表了全新数学研究路径，推动人工智能从单一模型输出模式，升级为可审计、可复用、可积累的人机协同科研平台。

中国科学院院士、数学院院长张平指出，数学机械化智能体不只是单项技术的创新突破，更有望推动数学研究范式的深层次变革。展望未来，数学研究将形成全新协同模式：由人类数学家提出科研问题、把控研究方向，大模型开展探索推演与定理证明，数学机械化智能体完成大规模精准计算，形式化系统筑牢科研严谨性底线，四方协同联动，推动人工智能辅助数学研究走得更远、更扎实。