纯数学陷入了危机？

证明

是数学的精髓

在数学上，证明是指在一个特定的公理系统中，根据一定的规则或标准，由公理和定理推导出某些命题的过程。

任何数学结果都应按照严格的逻辑从第一原理推导得出。

证明也可谓是数学的精髓，是将数学与其他智力活动区分开来的东西。

但近日，帝国理工学院的纯数学教授Kevin Buzzard在剑桥举办的一次研讨会上表示：

证明是一种很高的标准。它被兢兢业业地应用到了本科的数学课程中，却没有应用到更高层次的数学研究中。

（他的被观点整理在plus.maths上）

    Buzzard说：“事情有些失控。”    

作为一名专业的数学研究人员，Buzzard在博士期间就研究与费马大定理的证明有关的一些数学。

不过最近几年，他开始对学术界中的数学证明标准的担忧。

Kevin Buzzard

他认为有些证明是存在漏洞的，有些证明是有错误的，还有些证明在全世界只有一两个人能理解。即使是发表在学术期刊上的东西，也不一定都正确。

想要确切地知道哪些结果是可信赖的，你得成为一个能接近那些达成了共识的专家的圈内人。

他表示，这种担忧或许部分源于他的数学中年危机，这让他重新审视在自己选择的职业生涯内，事物是如何运作的。

    问题是什么    

Buzzard认为数学研究中的问题通常不在于有意地欺骗，而是源于一些其他的状况。

比如说，一些数学家有时会在自己的工作中引用尚未发表的论文，因为他们非常确信这些未被发表的结果是正确的，并认定它们会很快地通过同行评审然后得以发表在学术期刊上，这种情况并不少见。

然而，有时这些未发表的结果确实永远不会出现在期刊上。

那么当越来越多的工作建立在这些未经检验的结果之上时，未经检验这一事实就可能被遗忘和掩盖。

这样的事情就曾发生在数学家James Arthur的一篇著名的专著之上，这本专著是根据他的四篇未发表的论文写成。

虽然人们能意识到了这些证明中可能存在某些漏洞，但他们仍然一致认为它们可能大概率没问题。

加上Authur对数学作出的诸多贡献，还被授予了几个重要的奖项，这更加深了人们认为Authur的结果就100%正确的印象。

除此之外，还有一个问题，那就是犯错。

每个人都会犯错，而有的时候，这些错误甚至会逃过决定论文是否发表的专家评审的法眼。

因为评审们并不总是会逐行检验结果，他们的目标是说服自己，论文中使用的方法足以证明主要的结果。

即使发表后发现明显的错误，数学家都会承认错误。但错误的更正或论文的撤回都只是作为一个“更正”或者“编辑说明”出现在下一期的期刊上。

有多少人会读到这些呢？专业领域内的同行当然会知道，但其他人并不会。

有些证明又长又复杂，只有全世界的少数人能理解，这或许是错误或漏洞最主要的来源。

一个著名的例子是所谓的有限单群分类（classification of finite simple groups），这也是二十世纪数学领域的一大成就。

1983年，证明这个分类正确且完备的第一版证明被发布，证明长度超过了10000页，分布在500个期刊论文中，由100多个作者完成。

结果人们发现，这个证明之中存在一个问题，修正这个问题就又花了9年的时间外加一篇超过1000页的论文。

基于第一版证明的巨大复杂性，论文的主要作者承诺会给出一个“更简单”的第二个版证明，他们计划分12卷出版。

然而截至2019年，只有其中7卷已问世。最终能够完全理解整个证明的很可能只有极少数人，而那时候他们也已经不再年轻。

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

Buzzard认为，这类问题严重破坏了纯数学，以至于它陷入了危机。

   如何化解这场危机呢？    

作为一门创造性的学科，而不是程序性的学科，数学家也是人。他们喜欢分组工作，不喜欢被细节所困扰。

因此要求他们始终坚持正当程序就是要求他们像机器一样工作。

但Buzzard认为，这正是解决方案所在：我们不需要让数学家像机器一样工作，而可以让他们使用机器。

计算机科学家和数学家是两个相关联的群体，但他们有着本质的区别：计算机科学家修复错误，而数学家则忽略错误。

一些计算机科学家经常游走于数学家之间，他们开发出了一些定理证明软件，例如LEAN和Isabelle。

这虽然些软件并不能神奇般地为那些困扰了人们数个世纪的难题找到一个证明，这类问题仍需要人类数学家来解决题，但它们可以帮助我们检验数学家的证明是否正确。

当给出一个用代码表达的证明，软件会根据之前的结果和数学公理检验所有的逻辑步骤是否正确。

如果出现错误，机器就会发出信号告诉我们；如果之前在证明中留有漏洞，机器也不会放任我们忘记。

Buzzard说，计算机科学家可能会认为，一个结果只有经过定理证明软件的正式检验才能被证明。

这意味着，对计算机科学家来说，数学领域的许多重大成果，包括费马最后定理或有限简单群的分类，仍然可以得到更仔细的检验。

Buzzard深知，要把数学证明转化成软件可以理解的代码需要付出巨大的努力，以费马大定理为例，它的花费估计需要1亿英镑。

尽管如此，Buzzard认为，我们至少可以培养初露头角的数学家去接受这种方式。

他在帝国理工学院的本科生们就在学习如何使用定理证明软件，他还会鼓励学生将机器证明应用到结果当中。

如果数学家养成了这样做的习惯，同时还有其他人开始正式检验那些已有的证明结果，那么数学就可以被带回到正确的轨道上。

不过也有人担心，在数学中使用计算机是否会导致人们丢失对证明的真正理解。

假设计算机为我们做了工作，而且它们以一种我们人类较低级的数据处理能力，且我们无法跟进的方式来证明，那么我们就不能声称自己理解最终的结果了。

其实Buzzard并不是在提倡使用机器学习中的那种黑箱算法。

他是想将证明转换成计算机程序可理解的代码，以便证明过程可以得到非常可靠的检验，而不是要让证明变得无法理解。

虽然我们当然无法保证这些程序绝不会出错，但它们的错误比人类少多了。