数学机械化智能体(MMAT) 的研究路径与实践

　　赵成、薛文超、高小山

　　中国科学院数学与系统科学研究院

　　CICC自抗扰控制专业委员会

　　一、定理证明：检验人工智能推理的“试金石”

　　数学定理证明之所以成为检验大语言模型科学推理能力的重要场景，不只因为题目难，更因为证明有明确而苛刻的有效性标准。一个结论必须从给定假设出发，经由可接受的推理规则到达；局部看似合理的语句，只要遗漏条件、混淆量词或在一个关键环节失效，整条证明链就不能成立。与此同时，困难证明往往需要检索既有知识、选择路线、构造引理、排除反例、执行符号计算，并在失败后回到前序环节修正。知识调用、规划、计算、审查和长期记忆在同一任务中汇合，使定理证明成为观察人工智能能否由“生成答案”走向“组织研究”的理想窗口。

　　这项挑战有深厚的历史背景。希尔伯特在20世纪初提出公理化纲领，并于1928年明确提出判定问题，希望用统一算法判断公理系统中命题的真伪。哥德尔不完备性定理揭示了形式系统的内在界限；Herbrand则为一阶逻辑给出半判定思路，即只要证明存在，原则上可以自动生成；图灵则为“判定”提供了精确数学模型。到符号人工智能时期，Newell和Simon的“逻辑理论机器”、Robinson的归结法展示了自动推理的可能性，但Cook关于命题逻辑可满足性问题为NP完全问题的结果，又说明了完整且高效的通用证明算法受到计算复杂性的根本制约。

　　此后的实践形成了两条互补路线。交互式定理证明不要求计算机从头发现证明，而是让Isabelle、Rocq、Lean等系统核验证明的逻辑准确性；数学机械化则在适当且有意义的数学范围内发展专门高效算法。吴文俊开创的几何定理机器证明，以及此后形成的计算机代数、计算数论、计算代数几何和符号分析等方向，都体现了后一思想。前者强调可核验性，后者强调特定问题上的可计算性。这两条路线没有因为大语言模型的出现而变得无用，反而为大语言模型生成证明的正确性验证、弥补大语言模型计算能力弱短板提供了有力工具[1]。

　　图1. 定理自动证明发展的四个阶段[2]

　　二、从大语言模型到数学研究智能体

　　大语言模型具有广泛的数学知识记忆、语言表示和泛化能力，能够提出证明思路或补全局部推导。然而，困难数学问题通常不能通过一次对话获得完整证明。模型还可能在长链条中遗漏条件，计算能力也需要符号工具补足；自然语言证明与可由形式系统核验的证明之间，更存在明显能力鸿沟。直接让单一模型“从题目写到结论”，难以稳定完成研究级任务。

　　中国科学院数学与系统科学研究院数学机械化实验室因此研发了数学机械化智能体（MechMath Agent Team，简称MMAT）。它的目标不是把一个大模型包装成聊天工具，而是在数学研究全流程中组织模型、专用算法、外部工具和专家反馈，使文献查询、路线探索、证明生成、反例搜索、计算验证、形式化以及知识积累成为可管理的工作过程。“数学机械化”这一命名也指向两层传承：智能体以数学机械化和符号计算为核心工具来源，同时延续吴文俊关于计算机成为数学家重要研究工具的设想。

　　与大语言模型对话相比，智能体的关键变化是把研究活动变成可反复执行的闭环。单次对话中，研究者通常要亲自规划、追问、整理上下文和调用工具；在MMAT中，这些环节被显式纳入工作流。系统可以按问题自主安排路线、概要、引理、验证和修正，并把中间结果整理为报告供人检查。对于高难度问题，人机交互仍不可缺少，但智能体能够压缩机械性的组织工作，使专家把注意力集中在问题提炼、关键判断和方向修正上。

　　图2. “数学机械化智能体”成果发布会现场[3]

　　三、“Agent Team”如何形成协同系统

　　（一）General Harness：可调度的整体架构

　　MMAT由整体架构General Harness和三个面向研究任务的智能体组成。General Harness可形象地理解为“大语言模型的操作系统”。它将数学研究中的常用步骤模板化为约20个功能型子智能体，并与计算和验证工具共同形成30多种功能单元。一个编排器依据执行图与任务清单统一调度各单元；各子智能体在相互隔离的工作区中完成任务，通过文件传递结果，以减少冗余上下文、信息混乱和多智能体冲突。MMAT还汇总成功经验、失败路线和未解障碍，为长周期项目保留可复用的记忆。

