专访陶哲轩：大概只有0.1%的数学家可以用编程语言写证明

采访记录

（中文版）

Records of Interviews

（In Chinese)

陶哲轩：

      有一个问题我和四名合作者花了两三年才解决，跟一个叫做临界非线性薛定谔方程的偏微分方程有关。前人做的工作假设了初始值满足球对称，我们想要放宽这个条件。做了几个月之后，我们以为自己解决了它，几乎要开香槟。但是在把论文正式写出来的过程中间，我们发现我们遗忘了公式里的关键一项，而只对另外十一项做了估计，以至于整个证明都不成立了。但这个时候，我们已经努力了几个月了，心理上很难放弃。因此，我们接着尝试一个又一个的方法，直到我们两年后终于真正解决了这个问题。我对此很骄傲。而如果我们没有前面这几个月的尝试，我们可能早就放弃了。有时候曾经的错误是有益的，因为它可以给你决心。

陶哲轩：

     一般来说，是那些跨学科，也就是需要不同学科的灵感的东西。可能是有关数学的其他分支，也可能是有关物理、计算机等其他学科。特别地，现在越来越多的数学问题都在用电脑帮忙研究，包括我现在正在做的一个数论研究。我们会先用电脑生成一些真且可证明的命题，尽管电脑给出的证明非常冗长，但我们可以简化这些证明。实际上，当你知道要证明什么，事情就变得简单了许多。我们可以用电脑判断在证明过程中我们所想到的命题是否正确，然后写出人类能理解的证明。人工智能正被寄予帮助证明数学命题的厚望，而今天它越来越成功。如果你用某种特别的语言书写证明……

陶哲轩：

      对，LEAN是其中一个，也是我用的那个。它就像C或Python那样，是一种编程语言。主要的区别在于，一般的编程语言让你进行某些操作，比如打印字符串或者打开文件；LEAN则生成“证明凭证”。

陶哲轩：

      就是证明的形式化。比如你首先有一些公理，然后你有一个“A蕴含B”的证明凭证和一个“B蕴含C”的证明凭证，LEAN允许你将这两者合并，产生“A蕴含C”的证明凭证。最终，对于任何可以由公理证明的命题，你都可以写一段代码，生成它的证明凭证。但即便你只是想证明从1加到n的高斯求和公式……

陶哲轩：

     是的，这非常非常繁琐。像LEAN这样的定理证明器已经出现很久了，但之前要想用它写出任何有意思的证明，需要几年的时间。现在只需要几星期就好。变化在于，人们已经搭建好这些包含基础定理的数学图书馆，基本上涵盖了你在本科数学教育中能见到的任何东西，比如微积分基本定理、Stoke公式等等。你不会想要从公理开始证明一些东西，这很繁琐，从本科数学教材开始会好一些。当然，我们真正想要的，是囊括研究程度的数学结论，因为研究论文都基于它们。

陶哲轩：

      我见过一些把LEAN的证明凭证反过来变成人类的证明的尝试。到目前为止，我们还不能对一般的证明这样做，但对于一些特定的领域和特定的概念，比如点集拓扑和开集、闭集等少量概念，这样的翻译是有的。

     你们可能知道，在刚过去的国际数学奥林匹克（IMO）中，谷歌的DeepMind用它们的AlphaProof成功解决了三道问题。（注：AlphaGeometry另外解决了一道几何题。）如果你仔细看它给出的证明，你会发现一些很奇怪的地方，比如它用归纳法证明了一个命题对于n等于12时成立，但实际上这根本没有必要。所以说，这样的翻译不是显然的，你可以尝试自动这么做，但它不会像人类的证明，而更像一个奇怪的机器证明。

陶哲轩：

      这肯定是其中的一点。我可以说的是，大概只有0.1%的数学家可以用这些语言写证明。我们有很多人可以使用Python和Java等其他语言写程序，但是没多少人真正花时间去学习这样的证明语言，因为它不能够直接帮助你做研究。

      我们确实需要更好的翻译，这是理想中人工智能可以帮忙的地方。如果我们有这样的人工智能，那么大部分人并不需要真正懂得形式化证明的语言。这应该是几年内可以解决的问题。

