用1000页论文证明一个问题，再用1000页来填补漏洞

　　证明是数学的精髓。任何数学结果都应按照严格的逻辑从第一原理推导得出。证明是将数学与其他智力活动区分开来的东西，也是数学之所以优美并纯粹的原因。

　　最近，帝国理工学院的纯数学教授 Kevin Buzzard 在剑桥举办的一次研讨会上表示，证明是一种很高的标准，它被兢兢业业地应用到了本科的数学课程中，却没有应用到更高层次的数学研究中。

　　有些证明是存在漏洞的，有些证明是有错误的，还有些证明在全世界只有一两个人能理解。即使是发表在学术期刊上的东西，也不一定都正确。想要确切地知道哪些结果是可信赖的，你得成为一个能接近那些达成了共识的专家的圈内人。Buzzard 说：“事情有些失控。”

　　Buzzard 自己就是这样一位专家，从 1998 年以来，他就是一名专业的数学研究人员。在博士期间，他研究与费马大定理的证明有关的一些数学。不过最近几年，对学术界中的数学证明标准的担忧，悄然袭上了他的心头。他说，这种担忧或许部分源于他的数学中年危机，这让他重新审视在自己选择的职业生涯内，事物是如何运作的。

图片来源：medium.com

　　未经检验

　　数学研究中的问题通常不在于有意地欺骗，而是源于一些其他的状况。比如说，一些数学家有时会在自己的工作中引用尚未发表的论文，因为他们非常确信这些未被发表的结果是正确的，并认定它们会很快地通过同行评审然后得以发表在学术期刊上，这种情况并不少见。然而，有时这些未发表的结果确实永远不会出现在期刊上。那么当越来越多的工作建立在这些未经检验的结果之上时，未经检验这一事实就可能被遗忘和掩盖。

　　这样的事情就曾发生在数学家 James Arthur 的一篇著名的专著之上，它依赖于他的四篇还未经发表的论文。人们能意识到了这些证明中可能存在某些漏洞，却又会一致认为它们可能大概率没问题。最近，由于对数学作出的诸多贡献，Authur 被授予了几个重要的奖项，虽然这些奖项实至名归，却也加深了人们认为 Authur 的结果就 100% 正确的印象。

　　另一个问题是错误。每个人都会犯错，而有的时候，这些错误甚至会逃过决定论文是否发表的专家评审的法眼。因为评审们并不总是会逐行检验结果，他们的目标是说服自己，论文中使用的方法足以证明主要的结果。

　　如果在论文发表后发现了明显的错误，没有哪个自重的数学家会拒绝承认自己的错误。但错误的更正或论文的撤回都只是作为一个“更正”或者“编辑说明”出现在下一期的期刊上。有多少人会读到这些呢？专业领域内的同行当然会知道，但其他人并不会。

　　有些证明又长又复杂，只有全世界的少数人能理解，这或许是错误或漏洞最主要的来源。一个著名的例子是所谓的有限单群分类，也就是对无限多个数学对象中的每一个进行分类，这是二十世纪数学领域的一大成就。证明这个分类正确且完备的第一版证明发布于 1983 年，证明长度超过了 10000 页，分布在 500 个期刊论文中，由 100 多个作者完成。结果人们发现，这个证明之中存在一个问题，修正这个问题就又花了 9 年的时间外加一篇超过 1000 页的论文。

　　基于第一版证明的巨大复杂性，论文的主要作者承诺会给出一个“更简单”的第二个版证明，他们计划分 12 卷出版。然而截至 2019 年，只有其中 7 卷问世。最终能够完全理解整个证明的很可能只有极少数人，而那时候他们也已经不再年轻。

图片来源：akifaltundal.net

　　虽然数学家一致认为，有限单群分类确实是完备的，并且认为只要有人愿意在大量的文献中搜寻线索，最终就应该能够拼凑出完整的证明——但是多少人有这样的时间和这样的头脑去这样做呢？

　　怎么办？

　　Buzzard 认为，这类问题已经严重破坏了纯数学，甚至让纯数学陷入危机。但要如何才能化解这场危机？数学是一门创造性的学科，而不是程序性的；而且数学家是人，他们喜欢分组工作，而不希望深陷在细节的泥潭里。因此，要求他们始终坚持预设的程序就是要求他们像机器一样工作。

　　但是 Buzzard 觉得这正是问题的症结所在：我们不需要数学家像机器一样工作，而是可以要他们去使用机器。计算机科学家和数学家是两个相关联的群体，但他们有着本质的区别：计算机科学家修复错误，而数学家则忽略错误。

　　一些计算机科学家经常游走于数学家之间，他们开发出了一些定理证明软件，例如 LEAN 和 Isabelle。这些软件并不能神奇般地为那些困扰了人们数个世纪的难题找到一个证明，这类问题仍需要人类数学家来解决题，但它们可以帮助我们检验数学家的证明是否正确。

　　如果给出一个用代码表达的证明，软件会根据之前的结果和数学公理检验所有的逻辑步骤是否正确。如果出现错误，机器就会发出信号告诉我们；如果之前在证明中留有漏洞，机器也不会放任我们忘记。

图片来源：medium.com

　　Buzzard 说，计算机科学家可能因此会认为，一个结果只有经过了定理证明软件的正式检验之后，才能算是被证明了。这就意味着，对计算机科学家来说，数学领域的许多重大成果，包括费马大定理或有限单群分类，仍然可以被检验得更加仔细。

　　Buzzard 深知，要把数学证明转化成软件可以理解的代码需要付出巨大的努力，以费马大定理为例，它的花费估计需要 1 亿英镑。尽管如此，但 Buzzard 认为，我们至少可以培养初露头角的数学家去接受这种方式。他在帝国理工学院的本科生们就在学习如何使用定理证明软件，他还会鼓励学生将机器证明应用到结果当中。如果数学家养成了这样做的习惯，同时还有其他人开始正式检验那些已有的证明结果，那么数学就可以被带回到正确的轨道上。

　　不过有些人担忧，在数学证明中使用计算机会导致人们丧失对证明的真正理解：如果计算机做了我们的工作，如果它们以一种我们人类较低级的数据处理能力无法跟进的方式来证明，那么我们就不能声称自己理解最终的结果了。

　　但 Buzzard 并不是在提倡使用机器学习中的那种黑箱算法。他是想将证明转换成计算机程序可理解的代码，以便证明过程可以得到非常可靠的检验，而不是要让证明变得无法理解。我们当然无法保证这些程序绝不会出错，但它们的错误比人类少多了。

　　在他看来，这么做不会让数学失去任何东西，只会获得。

　　原文标题为“Pure maths in crisis?”，首发于2019年3月19日的Plus Magazine。原文链接：https://plus.maths.org/content/pure-maths-crisis. 中文内容仅供参考，一切内容以英文原版为准。