十年前，知乎上就有人问，AI 能在数学上打败人类吗？

昨天，我们在知乎热榜上发现一个整整十年前提出的、现在看来很有意思的问题：

2016 年 10 月 16 日 的凌晨 43 分，一位清华数学专业的知友@何通木 问出了这个问题。

他还补充到：

「如果有朝一日，人工智能可以在数学上全面领先于人类，那人类是否就真的在智力方面完败于人工智能了？」

从这些回答里我们能看到过去十年人们对人工智能的态度变化。

2016 年，AI 在数学上超越人类还是一个遥远而且有些轻松的想象。有人相信计算机迟早能做到，有人认定数学是人类最后的防线。彼时人们谈论这件事时还带着一种置身事外的调侃，奇点只是一个可以从容推演的未来。

十年过去，回头再看这些讨论才发现我们曾经离它那么远，又在不知不觉间走到了这里。

以下是这 10 年的回答。

在一定程度上不难。

并且不需要太强的人工智能，感觉机器学习已经够用了。

麻烦的只是数学系统和知识的编译，不过在一些数学软件和对应的网站里已经有了如 Mathematica 。

主要原因：很多数学证明看起来天马行空，其实是有一定规律的。人工智能难超越的是一些巨系统的现象，如人脑的无数神经元～但是数学的规则限制太多。

对于某一类型题目的证明方向一般最多不会超过10种，再会有一些普遍的可重复的证明方法，软件编程后一种种试，试出来的概率是很高的。比围棋的难度要低。

当然我这里说的题目需要很多类似的题目来提供样本解法和证明方向。

不过很多新的方法很多时候只是多种老方法的组合而已，能有这种计算力去验证各种组合方法的只有电脑了，可能会有惊喜哦。

人工智能可能就是人类的完全体，就算是人类被人工智能代替了，也不能说是坏事啊。

什么时候np=p被证明了 就没数学家什么事了 电脑必然可以证明或者证否任何一个命题

显然不是，智能是一个很复杂的东西，某一件事，比如围棋或者数学，是不能完全说明智能程度的。事实上，在围棋上胜过人类的阿法狗基本上没有任何智能可言，但如果能在数学上碾压人类，那必定是一种可怕的高智能体了，但是否已在智能上全面超越人类还不得而知。我觉得人类目前根本不用担心人工智能，如果有一天人类真创造了超越自己的智能体，人类一定会提前知道的，毕竟创造它一定是以完全了解它为前提的，就像上帝一定完全了解人类一样，如果上帝存在的话。

放心吧，人工智能不会在数学领域超过人类。

数学并不是一个封闭的体系，而是开放的，是对客观世界的高度抽象。随着人类对客观世界的不断认识，数学的外延也不断扩大。

首先，我们把这个问题看成两个子问题：

A： 人工智能数学证明发展到了什么程度。

B： 数学证明是不是最难的问题，以至于我们会考虑为一种「压制」人工智能的防线。

问题 A：

首先，用人工智能证明数学定理其实不是一个新课题，很早很早其实就有 ITP&ATP 领域各种大牛在探索。但是，时至今日，我们刚刚完成了基本的定理积累。换句话说，我们其实刚收集完数据，真正的用大数据，机器学习的方法来做的序幕才刚刚拉开。本人参加了 AITP 的会议，Conference on Artificial Intelligence and Theorem Proving 里面的人也是在探索阶段。从这个会议上「走出来」的 DeepMath 等也都不是很系统的方法。大多数都还是在探索，怎么选择 axiom 这类比较基本的。现在这方面比较好的就是布拉格 Joseph 那个组还有奥地利的 innsbruke 大学吧。总之，还远的嘞！

问题 B：

当然不会是，首先首先，没有几个人类可以掌握那么多定理，而且训练一个人类科学家的成本太高太高了。所以，用大数据机器学习来做数学其实是更合理的。然后，还有很多很多问题我们没有解决，而那些比证明定理可能难很多很多。这里牵扯到一个 proof complexity 的问题。有一些的缺很难，但是整体不是不能做，而是资金和关注度都不够。