　　（二）三类核心智能体

　　第一类核心智能体是自然语言证明器NL-Prover。它遵循“生成-校验-修正”的闭环，把证明活动分给不同角色的子智能体执行：检索者查找外部结果，探索者提出备选路线，综合者合并方案，概要生成者搭建证明结构，生成者补全步骤，验证者检查正确性，审计者检查假设与可行性，反例搜索者尝试否定错误命题，调节者诊断失败原因，代码执行器验证计算，最后再由精炼和写作角色整理结果。这里的“团队”不是多个模型简单投票，而是不同角色围绕同一证明对象分工，并通过检查结果触发回退和重做。

　　第二类是形式化证明器FL-Prover。它负责生成Lean 4代码形式的定理证明，或把自然语言证明转化为可编译、可核验的形式化版本，同时检查自然语言陈述与形式化陈述的语义对齐。形式化验证能够提供比语言判断更强的正确性保障，但目前NL-Prover的能力显著强于FL-Prover。Kolyvagin系统、复杂性理论中的NP难证明等领域缺少足够的形式化基础，许多自然语言证明尚不能完整转写为Lean代码，因此“已生成自然语言证明”不能自动等同于“已机器核验”。

　　第三类是数学知识管理器KB-Manager。它围绕具体研究课题建立本地知识图谱，统一登记和关联文献、概念、已证引理、Lean代码、中间证明、失败思路与障碍点。数学研究常跨越多轮讨论和较长时间，若只依赖对话上下文，重要条件和失败经验容易碎片化。KB-Manager把这些内容转化为可查询、可维护的项目资产，为后续路线探索提供状态和依据。

　　（三）外部工具与可验证闭环

　　外部工具把上述协作闭环落到可检查的计算对象上。系统可调用的工具包括Lean、程序执行环境、符号计算方法、吴方法、SAT/SMT求解器以及精确线性规划和精确平方和工具等。大语言模型擅长提出方向和连接知识，数学机械化与符号计算在确定范围内提供强计算能力，交互式证明系统负责严格核验；MMAT的作用正是按任务把三者组织起来。相比单一模型直接生成证明，它主要改善了长任务规划、并进行路线探索、反例与假设审查、工具调用、上下文管理和结果可追溯性，但这些机制降低错误风险，并不构成对所有输出的正确性担保。

　　图3. MechMath Agent Team 1.0整体架构[2]

　　四、从公开问题到研究级协作

　　（一）内部测试与稀疏多项式项目

　　在约两个月的内部测试中，MMAT独立或与数学家交互处理了11个数学问题，其中包括代数计算理论、微分代数和数论领域的8项长期公开问题，形成9篇arXiv论文。4项结果由MMAT完全自动证明，另有7项由MMAT完成核心关键引理。

　　稀疏多项式项目体现了“长期项目”而非“单题作答”的工作方式。研究者在MMAT中建立专门项目，积累文献和中间知识，并通过多轮人机交互解决了四个公开问题：证明了有限域上稀疏多项式整除判定为CoNP难，证明了有限域上输出敏感型稀疏多项式最大公因子计算为NP难，给出了整系数稀疏多项式乘法的拟线性时间算法，以及把Erd s-Rényi关于完全幂稀疏性的结果推进到多变量情形。这个案例说明，智能体可以在有关联的一组问题之间复用文献、定义和引理，也能通过反例生成帮助发现既有证明中的问题。

　　图4. 稀疏多项式基础计算项目[2]

　　（二）人机协作与自动证明流程

　　广义Airy算子等价问题则展示了人机协作。MMAT直接尝试完整问题时未能得到结论，但随后分别从整体方法和局部方法得到强、弱次数公式。数学专家提示弱公式可能加强为强公式，系统再在Katz条件下利用强公式完成证明。这里最有价值的并非“机器独立发现一切”，而是失败被保留并转化为后续交流的依据，机器提供可用的中间结构，专家识别真正的突破口。

　　与BSD猜想相关的CM椭圆曲线Shafarevich-Tate群问题更能说明边界。智能体尝试移植Kolyvagin系统时遇到剩余表示非满射和上同调群不消失等障碍；在专家补充文献与要求后，系统证明某种方法可在带误差项的条件下移植，并得到特定情形下可能适用的阶段性结论。该问题尚未被彻底解决。这个案例说明，MMAT可用于暴露障碍、验证局部路线并推进研究，而非保证把每个重大猜想闭合为完整定理。

