证明是数学的精髓。任何数学结果都应按照严格的逻辑从第一原理推导得出。证明是将数学与其他智力活动区分开来的东西，他也是数学之所以优美并纯粹的原因。最近，帝国理工学院的纯数学教授Kevin Buzzard在剑桥举办的一次研讨会上表示，证明是一种很高的标准，它被兢兢业业地应用到了本科的数学课程中，却没有应用到更高层次的数学研究中。
有些证明是存在漏洞的，有些证明是有错误的，还有些证明在全世界只有一两个人能理解。即使是发表在学术期刊上的东西，也不一定都正确。想要确切地知道哪些结果是可信赖的，你得成为一个能接近那些达成了共识的专家的圈内人。Buzzard说：“事情有些失控。”
Buzzard自己就是这样一位专家，从1998年以来，他就是一名专业的数学研究人员。在博士期间，他研究与费马大定理的证明有关的一些数学。不过最近几年，对学术界中的数学证明标准的担忧，悄然袭上了他的心头。他说，这种担忧或许部分源于他的数学中年危机，这让他重新审视在自己选择的职业生涯内，事物是如何运作的。
数学研究中的问题通常不在于有意地欺骗，而是源于一些其他的状况。比如说，一些数学家有时会在自己的工作中引用尚未发表的论文，因为他们非常确信这些未被发表的结果是正确的，并认定它们会很快地通过同行评审然后得以发表在学术期刊上，这种情况并不少见。然而，有时这些未发表的结果确实永远不会出现在期刊上。那么当越来越多的工作建立在这些未经检验的结果之上时，未经检验这一事实就可能被遗忘和掩盖。
Buzzard认为，这类问题已经严重破坏了纯数学，甚至让纯数学陷入危机。但要如何才能化解这场危机？数学是一门创造性的学科，而不是程序性的；而且数学家是人，他们喜欢分组工作，而不希望深陷在细节的泥潭里。因此，要求他们始终坚持预设的程序就是要求他们像机器一样工作。但是Buzzard认为，这正是问题的症结所在：我们不需要数学家像机器一样工作，而是可以要他们去使用机器。
计算机科学家和数学家是两个相关联的群体，但他们有着本质的区别：计算机科学家修复错误，而数学家则忽略错误。一些计算机科学家经常游走于数学家之间，他们开发出了一些定理证明软件，例如LEAN和Isabelle。这些软件并不能神奇般地为那些困扰了人们数个世纪的难题找到一个证明，这类问题仍需要人类数学家来解决题，但它们可以帮助我们检验数学家的证明是否正确。
Buzzard深知，要把数学证明转化成软件可以理解的代码需要付出巨大的努力，以费马大定理为例，它的花费估计需要1亿英镑。尽管如此，但Buzzard认为，我们至少可以培养初露头角的数学家去接受这种方式。他在帝国理工学院的本科生们就在学习如何使用定理证明软件，他还会鼓励学生将机器证明应用到结果当中。
如果数学家养成了这样做的习惯，同时还有其他人开始正式检验那些已有的证明结果，那么数学就可以被带回到正确的轨道上。