数学定理证明，作为检验人工智能科学推理能力的关键场景，正迎来一场变革。中国科学院数学与系统科学研究院的科研团队，在定理自动证明领域取得了突破性进展，他们研发的数学机械化智能体（MechMath Agent Team，简称MMAT），为数学研究带来了新的可能性。
数学定理证明的严格性，要求每一步推理都必须从给定假设出发，通过可接受的规则到达结论。这一过程中，任何遗漏条件、混淆量词或关键环节的失误，都可能导致整个证明链的崩溃。而困难证明往往涉及复杂的知识检索、路线选择、引理构造、反例排除和符号计算，这对人工智能提出了极高要求。MMAT的研发，正是为了应对这些挑战。
MMAT并非单一的大语言模型，而是一个集成了模型、专用算法、外部工具和专家反馈的协同系统。其目标是在数学研究的全流程中，将文献查询、路线探索、证明生成、反例搜索、计算验证、形式化以及知识积累等环节，转化为可管理的工作过程。这一设计理念，源于对数学机械化和符号计算工具的深度整合，以及对吴文俊关于计算机成为数学家重要研究工具设想的延续。
与直接调用大语言模型进行对话相比，MMAT的关键变化在于将研究活动转化为可反复执行的闭环。在单次对话中，研究者需要亲自规划、追问、整理上下文和调用工具；而在MMAT中，这些环节被显式纳入工作流，系统可以自主安排路线、概要、引理、验证和修正，并将中间结果整理为报告供人检查。这种人机协作模式，极大地压缩了机械性的组织工作，使专家能够将注意力集中在问题提炼、关键判断和方向修正上。
MMAT的整体架构General Harness，可视为大语言模型的“操作系统”。它将数学研究中的常用步骤模板化为约20个功能型子智能体，并与计算和验证工具共同形成30多种功能单元。一个编排器依据执行图与任务清单统一调度各单元，各子智能体在相互隔离的工作区中完成任务，通过文件传递结果，以减少冗余上下文、信息混乱和多智能体冲突。MMAT还汇总成功经验、失败路线和未解障碍，为长周期项目保留可复用的记忆。
在MMAT中，三类核心智能体发挥着关键作用。自然语言证明器NL-Prover，遵循“生成-校验-修正”的闭环，将证明活动分配给不同角色的子智能体执行，包括检索者、探索者、综合者、概要生成者、生成者、验证者、审计者、反例搜索者、调节者和代码执行器等。形式化证明器FL-Prover，则负责生成Lean 4代码形式的定理证明，或将自然语言证明转化为可编译、可核验的形式化版本。数学知识管理器KB-Manager，则围绕具体研究课题建立本地知识图谱，统一登记和关联文献、概念、已证引理、Lean代码、中间证明、失败思路与障碍点。
外部工具的支持，是MMAT实现可验证闭环的关键。系统可调用的工具包括Lean、程序执行环境、符号计算方法、吴方法、SAT/SMT求解器以及精确线性规划和精确平方和工具等。大语言模型擅长提出方向和连接知识，数学机械化与符号计算在确定范围内提供强计算能力，交互式证明系统负责严格核验。MMAT的作用，正是按任务将这三者组织起来，改善长任务规划、路线探索、反例与假设审查、工具调用、上下文管理和结果可追溯性。
在内部测试中，MMAT展现了其强大的能力。在约两个月的测试期间，它独立或与数学家交互处理了11个数学问题，其中包括代数计算理论、微分代数和数论领域的8项长期公开问题，形成了9篇arXiv论文。其中，4项结果由MMAT完全自动证明，另有7项由MMAT完成核心关键引理。稀疏多项式项目是一个典型案例，研究者通过多轮人机交互，在MMAT中解决了四个公开问题，证明了有限域上稀疏多项式整除判定为CoNP难等重要结论。
国际数学奥林匹克竞赛（IMO）的测试，进一步验证了MMAT的实力。在2026年7月举行的IMO上海竞赛中，MMAT对六道题均生成了自然语言解答及Lean形式化证明。这一结果不仅展示了MMAT在自然语言证明与形式化方面的端到端测试能力，也综合检验了其数学路线选择与形式化工程能力。然而，科研团队也指出，IMO题目的成功并不能直接外推为系统已普遍具备研究级定理证明能力，更不能替代专家对新概念、研究价值和理论体系的判断。
在使用MMAT时，研究者还应区分输出层次并落实核验。探索性输出用于发现路线和障碍，可以容许未闭合的分支；自然语言证明需要专家逐条检查；形式化证明则以Lean编译与依赖检查为验收标准。当智能体给出错误证明或不可验证结论时，研究者应定位最早失效的引理，记录失败原因，补充反例或文献，并将修正后的条件写回项目知识库。
从系统科学的视角看，MMAT的设计体现了局部与整体、分散与统一相协调的思想。它将完整证明流程拆解为约20类功能子智能体、30余种计算核验单元，划分NL-Prover、FL-Prover、KB-Manager三大核心子系统，各子智能体拥有独立工作区，通过标准化文件交互，实现分散模块与统一研究目标的协调平衡。这一设计有助于缓解单一大模型在长推理链中可能出现的条件遗漏、上下文碎片化和任务冲突等问题。
MMAT的研发，标志着数学研究智能体从单一解题工具向基础支撑型系统基础设施的转变。它融合了大模型智能体、吴文俊数学机械化、交互式形式证明三类技术，打通了文献、推理、计算、核验、知识沉淀的完整链路。在这一过程中，机器与数学家优势互补，共同推动数学研究向可持续、可验证的协作过程演进。