陶哲轩：

      这是一个不错的想法。现在我们也有一些的数学资料库，最大的当数整数数列线上大全（OEIS），它包含了几十万的整数数列。你可以拿两个数列组成一个新的。这其实是一个非常有用的资料库。当你研究一列数学对象的时候，会好奇有没有人已经考虑或者发现过这样的数列。对于一列有限群，你可以考虑群的成员个数；对于一列图，你可以考虑图的顶点或边的个数。你可以在这个资料库中检索你发现的数列，时不时你会找到完全一致的结果，点进去你会看到说，这个数列在某某文章里面被研究过，或者可以由另外的某个公式给出。有些人甚至专门研究OEIS，看看上面的数列之间有没有相关之处。

     如果像LEAN这样的形式化语言更加普及，或许我们会有更多像Wikipedia或Linux这样的开源社群项目。现在你不能这么做，因为如果没法进行自动的证明验证，而一个人犯了一个错误……希望以后会有更多数学的社群项目。实际上，别的学科现在更多。比如说，业余天文爱好者在发现彗星后可以上传图片到他们的系统上面；业余生物爱好者可以分别数某个地方昆虫或蝴蝶的数目。这样的项目很好，因为人们不需要一个博士学位，也可以为学术做贡献。其实很多形式化证明的项目都不是由数学家参与的，他们可能是程序员，来自科技公司，但他们受过数学训练。他们不一定能完全理解证明一个大定理的全部数学步骤，但当一个大定理被拆分成每个只需要十行就能证明的小引理，这几乎就变成了逻辑游戏。很多人就喜欢逻辑游戏。

陶哲轩：

      很对。AlphaProof之所以能够解决IMO的这些问题，是因为它首先生成了数以十万计的不同数学问题并试图求解，然后留下了“什么样的证明行”、“什么样的证明不行”的大量数据。知道“某种方法大概率会失败”，其实是非常有用的数据。当你阅读数学书的时候，可能99%的内容都是那些成功的证明，就好像我们取某个，然后证明就奏效，像魔法一样。但每个要成为数学家的人都需要自己学习“为什么证明要这么做”，而这不是数学书提供了的。我们需要更多人们做数学证明时的试错过程的数据，一些人已经在对小学生搜集了。现在有一些网上教育平台，学生可以登录自己的账号，然后试着解决一些数学问题。你可以给不同学生不同的提示，比如“不妨把这个问题化为代数”、“不妨试试更简单的例子”等等。你可以设置时间，记录他们解题过程中的一切。人们开始用机器学习来帮助学生学习。或许以后对于高等教育也可以这样。

陶哲轩：

      LEAN有一个很友好的基于Zulip的社群论坛，里面有各种频道，包括如何结合机器学习，如何做教育上的应用等等。我的建议是，你可以先在上面提问。

陶哲轩：

     可能在某种程度上是吧。但事实上，很大一部分的研究论文现在都放在arXiv上面。这恰恰是因为，人们发现如果你只在付费期刊上投稿，人们看不到你的工作，也就不会引用你的文章。所以，把自己的研究结果公开是更合理的，尤其是在快速发展的领域，比如机器学习。投稿一篇文章可能需要几个月，但你在一天之内就可以把它放在arXiv上，然后人们早早就可以引用它。当初arXiv出现的时候，人们很担心自己的研究成果会不会被轻易盗走；但这并没有发生，恰恰因为arXiv给你一个水印，如果别人改了名字放上来，日期在你的后面，显然你才是原创者。

     不过，要用来训练机器，你不需要100%的文章作为数据。如果40%的文章都用得上，已经非常不错了。