综上，人类担心的太多了。

一阶逻辑已经被完全解决了啊。高阶的逻辑，要么已经证明不可能是 decidable 的，要么也都解决了。

就算是 undecidable 的问题，也有类似 Coq 的 tactics 系统，可以有效的给出定理的证明。我觉得一个（强化学习的）神经网络加上蒙特卡洛方法，就可以像 AlphaZero 一样指导自动证明了。

事实上，数学证明与编程语言非常相近，简直就是一样的（Curry-Howard 同构），所以计算机处理数学证明非常方便。

你想怎样个压制法，不懂数学的人不容许从事人工智能领域工作，这样应该能压制一段时间。

数学证明是人类压制人工智能的最后一道防线 , 因为人工智能需要遵循数学原理与定理 , 只有理解与掌握数学 , 才能发展出更强大的人工智能。

数学不是人类压制人工智能的最后一道防线。正相反，数学是人工智能战胜人类的最大帮手。

现在的人工智能其实就是一个应用程序。就好像你手机里面的美团外卖一样。就是一个程序。你把他打开，问他一个问题。他回答。

而人工智能之所以能回答的原因就是：数学。更准确的说是概率论。人工智能通过分析人类所有的资料。之后根据这个资料建立了一个马尔科夫链。造成了能回答你的问题的艺术效果。

如果非要说，人类领先于人工智能的地方。在于人类的物理接触性。就是人啊！！是活在真实的物理世界里的。而人工智能其实活在网络的虚拟环境中。

一个幼儿只要花五六年的时间就能流畅的上下楼。拿取物体。准确的判断物体的属性。是热还是冷。是重还是轻。而人工智能虽然看起来无所不知。其实这些基本的生活技能都很难掌握。就是因为人工智能不接触物理世界。

这是一个整整 10 年前的问题。

时间过得是真的很快啊。

当真，是日新月异的 10 年。

2016 年，谷歌发表了 DeepMath - Deep Sequence Models for Premise Selection，首次将深度学习大规模应用于自动定理证明。这似乎是一条有趣的起点，但实际上确实黎明前最黑的深夜：那时候的 LLM，能让翻译软件想到的唯一含义只是『法学硕士（Legum Magister)』，所能使用的工具也只有的经典『深度学习』范式，文章所尝试的内容只不过是用 CNN、LSTM 或 GRU 去编码一阶逻辑公式再对其进行模式识别，只不过识别的标准是『对证明的重要性』。

从现在的视角来看，这实际上就像是神话中用蜡把羽毛粘在身上后试图飞向太阳的伊卡洛斯：以人类的骨骼构造和胸肌力量，即使给人类完美的翅膀，难道就可能学会飞翔吗？

2017 年 6 月，谷歌发表了新时代真正的奠基之作：Attention Is All You Need，完全舍弃了深度学习中的 RNN/CNN，提出了基于『注意力机制（attention)』的更适用于处理文本上下文信息的 transformer 框架。从此，千年暗室，一灯即明。

和串行的 RNN 不同，attention 是原生的并行架构，天然适合大规模并行计算，在 gpu 充足的情况下能够极致地提高参数量，甚至可以说，只要卡有多少，模型就能做到多大。这件事或许比 attention 本身还要重要。某件很直观的事情终于似乎可以理所当然地发生了：算力有多少，模型就能多大，而模型越大，理论上来说能力也就越强。在不算很久的之后，人们开始把这件看似理所应当的事情叫作『Scaling Law』。

2018 年，某个当时名不见经传的初创公司发表了 Improving Language Understanding by Generative Pre-Training，开始了『无监督预训练』+『具体任务微调』的基本范式。让模型在 7000 本书构成的无标注文本数据集 BookCorpus 先进行预训练，预测一串文本的下一个词；再针对某些具体任务微调模型。

当然，人们似乎还没有真正意识到这种训练方式将成为未来的基本范式，更没有人真正意识到文章标题中的 Generative Pre-Training 的缩写『GPT』在未来将意味着什么。

