三局输给阿法狗，痛哭后的柯洁认为人类没有一个沾到围棋真理的边，在数学机器人面前，谁是最理解数学的人？ 第1页

本文首先在我的博客和爱发电发布，转载请务必注明作者和来源。

问题问的很_____，无论如何，我们就来聊聊计算机证明数学这个话题。

最早关注这个话题是四年前了，这么多年也读过一些文献和讨论，了解了不少例子。结合数学上的经历，粗浅的编程经验，自己也做了多次思考，下面就来简单谈一谈。

一些看法不一定对，但感觉很多是中文社区上其他任何人都没提过的。看法会随着时间发展变化，只有更多实践和思考才会告诉我们真知。

（讨论不可避免的会涉及一些big words，而为了突出重点，对它们的描述是不够全面的。）

首先，"数学机器人"真的被造出来了吗，有哪些"数学机器人"？

回答这个问题，首先就要问，数学有什么特点？

数学是一套系统性的、严格、不断发展的知识理论体系，可以作为工具来解决各种问题。

数学论文的格式是严谨的，开头是介绍和致谢，然后是（定理叙述-定理证明-定理注记）的逻辑推演，最后是参考文献。

数学需要新的理论和新的例子，需要想象力和创造力，求真求美，而不是单纯的重复检验。

这是书和文章教给我们的三个"常识"。

对于特定的数学理论，除了没听说过它们是什么的人之外，还有三类人，他们是用户（User），贡献者（Contributor），创造者（Creator），对应上面这三个"常识"。

实际上，大部分人是这三类人的混搭，哪种更多取决于我们谈论是哪一个具体理论，讨论的是哪一篇文章。为了突出重点，我只能刻板地谈一谈。

如果你想找一个粗糙的类比，开源软件社区里就有这三类人，使用软件的用户，提出问题/修改代码/解决bug的贡献者，软件开发者本身。

如果你还想找一个更粗糙的类比，独立游戏的社区里也有这三类人，玩游戏的玩家，制作攻略或mod / 指出bug / 参与测试 的贡献者，游戏开发者本身。

当然你也可以问计算机能不能写开源软件、做独立游戏。但请注意数学的不同领域差异极大，一些领域的难度非常大，社区非常小，生产关系还停留在很原始的年代，不能一概而论。

现在我们聊一聊这三类人，以及计算机能不能扮演他们的角色。

一. 用户（User），计算机编程

随着时代的发展，数学日益复杂，不同领域的人可能完全无法理解对方在干什么，有什么目标。甚至一个领域的工作者也未必熟悉很多前人的工作和证明，而是当成黑箱来使用，在这个基础上创新，给出新结论的证明。为了"严谨性"，文章都会标上参考文献。

很多人学习新的数学知识，目标是应用或简单了解，为了追求效率，会承认一些结论，只求"直观上"的理解，直接作为工具使用。就像手机用户能用手机干很多事，却不需要了解手机运行的原理一样，这是正常的经历。

用户是大多数人。面对【真理无穷时间有限】的困境，用户(User)会有意识/无意识地做出妥协，承认黑箱的存在。理论已经被前人做好了，我只需享受前人的成果，记一下结论和定义。

看起来似乎没有什么问题。真的么？

①如果一篇古老的参考文献有错怎么办？

那一错皆错，如果世界上懂这些东西的专家不过个位数，他们没有发现或者修正，那错误将会一直保留并传递下去，导致不可避免的麻烦，结论的"严谨性"变成笑谈，变成"信则有，不信则无"的主观判断。这想必是大多数人不想看到的。

这里发生的错误，既有可能是逻辑错误，也可能是打印错误。说起来可能好笑，确实有很多这样的例子，因为论文打印错误，后面引用的大批文章出现问题。这其实不是用户(User)的毛病，但用户没有能力去判断错误，导致了错误的进一步传递，之后的用户成了受害者。

②如果接受的黑箱太多怎么办？

