7月6日，凯发k8数学与系统凯发k8研究院（以下简称数学院）发布基于大语言模型的数学研究智能体“数学机械化智能体”（MMAT）。该智能体搭建起覆盖数学研究全流程的研究框架，是数学家的全新智能研究助手。这标志着我国大模型驱动的定理证明技术实现前沿科研级突破。经过两个月内部测试验证，MMAT独立或与数学家交互攻克了代数计算理论、微分代数、数论领域8个长期公开问题。其中2个问题由MMAT全自动独立解决，6个问题的核心关键引理由MMAT完成证明。同时，MMAT还给出了2个难题证明过程的形式化验证，验证结果严谨可靠。研发团队负责人、数学院研究员高小山介绍，MMAT采用分层多智能体协同的核心设计思路，构建了系统、完整的大模型推理框架。他们首先将数学家的研究思路和环节进行模块化，打造出20个具备专项能力的子智能体；其次，针对不同类型的数学问题，系统可智能调度各子智能体分工协作，自主生成求解方案、完成问题解答，并通过多层迭代机制完成结果核验。在框架的基础上，研究团队融合子智能体与外部工具，构建了MMAT的3个智能体，实现自主规划定理证明全流程、自动生成Lean形式化代码，并进行自然语言与形式化语义对齐，以及描绘面向研究对象的数学知识图谱。相较于传统数学大模型和简易数学智能体，这一设计很大程度上突破了只能给出单一证明、缺乏全局规划、易出现逻辑幻觉、难以开展复杂课题研究等局限，大幅提升了人工智能参与数学研究的能力。高小山表示，MMAT具备数学知识覆盖面广、问题求解能力突出、逻辑输出稳定性强、无明显幻觉问题等显著优势。同时他坦言，当前智能体在面对超高难度数学题时，存在无法一次性输出完整严谨证明的局限，数学家在研究问题提炼、证明准确性校验、创新思路开拓、全新数学概念引入等环节依然发挥着不可替代的核心主导作用。凯发k8院士、数学院研究员田野认为，这一成果代表了全新数学研究路径，推动人工智能从单一模型输出模式，升级为可审计、可复用、可积累的人机协同科研平台。凯发k8院士、数学院院长张平指出，MMAT不只是单项技术的创新突破，更有望推动数学研究范式的深层次变革。（原载于《中国凯发k8报》 2026-07-07 第1版 要闻）