2026年7月6日上午，中国科学院数学与系统科学研究院（以下简称数学院）举行“数学机械化智能体”（MechMath Agent Team，简称MMAT）成果发布会，数学院院长、中国科学院院士张平，数学院学术副院长、中国科学院院士田野，中国科学院院士郭雷团队代表，中国科学院基础科学研究局数学天文力学处处长沈连成等出席发布会，发布会由数学院副院长黄飞敏主持。

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

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

郭雷院士团队代表赵成副研究员介绍，团队在大模型辅助下，解决了机械臂 PID 控制领域悬而未决四十余年的全局稳定性问题，形成了从关键稳定性证明、参数设计到高维反例构造的完整结果。他指出，AI是概率生成模型，需通过多轮交互、严格核查激发其创造力，研究者应保持判断力，将机器输出转化为可靠知识。

随后，"数学机械化智能体"研发团队负责人高小山研究员介绍了定理自动证明发展概述、"数学机械化智能体"的构建思路和实验结果。经过两个月内部测试验证，MMAT独立或与数学家交互攻克了代数计算理论、微分代数、数论领域8项长期公开问题，比如稀疏多项式计算复杂性与最优算法、广义艾里算子等价问题，以及BSD猜想重要研究内容等。其中2项问题由MMAT全自动独立解决，6项问题的核心关键引理由MMAT完成证明。同时，MMAT还给出了2项难题证明过程的形式化验证，验证结果严谨可靠。他指出，MMAT具备数学知识覆盖面广、问题求解能力突出、逻辑输出稳定性强、基本无幻觉问题等显著优势。同时他坦言，当前，智能体在面对超高难度数学难题时，无法一次性输出完整严谨证明，数学家在研究问题提炼、证明准确性校验、创新思路开拓、全新数学概念引入等环节，依然发挥着不可替代的核心主导作用。

在交流环节，十余位现场听众就MMAT的技术构架、使用方法、能力拓展等方面与高小山研究员进行了热烈讨论。

MMAT以"数学机械化"命名，既因其核心工具源于数学机械化与符号计算，亦为纪念吴文俊先生关于定理自动证明的远见卓识。高小山研究员表示，团队未来将建成数学家的助手，把我国数学机械化传统、基础数学优势与新一代人工智能技术真正结合，使其成为数学共同体可以信任和共同建设的长期基础设施。