　　一个具有代表性的全过程自动证明案例展示了MMAT从问题分析、方案搜索到证明生成和结果检查的完整工作过程。系统先审查问题，两轮构建并排序证明路线，形成概要和证明，将目标分成五个引理，随后集中处理唯一未解决的第二引理。第一条下降路线在大量分类、阿基米德困难和若干非周期情形上失败；第二条路线融合候选方法，并借助精确线性规划处理大量锥与困难情形，最终完成引理，再生成自然语言证明和Lean证明。该案例说明MMAT能够记录失败、改变路线并调用专用计算工具，但单个成功流程不能证明同样规模的搜索对任意问题都有效。

　　图5. MMAT全过程自动证明工作流程[2]

　　内部测试表明，与直接调用单一大模型相比，NL-Prover通过多轮生成、校验、反例搜索和修正机制，能够显著降低证明过程中的幻觉和逻辑错误。对于其最终生成的完整证明，多数经人工检查或形式化验证后表现出较强的逻辑严谨性。

　　五、IMO 2026：自然语言证明与形式化的端到端测试

　　2026年7月15日至16日，国际数学奥林匹克竞赛在上海举行。MMAT对六道题均生成了自然语言解答及Lean形式化证明[4]。实验在关闭网络访问和网页搜索的离线沙箱中进行，用以排除模型获取外部解题信息的可能。每道题公开三个核心文件：原问题的形式化陈述、完整的机器检查证明，以及供数学读者阅读的解答[5]。

　　六题构成了紧凑而多样的测试集。第一题和第六题属于数论，分别涉及整数操作的终止性与不变性、递归数列的质因数和周期性；第二题以复数坐标连接欧氏几何约束与代数恒等式；第三题是区间细分上的组合博弈，需要同时建立博弈值的上下界，其形式化代码达到2983行，是六题中工作量最大的一题；第四题是以三角形角度和递归必胜位置表述的几何博弈；第五题是正实数上的函数不等式，形式化过程中先处理根式不等式平方变换的等价条件，再推出函数的结构约束。

　　这一结果值得关注：六道题均给出了通过机器检查的Lean形式化证明，而不仅是自然语言答案；同时，题型涵盖数论、组合、博弈、不等式和几何，综合检验了数学路线选择与形式化工程能力。但也应指出，IMO题目有明确陈述和有限知识范围，六题成功不能直接外推为系统已普遍具备研究级定理证明能力，更不能替代专家对新概念、研究价值和理论体系的判断。

　　六、科研人员如何正确、高效地使用MMAT

　　（一）选择问题并准备输入

　　目前，较适合交给MMAT的任务主要有三类：能够复用文献中已有技巧的问题、可通过分类搜索或显式符号计算推进的问题、研究者正在持续开展并能够及时提供反馈的课题。最后一类尤其重要，因为困难问题往往需要专家解释背景、判断中间信息是否有价值，并在系统停滞时提供新文献或新方向。相反，若问题陈述尚不清楚、评价标准无法明确，或突破依赖全新概念的发明，智能体目前并不占优势。

　　以下做法应理解为结合系统工作方式提出的实践建议，而不是宣称MMAT已经自动替用户完成全部准备。提交问题时，应明确对象、符号、量词、假设、目标和允许使用的已有结果，并附上必要定义、关键文献和已有引理。对复杂课题，应建立独立Project，由KB-Manager持续登记来源、概念、部分证明和障碍，再把总目标拆成可以分别审查的路线、概要和引理。输入越精确，后续的反例搜索、语义对齐和形式化检查越有可操作的基准。

　　（二）区分输出层次并落实核验

　　研究者还应在开始时区分所需产物。探索性输出用于发现路线和障碍，可以容许未闭合的分支；自然语言证明强调数学读者可理解，但仍需专家逐条检查；形式化证明以Lean编译与依赖检查为验收标准，严谨性更强，却受形式化知识基础和工程成本限制。若形式化条件具备，应优先争取机器核验；若暂时不能形式化，则应重点核查关键推导、边界情形、隐含假设、引用结果的适用范围，并主动要求系统构造反例或重新审计。