那用户可能最后完全不理解这个东西是怎么回事，连用都不会用，或者是多次错误的使用，结果无法保证自己得到了正确的结果。这是第三种错误，理解错误。

所以人们常说学习知识要多看多理解，而不是只记住结论。因为很多时候，肤浅的理解会导致错误的判断，依赖直觉和几个特例得出来的经验可能完全不符合一般规律。

③用户需要更强的结论怎么办？我可能需要的不是这个黑箱，而是这个黑箱的一个更强版本。这时候用户就遭到了困难，难以解决这个问题。

避开这些问题不谈，计算机能够成为数学的用户(User)么？答案是肯定的。

实际上，你想好了算法，再写出代码让计算机运行的这个过程，计算机就已经部分扮演了用户的角色。

比起人脑，机器更擅长处理重复机械的计算任务，只要这次输入的数据能保证它在有限步停止。

暴力穷举是最简单也最常见的方法，只不过因为运算资源的问题，我们需要合适的算法减少计算的复杂度。

算法是一切的关键，而AlphaGo在围棋这个问题上打败了柯洁，是因为它的算力远远超过了人类，能够找到"按算法的标准"更优的下一步策略，而算法的胜利离不开设计者的努力和输入的大量数据（它之前的对战数可远超一个人一生能下的棋局数）。

又比如"困扰数学家90年的猜想，被计算机搜索30分钟解决了"这种标题吸引眼球的文章，里面做的也是暴力枚举的工作。

人设计算法，机器按照指令一步步去求出合适的解，完成赋予的任务，这远远谈不上真正的数学。

就像你会8位数的乘法，会背圆周率后100位，都不应该算是理解了这方面的数学，当然前者至少是规律的运用，后者只是直接的背诵。

但也许它们已经很有用了。高斯当年发现二次互反律是基于他手算的很多例子，而现代也有数学家通过计算机编程算一些具体的例子（Sagemath了解一下），来试图找规律，你不能说计算机的发明对数学的发展没有用处。

有一个期刊叫做Experimental Mathematics，很多人都在上面发过计算机算的例子和自己的猜想。

好，回到之前的三个问题，应该怎么解决？那就需要有"人"来理解证明，保证结论和证明的正确性，让用户能可靠地使用结论。

二. 贡献者（Contributor），计算机辅助证明与形式化

怕什么真理无穷，进一寸有一寸的欢喜。

证明正在逐渐变得复杂，而数学应该保持证明的严格。

修正错误并指出正确的证明，是数学家这个群体的一个"常识"。而随着数学日益变得复杂，我们需要更多人重新整理以前的内容，改正错误。

正如我在之前一个数学回答https://www.zhihu.com/question/26767399/answer/1464241237所说，成为一个contributor，而不仅仅是user，是一件很棒的事。这就好比给开源项目做贡献一样，看起来你自己在浪费时间浪费赚钱的机会，实际上这有助于你自己成为一个creator，有助于他人。

