AI风暴席卷数学界，人类如何主导
■朱震昕
高小山素描画。
数学研究智能体系统基本架构。图片由作者提供
前不久，第67届国际数学奥林匹克竞赛（IMO）举行，中国代表队夺得团体第一名。赛场外，一场关于AI与数学的较量同样引人注目。多个大模型在此次竞赛中获得了满分成绩，中国科学院数学与系统科学研究院研发的数学研究智能体系统独立攻克了全部6道赛题。
与此同时，2026年国际数学家大会（ICM）上，菲尔兹奖得主陶哲轩在公开演讲中表示，数学正在迎来一场百年新危机，而这场危机正是来自AI。
今年以来，AI攻克数学难题的新闻层出不穷。数学界开始思考：AI时代，数学将走向何方？关于这一问题，中国科学院数学与系统科学研究院研究员高小山，给出了他的答案。
面对AI的迅猛发展，他的回答也在启示我们：科学研究只有主动适应变化、积极拥抱浪潮，才能化挑战为机遇、乘大势而快上；与此同时，拥抱不等于盲从，使用不等于依赖，AI说到底只是一位超级助手，科学研究中最为宝贵的、真正定义科学未来的，永远是人类提出问题的创造力。
我们用的AI，是怎么解决数学题的
问：现在大众经常使用DeepSeek、豆包等AI大模型，不仅和它们对话，还会用来解决数学题。从原理上讲，大模型是如何解答数学题的？
答：大模型解决数学题，本质上还是依靠Transformer架构下的概率生成模型。当我们输入一个数学问题时，模型会根据它在训练时“看过”的海量数学书籍、论文和题库，计算出下一个Token（词元）的概率分布，最终给出它认为正确概率最高的答案。
所谓“概率最高”，意味着在大模型的认知里，最符合已有数学语境，逻辑连贯的答案会被优先生成。比如说，如果你问它一道已知题库里的原题，那么题库里原题的解法就是概率最高的选择，它会直接输出相同的答案。
也正因为是概率解答，有时会产生“幻觉”，给出看似合理、实则错误的证明。
问：此次在IMO中发挥出色的数学研究智能体系统，和大模型有什么不同？
答：首先，目前常用的通用大模型，推理数学题时采用的都是自然语言证明。数学研究智能体系统则可以提供自然语言证明与对应的形式化版本。
我们在数学教科书、学术论文里看到的绝大多数数学证明，都是自然语言证明。简而言之，只要是人能直接阅读、依赖人类逻辑习惯写出来的数学证明，都属于自然语言证明的范畴。
自然语言具有很强的表达能力，但也可能容纳大量隐含信息。例如：“容易看出”中可能藏着一个并不成立的推论、“类似可得”可能遗漏边界情形、证明过程中可能悄悄改变了对象的定义，等等。大模型特别擅长生成结构完整、语气自信、符号漂亮的自然语言文本，即使输出了错误的答案，人类也很难发现漏洞。
与之相比，形式化证明是用一种极其严格的计算机编程语言（如Lean、Coq等）将数学命题和推理规则完全编码。在形式化证明中，每一个推理步骤都必须产生一个逻辑正确的证明项，只要存在条件遗漏、类型错误、循环论证、未证明的中间命题或虚构定理，编译就不能通过。
因此，在底层机制上，形式化证明能保证证明在逻辑上绝对正确，没有任何漏洞。只要一个证明能被完整地写成形式化语言并通过验证器的检验，它就是正确的，不再需要人工审阅。
其次，从架构上，大模型单独面对困难的数学定理时，往往会因为证明步骤太长而产生幻觉。智能体系统通过系统、完整的推理框架反复调用大模型，具备长程推理能力。
数学研究智能体系统将数学研究流程模板化为30多种功能不同的子智能体与工具，并通过三个核心智能体协同工作。其中，自然语言证明器负责生成自然语言数学证明；形式化证明器自动生成或将自然语言证明转化为编译器可核验的形式化代码；数学知识管理器负责组织与归档数学推理历史。最终，编译器会对每一步逻辑进行机器核查，通不过则直接拒绝。
这样做有两个优点：一是能够处理更长、更复杂的形式化证明，比如这届IMO最复杂的第三道组合博弈题，数学研究智能体系统生成了近3000行形式化代码；二是经过检验的形式化证明，正确性较高，且可被独立复现与溯源，从而能够降低证明过程中的幻觉风险。
人类还需要数学家吗
问：AI能为数学研究带来哪些实际帮助？
答：在数学研究中，AI可以在以下几个环节发挥作用：
证明审计。系统可以沿着论文的推理链条逐项检查条件，寻找漏洞、错误引用，并生成反例。
定理证明或证明思路。系统会努力生成定理证明。在不能生成证明的情况下，会告知证明的进展与卡点，以及进一步证明的可能路径。
证明补全与文献检索。数学家给出核心构想后，智能体可以承担大量中间引理补全、库检索等工作。
新结果形式化。对得到的证明进行形式化验证，确保证明的正确性。
符号计算认证。计算机代数系统产生的复杂恒等式、有限分类和计算证书，可以被进一步纳入形式化证明。
长期项目记忆。定义、定理、部分证明、反例和失败路线被组织成可复用的知识图谱，后续工作就不必从零开始。
问：近期，王虹、邓煜荣获菲尔兹奖，引发了公众对数学研究的高度关注。然而，在AI数学解题能力突飞猛进的背景下，有人将2026年的菲尔兹奖称为“最后一届没有AI的菲尔兹奖”，甚至假想以后数学难题都将由AI解决。您对此怎么看？
答：作为相关领域的研究人员，我倾向于更严谨、中肯的看法。
目前的数学智能体，还无法凭空解决像挂谷猜想这样需要开创性理论框架的顶级难题。它更多是扮演研究助手的角色，帮助数学家完成繁琐的推导、在证明“卡壳”时提供建议、加速局部的证明过程。
我认为，AI不会完全取代数学家。提出好问题、提炼核心概念、构建全新理论框架，这些依然是人类的专长。未来AI会成为数学家标配的工具，可能会让我们的研究效率提升数倍甚至十倍，下一届菲尔兹奖的研究成果里大概率会有AI的影子，但主导权依然在人类手中。