2019 年，还是那家公司，发表了 Language Models are Unsupervised Multitask Learners。15 亿参数的 GPT-2 出现。这里有个不大不小的标志：文章 conclusion 部分的第一句话是：

When a large language model is trained on a sufficiently large and diverse dataset it is able to perform well across many domains and datasets.

从此，LLM 不再只是『法学硕士』的简称，逐渐拥有了后来更广为认知的含义：『大语言模型（ large language model)』。

2020 年，Scaling Laws for Neural Language Models 把原本模糊的『Scaling Law』精确化，之后就是 1750 亿参数的 GPT-3 出现。2 年后的 11 月，chatgpt 出现了。一夜之间，全世界都知道了那个初创公司的名字：openai。

之后的节点是 23 年推理思维链『Chain of Thought，CoT』和强化学习。此时，数学题成为模型的优质数据来源，是评估和训练模型推理能力的最佳的测试集和训练集。针对数学题的专用模型开始产生。但实际上这似乎可能也是一条弯路。

模型基础能力的提升自然是必要的。但是，对于绝大多数的数学问题来说，都不可能是一蹴而就的结果，都是在不断的猜测试探中摸索着前进的过程。或者，从某种角度来说，『证明即搜索』。所以，试图解决数学问题，不光是模型智力本身够不够高，更是模型能否围绕着某个目标开展持续不断的循环工作，并根据工作的进展动态地理解修改自己的局部目标。

这实际上就是 agent 的作用。综合起来，最初的 transformer 解决了如何把模型做大，scaling law 解释了模型变大后的潜力提升，reasoning model 则可以让模型在单个问题上花费更多的经历，agent 则以模型为大脑，装备了其他工具，并且借助多 agent 系统，把一个模型扩展为了一个完整的研究团队。

这时，以『标准形式化验证』作为反馈机制的数学便成为了检验和训练多 agent 系统能力最佳的试验对象。

之后的故事要从一场堪称无趣的世界杯决赛开始。claude fable 5 举出了以下反例，证否了 3 维及更高维度的雅可比猜想：

再之后，是 2026 年 9 月初的 openai 宣称使用内部模型解决的 NS 问题；再之后，是 10 月 7 日公布于 GitHub 中包含 722 份手稿、涵盖 372 个结果家族的文件。

与次同时，陶哲轩表示现在数学应该从重视『解法』的数学 1.0 时代进入『更加重视理解』的数学 2.0 时代。这是由于在 AI 时代，将解法视作中心的结构已经开始阻碍数学的进一步发展了。所以数学学界的生产关系也要为 AI 生产力所重塑，需要把之前以『解法/证明』为中心的学术结构推倒，重构为以更能激发数学活力的『解法理解』或者其他暂时还没有真正出现的焦点为核心。

最后，我们可以考虑这样一个看似无关的思想实验。

现在假设你得了一种病，现在有两种药可供选择：

第一种的说明书中声称 ai 独立研发了此种药物，并且 ai 提出了一个你看不懂的理论解释了药物的具体作用机制，并且给出一系列你看不懂的实验数据进行验证，并声称此药已经通过 FDA 的三期临床实验。当然，你也没有任何第三方的验证机制。

第二种的说明书中声称专家独立研发了此种药物，并且给出了一个你看不懂的理论解释了药物的具体作用机制，并且给出一系列你看不懂的实验数据进行验证，并声称此药已经通过 FDA 的三期临床实验。当然，你也没有任何第三方的验证机制。

请问，你更倾向于选择哪种药物？

变式： 以下两种情况，何者将可能改变你的想法（即本来不想选，但增加后愿意选）第一种情况中，有一位人类专家（自称）表示他理解 ai 所说的机理。

第二种情况中，你问了 ai 后 ai 表示第二种人类专家的方案是可行的。

当然，很多人还是会选择人类专家。

因为只有人类才有担责的能力。

或许这才是人类的最后一道防线。

阅读更多