举例来说，哪怕是著名的代数几何教材EGA，也有错误(如https://arxiv.org/abs/1403.5814)。虽然很多人现在也在引用EGA这套书，但你会发现愿意认真看EGA等古老教材的人越来越少了，大家当成黑箱用就好了，管它那么多干啥。问题就来了：如果你要用的冷门结论是错的呢？可惜EGA是法语写的，字体古老，甚至不会用证明终止号，你未必会去查，如果以后别人构造出你结论的反例，你这篇工作该怎么收场？

一些大数学家在听报告时，喜欢疯狂问问题，就是为了保证证明确实能过得去。

再举例来说，很多发布在顶级杂志上的文章，在十年二十年后才有人看出问题所在，结论是不对的，导致文章被撤稿。还有一种可能是，只有圈内人才知道某篇文章是错的，而它还挂在某某杂志上，然后你不知不觉中使用了它的结果...

再举例来说，我们都知道文章要有几个审稿人来检验你的证明，但是你发现了解你文章知识的专家少之又少，可能找不到审稿人。而且审稿人也是义务劳动没有工资，他有别的事要做，很长时间之后才能确认你的证明给出修改意见。你只能漫长的等待...

好，想必你已经大概能想象检验证明这件事很枯燥很难做，但却值得去做。如果机器能帮我们解决这件事，我们就轻松多了。

那计算机能够成为数学的贡献者(Contributor)么？答案是还在发展的计算机辅助证明与形式化。

这个故事很长，有机会我们慢慢聊。可以先看看《计算机辅助证明简介》这篇文章

https:// zhuanlan.zhihu.com/p/18 1671237

(待补充)

三. 创造者（Creator），计算机自主发现与证明

那计算机能够成为数学的创造者(Contributor)么？

有一些小例子，例如平面几何的一些解题机器。

遗憾的是，它们不够"创造"。

我们需要输入题目，题目需要满足一定的模式，它们负责扮演好"做题家"的角色，做好这一类题。自动化定理证明（Automated theorem proving）的实现需要我们首先对这一套东西比较熟悉，

同样遗憾的是，这些例子超级少，它们也不够"前沿"。

大部分现代领域关心的数学问题，和计算机辅助证明一点关系都没有（虽然Buzzard等人已经做了一些现代数学的实验），更不要提自动证明了。

二十年前是如此，现在也是如此，更不用说数学也在发展，新的数学理论仍然还在出现，只是更为复杂，计算机辅助证明还是跟不上进度。

数学在创造新事物这一方面，是一门艺术。你很难把艺术这种东西量化，让机器去理解。

而你看文章，和人讨论，然后灵感出现，找到感兴趣的问题这个过程，也没法让计算机做到。

人究竟是怎么理解一个谜题并解出它的？人究竟是怎么发现事物的内在规律并学习的？这实在是一个很难回答的问题。

我玩过很多逻辑解谜游戏，知道有一些人在做这方面的研究，从计算复杂性理论我们是可以谈论一个谜题有多难的，只要规则给定。

这又是可以展开聊一晚上的话题，我暂且打住，倒是推荐一个解谜游戏

见证者 The Witness by Jonathan Blow

https://store.steampowered.com/app/210970/The_Witness/
(待补充)

四. 一些重要的例子

一些初等数论结果的证明，基于解析数论的工具，可以证明充分大的整数n都是对的，有时候甚至能给出具体的界（比如说对大于10000000000000000000000的整数n），那比较小的整数n可以交给计算机来检验是否正确。可惜，我们现在计算机的算力，还是不够高。

像2013年Helfgott严格证明了三元哥德巴赫猜想：每一个不小于7的奇数都可以写成三个素数之和，就是进一步降低了之前的界（1939年Borozdin就证明了大于3^{14348907}的奇数都可以写为三个素数之和，然而这根本没法枚举），最后用计算机枚举。这是一个User的例子。

另外我们知道四色定理的证明，最早需要借助计算机穷举 (User），后来有了辅助证明+形式化（Contributor)。

有限单群分类的结果非常漂亮，但它的证明耗时50年，加起来有几百篇文章，几万页的篇幅，这过程中还发现了一些计算错误（2008年都有人发现了）。

所以人们为了严格化开始使用Coq试图给出形成化证明，特别地试图给出Feit-Thompson定理（奇数阶有限群都是可解群）的形式化证明。目前完整的形式化还未完成。

从事代数几何研究的菲尔兹奖得主Vladimir Voevodsky（三年前的9月去世），后来兴趣转向机器辅助证明，因为他1989年的一篇文章在1998年被Simpson发现有错误，他很惊讶觉得Simpson的文章才是错的并给出了解释，然而到了2013年，他才发现自己的文章原来真的是错的！

另外，他得菲尔兹奖的主要工作之一是严格定义了motivic cohomology，有很多篇文章，其中一篇1993年的文章，他1999年自己发现了错误，然而在这之前竟然没一个人指出（见参考文献[6]）：

"This story got me scared. Starting from 1993, multiple groups of mathematicians studied my paper at seminars and used it in their work and none of them noticed the mistake. And it clearly was not an accident. A technical argument by a trusted author, which is hard to check and looks similar to arguments known to be correct, is hardly ever checked in detail."

他于是转向机器验证的形式化证明，发明了HoTT（见参考文献[7]）：

"Who would ensure that I did not forget something and did not make a mistake, if even the mistakes in much more simple arguments take years to uncover?"

从事数论研究的Thomas Hales，后来兴趣转向机器辅助证明，他用机器辅助证明了开普勒猜想，他建立了Formal Abstracts这个项目。我们都相信开普勒猜想是对的，但严格的证明必须要借助计算机。

从事数论研究的Kevin Buzzard，后来兴趣转向机器辅助证明，他建立了著名的Xena project，主要在推广使用Lean这门语言。

还有更多很久才被发现错误的数学证明，下次再聊。

(待补充)

五. 问题与现实，避免过度美好的想象

当然，也有很多人不看好机器证明，这不是没有道理的。

就先扔出三个问题：

1. 假如计算机给出的证明有5000万页，语言非常奇怪，我一个人一辈子也看不完怎么办？

这是一个通俗笑话的改编：

假如一个外星人来到地球，给出了XX定理的证明，但是有5000万页，人们对此毫无了解得从零开始看，结果发现一辈子也看不完。是不是人类没有一个沾到XX定理的边？

2. 我知道有Coq这样的程序能检验计算机证明是否正确，但我就是接受不了怎么办？

这也是一个常见的问题，这方面有很多争论。

3. 数学只要观念对了，证明什么的就随便写写，都不重要，我们相信它是对的，那就是对的，错的，那就是错的。你难道不知道Weyl大大曾经说过" My work always tried to unite the truth with the beautiful, but when I had to choose one or the other, I usually chose the beautiful"？你难道不知道Gromov的论文是多么高瞻远瞩？

这属于转移问题，拒绝回答"一个证明如果是错的，结论也是错的，那么我们应不应该相信或者使用它"这个本质性的问题，同时否定了计算机潜在的未来可能性。

试图用美来解释一切，这也是一种常见的思潮。

(待补充)

六. 我们可以做什么？

(待补充)

参考文献：

[1] 2018年国际数学家大会的一个讨论环节

Machine-Assisted Proofs (ICM 2018 Panel)

https:// arxiv.org/abs/1809.0806 2

[2] Kevin Buzzard的数学主页

https://www. imperial.ac.uk/people/k .buzzard

[3] 一篇最近的批判性博文

The inevitable questions about automated theorem proving

https://mathematicswithoutapologies.wordpress.com/2020/09/01/the-inevitable-questions-about-automated-theorem-proving/

[4] 机器辅助证明的wiki介绍

https:// en.wikipedia.org/wiki/C omputer-assisted_proof

[5] When will computers prove theorems?

http://wwwf.imperial.ac.uk/~buzzard/xena/computers.pdf

[6] The Origins and Motivations of Univalent Foundations

A Personal Mission to Develop Computer Proof Verification to Avoid Mathematical Mistakes

https://www.ias.edu/ideas/2014/voevodsky-origins

[7] Vladimir Voevodsky 1966–2017

https://www. ias.edu/news/2017/vladi mir-voevodsky-obituary

在哲学层面讨论AI能不能在智慧上干过人是一个人人似乎都感兴趣，但目前谁也没法知道正确答案的事。

目前AI的优势(实际也是计算机作为单纯工具的优势)是两个：

1. 广度，没有人能把所有棋谱都过一遍。更不要说有效学习。但只要算力跟上，整个知识库都可过一遍。
2. 效率，庞大计算处理，AI理论上没有上限。

目前和可以预见的未来，AI在某个行业的特定领域干过人类是肯定的。

但整个行业的人一钱不值则是小概率事件。

就以围棋领域为例，人类亲自下场确定不行了，但你弄个阿尔法狗，他弄个贝塔猫斗一斗还是可以的。

人类斗不过狗，但人培养狗斗狗还是可以的。

当然，稍远或遥远的未来如何还是未知。