　　（三）把失败转化为项目知识

　　当智能体给出错误证明、遗漏条件或不可验证结论时，不宜只要求它“重写一遍”。更有效的做法是定位最早失效的引理，记录失败原因，补充反例或文献，把修正后的条件写回项目知识库，再从受影响的节点重新规划。全过程自动证明和Airy算子案例都说明，失败路线本身可以成为下一轮搜索的状态信息。与此同时，实际部署还需要准备大语言模型接口、编码智能体、Lean环境以及与课题相适配的符号计算或求解工具；基座模型能力和Harness设计共同决定系统表现。

　　无论采取何种工作方式，最终把关仍属于数学专家。形式化代码需要确认形式化命题确实表达了原命题；自然语言证明需要确认每一步和全部边界条件；阶段性计算需要确认其模型、精度与适用域。更重要的是，提炼值得研究的问题、搭建理论框架、发明概念和评判成果价值，仍是人类数学家的核心职责。

　　七、系统科学视角下的MMAT系统

　　从系统科学的视角看，科学智能体的设计不宜仅停留在任务的简单拆分，还需要协调局部模块的相对自治与全局目标的统一 [6]。MMAT 将 General Harness 作为全局调度核心，依托任务执行图统筹全部资源，将完整证明流程拆解为 约20 类功能子智能体、30 余种计算核验单元，划分 NL-Prover、FL-Prover、KB-Manager 三大核心子系统。各子智能体拥有独立工作区，通过标准化文件交互，减少信息冗余与多主体冲突，实现分散模块与统一研究目标、多元推理角色与同一证明对象的协调平衡。这有助于缓解单一大模型在长推理链中可能出现的条件遗漏、上下文碎片化和任务冲突，体现了系统科学中局部与整体、分散与统一相协调的思想。

　　反馈与调控是系统科学的重要思想，也是MMAT工作流的重要组织机制。MMAT 形成了 “规划 - 执行 - 观测 - 修正” 闭环运行结构：编排器统筹分配整体任务，各类功能子智能体负责局部推导模块，KB-Manager 留存全流程证明状态，形式化核验、反例搜索构成核心反馈回路，外部各类符号求解工具提供确定性符号与逻辑校验。NL-Prover 严格遵循 “生成 - 校验 - 修正” 机制，划分检索者、探索者、验证者、反例搜索者等多类分工角色协同完成证明推导，校验识别错误后自动回退重做；FL-Prover 生成 Lean 4 代码，完成自然语言证明向可编译形式化文本转化，核对两类文本语义一致性。系统可调用吴方法、SAT/SMT 求解器、精确线性规划等工具，对其适用范围内的符号计算、有限分类和关键推导进行可检查验证。反馈回路有助于发现并修正量词混淆、条件缺失等推导偏差，提高长链条推理的稳定性和可检查性；多路线并行搜索则可以拓展候选证明思路，为数学家提供新的启发。

　　MMAT 并非单一解题工具，而是面向数学科研领域的基础支撑型系统基础设施，融合大模型智能体、吴文俊数学机械化、交互式形式证明三类技术，打通文献、推理、计算、核验、知识沉淀完整链路。现阶段，多数前沿复杂数学问题仍需数学家与MMAT等数学智能体协同研究，人机紧密协作有望成为提升定理证明效率与可靠性的重要路径。在这一过程中，机器既可承担文献检索、大规模分类和符号计算等高强度工作，也可参与证明路线探索、候选证明生成和关键引理求解；数学家则主要负责核心问题提炼、理论框架构建、新概念创造以及最终的正确性核验与学术价值判断。二者优势互补，共同推动数学研究由单次问题求解向可持续、可验证的协作过程演进。

　　八、结语

　　MMAT所展示的核心进展，不是让一个模型写出更长的证明，而是把大模型推理、数学机械化、符号计算、自然语言推理、形式化验证、知识管理和人机协作组织成一个可迭代的智能体团队。

　　实验验证说明它能够参与研究级路线探索和关键引理证明；IMO 2026项目则提供了从自然语言求解到Lean核验的集中测试。两类证据共同表明，大语言模型驱动的数学研究正在从“会答题”走向“能参与流程”。这一转变具有现实价值，也要求科研人员坚持精确定义、工具验证、专家审查和适用范围意识。只有在这些条件下，智能体生成的候选推理才可能沉淀为可靠、可复用的数学知识。