陶哲轩：

      到研究生的时候，你不会再有很多的考试，也不用再做很多具体的计算，但你需要控制你计算时的错误率，不然你的研究可能会进展艰难。当我们遇到一个研究问题的时候，我们可能会尝试各种方法，比如考虑简单的情形，或者将一个大而难的问题换成一个简单一点的问题，用这个简单一点的问题来解决一开始的大问题。很多时候，找到存在于中间的这样的命题，就已经是很大的一步了。但为了这么做，你必须要有一种感觉，就是“哪些问题简单一点”、“哪些问题难一点”。比如在数论之中，基本上涉及质数的问题就都是挺困难的。我们有很多像哥德巴赫猜想那样的命题，我们觉得它是对的，但我们就是不知道怎么证明。遇到质数的时候，我们可能会想把这样的数论问题转换成组合问题。研究就好像科学家做实验，你可能会了解一些数据，做一些假设，然后用一些简单的例子去测试它，等等。你在研究阶段也会用到大量的文献，而尽力避免只用自己的知识储备，这跟考试或竞赛是很不一样的。

陶哲轩：

主要是在细节上用到。在本科和研究生阶段，你往往是在学习整体的情况，比如“什么应该是对的”、“什么应该是困难的”等等。但你还是需要去检验一些小的步骤，比如一些不等式的变换，而竞赛的训练在这些地方是挺有用的。

陶哲轩：

      是的。不同人其实适合不同的学习方式。有些人可能喜欢可视化，希望看到图像；有些人可能喜欢形式化，希望看到严谨的细节；有些人喜欢类比，希望将数学问题转化为生活或其他领域中的问题。如果你被教导的方法不适合你，你可能会学得很慢。内在的天赋会给你“可以学多快”的上限，但在现实中，你从来不会碰到这个上限，因为你没有在用最适合你的学习方式。

而实际上，你做一件事越有经验，就越轻松。就好像学习英语。一开始你需要一个一个地学习词汇，后来你变得流利，看一篇长的英文文章就不需要一个词一个词地读，而是可以总览它的内容。当你第一次读一本数学教材，你就好像是一个正在试图编译代码的机器，一旦遇到代码中的“语法错误”，你就会崩溃并报错。过了一段时间之后，即使书里面有一些小错误，你也可以克服它。我可以做这样的比喻，当你第一次观看一种全新类型的电视剧，比如古装剧，你不知道会发生什么，然后不断好奇“他是谁”“为什么这个人需要和这个人结婚”等等。但当你看了很多类似的古装剧，然后看一部新的，你就可以预测故事的走向了。你会发现，数学书其实是一样的。当你习惯了，然后再看一篇深奥的数学论文时，你会想“我知道了，这个引理大概率要用来构造这样一个反例，所以它很重要”。

陶哲轩：

      这其实是个好问题。我总觉得我一直有事情要做。如果你问我的话，我很多的日子都像在玩俄罗斯方块，比如我有一个耗时15分钟的任务，然后我在这件事和这件事之间有15分钟的间隙，于是我把它放在这里。我擅长这么做。当你在很多年以来一直重复做一些事情，比如写邮件，你可以做得非常快。

陶哲轩：

      这么说吧，我知道不要在我10分钟后就要去一个会议的时候做一个问题。但如果我有一个一直想做的问题，然后我突然有2至3小时的空闲，我可以选择去专注做这个问题。有时候，时间紧迫在一定程度上可以让你更加高效。

陶哲轩：

这取决于你的目标是什么。如果你想要成为第一个做某件事的人，或者发表最多的文章等等，那你可能就会像是在竞速。但不同人有不同的工作和生活的平衡。确实有很多数学家都对数学比较痴迷。你当然在一些时候需要专注的能力，但你并不需要永远做数学。

      有些人喜欢同时做很多事情，但我不行，我会分别在每件事情上专注。有些人则习惯专注做一件事情好几天。工作节奏是因人而异的，你需要找到最适合你的状态，否则即使你逼自己以某种你不喜欢的方式工作，你的大脑也会罢工。我试过工作的时候听音乐，我发现我还是喜欢完全宁静的环境，但我有一个数学家朋友，他说他在咖啡或酒吧这样嘈杂的地方反而工作得最好。有些人喜欢散步，有些人则喜欢一动不动。我可能喜欢躺着做数学，在地上放很多的文章。我也喜欢大的黑板，这样我可以做很多的计算，并一次性看到所有内容。