阿蒂亚（Michael Atiyah）曾说过：“我们的理想是探究数学真谛，而不是利用机械执行指令的计算机推演论证。”另一位菲尔兹奖获得者泽尔曼诺夫（Zelmanov）也表示赞同：“只有所有数学家都认可的证明方法才是真正有效的，所以我对机器证明方法的前景并不看好。”他说的有道理吗？如果数学证明方法只有生成它的机器能够理解，我们真的可以相信吗？
我们的写作工具参与了我们思想的形成过程。
——弗里德里希·尼采（Friedrich Nietzsche）
撰文｜Marcus du Sautoy（牛津大学数学教授）
翻译｜王晓燕、陈浩、程国建
尽管我有点担心计算机会让我丢掉工作，但我不得不承认，作为一种工具，它是一个“无价之宝”。当我们需要将一系列方程合并成一个方程时，手工计算是很难保证不出错的。但对于计算机来说，它就很擅长处理这种重复而机械且计算量庞大的任务。你只需要定义一套规则，剩下的就由计算机接手了。而且，在速度与准确性等方面，计算机是远超过手工计算的。正因为如此，近年来计算机的作用越来越重要，其应用领域也越来越广泛。
数学与计算机程序的算法紧密相关。因此，近半个世纪计算机常用于证明一些复杂的数学问题。20世纪70年代，计算机对“四色定理”的证明轰动了全世界。四色定理指的是“任何一张地图只用四种颜色就能使具有共同边界的国家着上不同的颜色。”也就是说，在不引起混淆的情况下，一张地图至少需要四种颜色来标记。
尽管此前很多人认为五种颜色就是下限，但计算机的发明大大加快了对四色定理证明的进程。1976年，数学家凯尼斯·阿佩尔 （Kenneth Appel） 和沃尔夫冈·哈肯 （Wolfgang Haken） 在前人的基础上用计算机证明了四色定理。阿佩尔与哈肯把地图的无限种可能情况简化为1936种构型，但是要靠人工逐一验证如此之多的构型是不现实的，所以才需要借助计算机进行验证。计算机根据程序指令逐一浏览地图并检查其是否满足四色定理。当时的计算机运算速度还不够高，整个证明过程的耗时超过了1000小时。
能相信计算机吗？
计算机只能执行指令，并无自主创造力。但是，想要证实程序中是否存在错误是很困难的。我们能在多大程度上相信计算机，这个问题一直困扰着人工智能领域的学者。当我们进入由算法主导的未来时，确保代码中没有未被检测出的错误，将成为一项艰巨的挑战。
2006年匹兹堡大学的托马斯·黑尔斯 （Thomas Hales） 教授在《数学年鉴》上发表了关于借助计算机证明著名的数学问题—“开普勒猜想”的论文。简单来说，开普勒猜想就是对在空间中如何最密集地堆积圆球的解答。出于有效利用空间以及避免压坏水果的考虑，水果店店主一般会将水果层层交替堆叠，任意平面上的每个水果都与六个水果相邻，构成正六边形。像阿佩尔与哈肯一样，黑尔斯采用的也是借助计算机对足够多的案例进行穷举证明的方法。事实上，早在1998年，黑尔斯就曾宣布他的证明完成，并向《数学年鉴》评审组提交了论文、程序代码及相关资料，但该项证明的审核验证经历了漫长的时间。这是因为人类大脑的物理局限性，审核人必须得充分相信计算机的能力，就好比我们第一次乘坐飞机一样，心中难免惴惴不安。用了8年时间，数学家们证明了黑尔斯是正确的，但其确定性是99%。
对于数学纯化论者来说，这1%也是不可容忍的。这就好比，要证明你是牛顿的亲戚，可是家族谱系图里却缺少了关键的一环…… 人们质疑计算机证明数学问题的能力，并不是因为害怕计算机在未来会使得他们丢掉工作（早些年计算机只会按人类的指令执行操作，并不具备自主学习能力），主要是因为无法确定计算机程序是否存在潜在缺陷 。我们该如何去相信计算机的证明呢？
数学家们就曾被程序代码中的缺陷困扰。1992年，牛津物理学家利用弦理论中的启发法对高维几何空间中可识别的代数结构数量进行了预测。对于该预测，数学家们持怀疑态度，因为他们觉得物理学不具备解释抽象结构的能力。当有证据表明这个猜想是错误的时候，他们觉得自己的怀疑是有道理的。然而，后来事实证明，否定这个预测的错误证据正是由一个有缺陷的计算机程序生成的。所以，错的是数学家，而不是物理学家——程序的错误把他们引入了歧途。几年之后，数学家们开始努力地证明物理学家的预测是对的 （这一次数学家们把计算机排除在外了） 。
这样的故事加剧了数学家们的担忧，他们担心计算机可能会让我们在结构不健全的“程序地基”之上建造精巧的“数学大厦”。但坦白讲，许多问题的证明往往都存在不足或错误，人类犯错的可能性通常比计算机更大。包括我本人发表的一些证明，后来也被发现存在一些漏洞。错误可以被修正，但遗憾的是，在证明的验证和审核阶段它们并没有被找出来。
证明的验证和审核非常重要，它是发现缺陷和漏洞的重要环节。这就是为什么数学界“千禧年大奖问题”的证明要经过两年的审核验证期—大家认为24个月的时间足够让错误暴露出来。以安德鲁·怀尔斯证明“费马大定理”为例，在其证明方法付梓之前，审验人员发现了一个小缺陷。但怀尔斯和理查德·泰勒 （Richard Taylor，曾是怀尔斯的学生） 奇迹般地修正了这一缺陷。即便如此，在错误证明的基础上构建数学体系的情况也是屡见不鲜的。
许多新的证明极其复杂，以至于数学家们很担心一些潜在的错误难以被发现。以有限单群分类定理 （classification of finite simple groups） 为例，单群在有限群论中的地位，与素数在数论中的地位、原子在化学中的地位一样，它们都是构建各自所在世界的“砖块”。对于任意的有限群，我们可以将其分解为一系列单群，且分解方法是唯一的。通过研究这些“砖块”，我们可以进一步发现由它们所组成的物质的结构和性质。与当年化学家寻找新元素一样，数学家也开始了对于单群的寻找—列出一个单群的“元素周期表”，并证明这个“周期表”中包含了所有的单群。其中，“魔群”是最大的“散在单群”。“魔群定理”的证明散落在100多篇论文中，合计超过10000页，涉及数百名数学家。单群的“元素周期表”中含有26个散在单群，对于是否存在第27个散在单群，人们总是持怀疑态度。对于这种类型的复杂证明，进行人力审核几乎是不可能的，那么，是否可以通过计算机程序来检验数学定理的证明呢？
新的问题又出现了，用计算机程序去检验计算机证明的步骤，是否可信？怎么确保计算机程序中没有缺陷？再用另一台计算机去查证吗？这会陷入一个永无休止的死循环。你怎么能确定你的方法正在引导你走向真正的知识的“圣杯”？真理的产生取决于你的证明方法。
正如哲学家大卫·休谟 （David Hume） 指出的，大多数科学研究都建立在归纳法之上——通过观察特定的例子来推断出一个普遍的规律或原则。为什么归纳法是一种产生科学真理的好方法呢？这主要是因为在归纳法里我们可以举出许多例子来说明。基于归纳法，曾产生了许多著名的科学理论，这反过来证实了归纳法确实是一种科学研究的好方法。
Coq证明助手
在过去，数学问题的证明和验证过程全凭人工完成。而现在，越来越多的证明开始借力于计算机，但因为验证的过程既烦冗又复杂，并且工作量巨大，人类大脑的局限性决定了无法采用人工验证的方式判断其对错。因此，我们迫切需要一种解决方案，即通过构建新的程序来验证计算机证明的正确性。
20世纪80年代末，法国数学家皮埃尔·于埃 （Pierre Huet） 和蒂埃里·科昆德 （Thierry Coquand） 开始从事结构微积分 （calculus of constructions） 项目。该项目简称CoC，但很快又被称为Coq （法语里意为“公鸡”） 。这个改动一方面是为方便记忆，因为在法国一直有以动物命名开发工具的习惯；另一方面是因为Coq是其开发者之一科昆德姓氏的前三个字母。Coq为验证数学证明而生，很快也成了验证计算机证明的重要程序，备受青睐。
2000年，微软研究院首席研究员乔治·贡蒂尔 （Georges Gonthier） 及其同事使用Coq对阿佩尔与哈肯的四色定理的计算机证明进行了验证，因为这是史上第一个需要计算机才能完成的证明 （假定Coq不存在任何缺陷） 。然后，他们也使用Coq去验证了阿佩尔和哈肯自己所写的证明部分。
人类手工证明与计算机证明不同，手工证明过程中会跳过一些烦琐或众人皆知的步骤，而计算机却依赖于明确、细化的步骤才能正确执行指令。这类似于写小说和写保姆指导手册的区别。前者不需要对主人公的每一个动作都解释得一清二楚，而后者则需要尽可能地明确和详尽，包括一天中婴儿的食谱，以及吃饭、睡觉、上厕所的每一个细节。
计算机用了5年的时间进一步自动识别并验证人类证明的过程。这期间，人们惊讶地发现了在第一次证明中被忽略的数学知识。
Coq与原始的计算机证明相比，更应该信任谁呢？当然是前者。越来越多的计算机证明被Coq所验证，使我们更加确信Coq是可靠的。这就像我们通过归纳法验证数学中的基本公理一样。这就像任取两个数A和B，如果A+B都等于B+A，那么A+B=B+A就是正确的。用一个计算机程序来验证多个计算机证明，比编制一个特定的证明程序或者进行人工证明更值得我们信任。
贡蒂尔团队验证完四色定理后，紧接着开始了对奇阶定理 （odd order theorem） 的验证工作。奇阶定理是对称性研究最重要的指导定理之一，通常被认为是有限单群分类的基石。像化学里的元素周期表一样，有限单群是构成数学有限群论“元素周期表”中的基本元素，所有的对象都由有限单群构成。具有素数边的正多边形 （如正三角形、正五边形） 是该周期表中的元素。此外，该周期表中还有一些复杂且独特的对称元素，如旋转了60次的正二十面体、需要196883维线性空间才能表达的“魔群”等。“魔群”具有的元素个数超过了构成地球的原子个数。
该定理指出，任何奇阶对称结构的基本组成单元都是素数多边形，此外再无其他结构。如果把对称物体分为奇阶和偶阶两种，那么该定理就等于涵盖了其中的一半，意义重大。
奇阶定理的原始论文有255页，占据了《太平洋数学期刊》的全部篇幅。在它出版之前，大多数证明最多只有几页，一天内即可掌握。这个冗长复杂的证明，对每一位数学家来说都是一个挑战。因此，其中是否存在细微的缺陷或错误，始终无法考证。
Coq对复杂数学定理的证明过程，一方面可以检验Coq的能力，另一方面能帮我们树立足够的信心。但将人工证明转换成可验证的计算机代码这一过程并不容易。
贡蒂尔略带腼腆地回忆道：
第一次开会讨论时，我向团队里其他成员宣布了我的宏伟计划，他们流露出不可思议的表情，就像是我得了妄想症。奇阶定理的证明过程太过复杂，验证它最初被认为是不可能的。做这个项目的真正原因，是为了充分理解数学理论的构建过程并使之与Coq充分融合。
会议结束后，团队里的一名程序员查看了原始证明，随后向贡蒂尔发来一封邮件：“17万行代码，1.5万个变量，4300个函数。好玩，太棒了！”微软剑桥研究院团队用了6年的时间完成了证明。当项目即将结束时，贡蒂尔兴奋地说，经过无数个不眠之夜，他终于可以放松一下了。
贡蒂尔说：“数学是最伟大的浪漫主义学科之一，即便是天才，也得掌握所有知识才能激发灵感，理解一切。”但是，人类的大脑存在物理上的局限性。他希望他们所做的一切能够叩开人类与机器彼此信任、持续合作的新时代“大门”。
人脑的极限
年轻的数学家们开始意识到，数学研究变得更为艰难了：学科分支越发密集，问题越发复杂。攻读博士学位的3年时间，只够去理解导师所给题目的含义。随后，再花费数年时间去研究、探索，运气不错的话，会得到一些研究成果。然而，你发表的论文却面临着没人能审核它。
审核别人发表的论文是得不到太多报酬的，但期刊论文的审核必须经过同行的评审。职称评定也以公开发表在《数学年鉴》或《l扞HES数学期刊》这类文献中的论文积分为基准。因此，有一个像Coq证明助手这样的系统就非常重要了。
一些数学家认为我们目前正处在一个新旧时代的交替期——数学的发展虽然受到人类大脑局限性的制约，但借助于计算机，我们对数学的探索已远远超出了人脑的思维范畴。
伟大的数学家们能够用他们睿智的头脑，借助于纸和笔这些极其简单的工具，构造出像“魔群”这样具有196883维的对称体，这是人类的奇迹。但数学家们终将会老去，就像中世纪的泥瓦匠，其精湛的技艺将伴随身体的死亡而从人世间消失。如果很难找到通往“新奇迹”的方向，人们终将失去创造的原动力。
费马大定理的证明长达数百页，跨越3个世纪，这说明人类拥有足够的耐心。当你努力去证明一个极其复杂的猜想时，隐约会有一种突破人类大脑物理极限的感觉。数学是无限的，而人的能力是有限的。但即便如此，我们常会为自己所做的努力感到吃惊，因为我们用数学的方式证明了“数学海洋的广阔无边”。
有一个问题几乎困扰了我15年之久。每次推演时，总是在即将得到解决方案的关键时刻，我的大脑容量就不够用了，它给我“即将宕机！”的警告。距离成功仅一步之遥，却难以取得突破。就像现象与本质之间隔着一张“渔网”，它制约着我们，让我们难以冲出迷雾，得到光明。当几代数学家致力于黎曼假设的证明而不得其解时，人们开始怀疑，是否这样的证明已超越人脑的极限。
著名数学家哈代多年来一直试图证明黎曼假设，后来他自嘲道：“每个傻瓜都能提出有关质数的问题，而最聪明的人却无法解答。”奥地利数学家、逻辑学家库尔特·哥德尔 （Kurt Gdel） 有过论证：数学中包含了许多没有经过证明的真理。能否用新的公理去证明那些未被证明的真理呢？哥德尔早在1951年就发出了警示，他认为我们可能会越来越难以掌控现代数学的发展方向：
人们创造出了一套庞杂且仍在扩展的公理系统，但人们研究它的目的越来越说不清楚……的确，在现代数学中，这些更高层次的理论成果实际上无法投入使用，这有可能与它们无法证明某些基本定理有关，例如黎曼假设。
鉴于我们可能即将触及人类自身能力的极限，一些数学家已意识到，如果希望人类文明持续进步，我们将需要