当AI已经拿下奥数满分，未来人类还需要数学家吗？|定理|推理|数学家|翻译

来源：市场资讯

（来源：中国科普博览）

编者按 :

2026年7月16日，第67届国际数学奥林匹克竞赛（IMO）在上海落幕，中国队荣获团体第一名。而在赛场外，一场关于AI与数学的较量同样引人注目。多个大模型在此次竞赛中获得了满分成绩，中国科学院数学与系统科学研究院研发的 MechMath Agent Team（以下简称MechMath）独立攻克了全部六道赛题，并自动实现了形式化。

如今，用DeepSeek等AI大模型解决数学题，早已进入了数学教育和日常生活场景中。MechMath又是什么，和我们平时用的大模型有什么不同？当AI连IMO的难题都能独立攻克，未来人类还需要做数学题吗？数学家会不会失业？

关于这些问题，我们采访了MechMath项目团队负责人、中国科学院数学与系统科学研究院高小山研究员，揭秘这一重大进展背后的技术逻辑，以及分享他对AI辅助数学发展的观点。

问：现在大众经常使用DeepSeek、豆包等AI大模型，不仅和它们对话，还会用来解决数学题。从原理上讲，大模型是如何解答数学题的？

高小山：大模型解决数学题，本质上还是依靠Transformer架构下的概率生成模型。当我们输入一个数学问题时，模型会根据它在训练时“看过”的海量数学书籍、论文和题库，计算出下一个 Token（词元）的概率分布，最终给出它认为正确概率最高的答案。

所谓“概率最高”，意味着在大模型的认知里，最符合已有数学语境、逻辑连贯的答案会被优先生成。比如说，如果你问它的一道它已知题库里的原题，那么题库里原题的解法就是概率最高的选择，它会直接输出相同的答案。

本质上，大模型是生成概率上最优的解答，所以有时会产生“幻觉”，给出看似合理、实则错误的证明。

大模型根据问题，生成正确概率最大的答案

对于“1+1=？”问题，2的正确概率显著高于3、car、tv等答案

问：MechMath不仅对IMO的六道题目实现全自动生成题目解答，还提供了自然语言证明与对应的形式化版本。能请您解释下什么是自然语言证明和形式化语言证明吗？

高小山：我们在数学教科书、学术论文里看到的绝大多数数学证明，都是自然语言证明。哪怕里面夹杂着大量符号、希腊字母和公式，只要是人能直接阅读、依赖人类逻辑习惯写出来的数学证明，都属于自然语言证明的范畴。

2026年IMO第一题，题干属于自然语言

自然语言具有很强的表达能力，但也可能容许大量隐含信息。例如：“容易看出”中可能藏着一个并不成立的推论、“类似可得”可能遗漏边界情形、证明过程中可能悄悄改变了对象的定义等等，这些问题在人类阅读时可能很难发现。

目前常用的通用大模型，对数学题采用的都是自然语言证明。这些大模型还特别擅长生成结构完整、语气自信、符号漂亮的自然语言文本，即使输出了错误的答案，人类也很难发现漏洞。

与之相比，形式化证明是用一种极其严格的计算机编程语言（如Lean、Coq等）把数学命题和推理规则完全编码。在形式化证明中，每一个推理步骤都必须产生一个类型正确的证明项，只要存在条件遗漏、类型错误、循环论证、未证明的中间命题或虚构定理，编译就不能通过。

因此，在底层机制上，形式化证明能保证证明在逻辑上绝对正确，没有任何漏洞。只要一个证明能被完整地写成形式化语言并通过验证器的检验，它就一定是正确的，不再需要人工审阅。

Lean语言中的形式化证明

问：既然形式化证明能保证绝对正确，为什么数学家没有将自然语言所写的证明，全部转化为形式化语言？现在大模型的出现又带来了什么改变？

高小山：原因很简单——成本太高。将自然语言证明转化为形式化证明，对语言的要求极严、书写极度耗时。转化一个困难的的证明，往往需要耗费数学家数天甚至数周的时间。

事实上，Lean等形式化语言已经出现了几十年。然而，人类的基础数学知识库绝大多数还是使用自然语言表述，这就导致大规模形式化在过去几乎是不可能完成的任务，也缺乏相应的投入。

但在大模型出现后，情况发生了巨大改变。大模型可以极大地加速从自然语言证明到形式化证明的自动翻译过程，也能辅助生成形式化代码本身。可以说，大模型让沉寂多年的数学形式化工作重新焕发了生机，国内外很多团队都在借助大模型做大规模的数学知识形式化。

问：此次团队研发的MechMath是如何通过形式化证明来解决IMO题目的？

高小山：第一步是形式化建模。拿到题目后，MechMath 做的第一件事不是着急算答案，而是把自然语言描述的题目（比如涉及整数、几何图形或函数不等式）翻译成机器能懂的形式化证明语言。

第二步是智能体自主推导。MechMath能够通过多步规划来寻找证明路径。比如这次届IMO第三道组合题，模型需要自主处理有序分段长度和博弈值边界。在这个过程中，它会像数学家一样，尝试不同的策略，直到找到那条逻辑通畅的路。

第三步是全自动翻译与验证。模型会把找到的自然语言证明，自动转换成 Lean 代码。最后，Lean验证器会对这段代码进行扫描。只有当所有代码都通过了依赖检查，没有任何逻辑漏洞，才能认定问题得到了完全解决。

为了保证公正性，MechMath全程配备了离线沙箱环境，全程关闭网络访问与网页搜索，保证模型无法获取外部解题资料，所有证明结果均为模型独立自主生成。

模型生成自然语言证明（NL）与Lean形式化证明（FL）的耗时对比

问：MechMath是一个智能体，和大模型有什么本质不同？

高小山：大模型单独面对困难的数学定理时，往往会因为步骤太长而产生幻觉。MechMath智能体的设计更为完整，采用了分层多智能体协同的核心设计思路，构建了系统、完整的大模型推理框架。

MechMath将数学研究流程模板化为 30 多种功能不同的子智能体与工具，并通过三个核心智能体协同工作——NL-Prover（自然语言证明器）负责生成自然语言数学证明，FL-Prover（形式化证明器）自动生成或将自然语言证明转化为 Lean 4 编译器可核验的形式化代码，KB-Manager（数学知识管理器）负责组织与归档数学推理历史。最终，Lean 4 编译器会对每一步逻辑进行机器核查，通不过则直接拒绝。

这样做有两个显著突破：一是能够处理更长、更复杂的形式化证明，比如这届IMO最复杂的第三道组合博弈题，MechMath生成了近 3000 行形式化代码；二是经过 Lean 验证器检验的形式化证明，其正确性由Lean语言内核保证，可被独立复现与溯源，从而极大降低了证明过程中的幻觉风险。