对数学证明的审查及数学可谬性范文

摘要:皮尔士、拉卡托斯和欧里斯特对于数学可谬性的论断是从宏观的角度进行的。数学证明的可审查性可以最大限度地保证其正确性，但机器证明和长证明使得审查难以进行，它们的存在也为数学可谬性提供了微观证据。

关键词:数学证明;可审查性;数学可谬性

一方面，就今天的数学哲学领域来说，数学可谬性已经成为共识，尽管很多数学家们对此并不在意。另一方面，数学科学在当代的发展出现了一些新的情况如信息技术在数学研究中扮演重要角色、数学与现实的联系更加密切以及数学家之间合作研究程度的增加等。其中，难以审查数学证明的出现尤为引人注目。我们认为，难以审查数学证明的出现实际上为数学可谬性提供了进一步的证据。

一数学可谬性

长期以来数学都被赋予成一种可靠、准确和客观知识的典范。一般人皆视数学为真理，数学家们对此往往更是引以为傲。数学家克兰茨(Krantz，S)的话是具有代表性的，他说，数学“具有一种确定性，这是其他科学所不具备的。我们赋予这个系统以可靠性、再现性以及可移植性，这是任何其他科学所做不到的”。克莱因(Kline，M)在描述传统的数学真理观也说过:“无论什么时候，当一个人需要一个确定性和推理正确性的例子时，他一定会求助于数学”。［1］数学哲学家们对于数学知识是否具有真理性的问题很早以前就有过认真的思考。以美国数学家和数学哲学家皮尔士(CharlesSandersPeirce，1839—1914)、匈牙利数学哲学家拉卡托斯(ImreLakatos，1922—1974)和英国数学哲学家欧里斯特(PaulEr-nest，1944—)为代表的数学哲学家相继地提出了数学具有可谬性的看法。简单地说，皮尔士认为数学可谬性的根据主要是通过将数学家的数学创造与科学家对于经验科学的探究过程进行对比得出的。皮尔士指出，数学家在数学创造过程中需要将数学命题转换成头脑中的图形，思维的过程就是对图形的操作，该过程与科学家的实验是很相似的。由于经验科学的探究是可谬的，因而数学也将是可谬的。拉卡托斯区分了两类系统即欧几里得系统和拟经验系统，逻辑主义、直觉主义和形式主义三大学派的基础研究本质上都是要将全部数学重建为欧几里得系统，而它们的失败说明了数学必然是拟经验的，数学的拟经验性又说明了数学的可谬性。［2］欧里斯特的数学可谬观最先来自于拉卡托斯的数学可谬思想，并在后者的基础上进行了进一步的分析。他将数学上的认识论观点分成绝对主义数学观和可谬主义数学观，而三大学派都持有绝对主义数学观。欧里斯特通过分析指出，三大学派的绝对主义数学观都是错误的，因此，数学就应该是可谬的。［3］可以看出，欧里斯特数学可谬观的得出与拉卡托斯在本质上是类似的，都是通过对于绝对主义数学观的否定而实现的，而皮尔士的数学可谬观则是通过对于数学创造与经验科学的探究之间的相似性而得出。尽管二者是从不同的途径得出数学可谬性这个相同的结论，但二者之间也有其共同点，那就是它们都是从宏观上说明数学是可谬的。根据皮尔士观点，既然数学创造与自然科学的探究相似，那么数学本身就一定也像自然科学一样是可谬的;而根据拉卡特斯与欧里斯特的观点，可谬性本来就是数学自身的特点。那么，除此之外，是否还有其他的证据表明数学的可谬性呢?特别是，现代数学发展有没有为数学可谬性提供更加微观的证据呢?

二数学证明可审查的必要性

数学证明被认为是数学与自然科学之间的核心区别所在，它在数学发展中扮演着极为重要的作用。通过数学证明，一个对错不定的数学猜想或者变成了一个数学真命题或数学定理，或者被认定为假命题而抛弃。就数学共同体来说，数学证明发挥着让数学家们确信某个命题是正确无误的作用，从而可以让他们在自己的数学研究中放心地加以运用。就数学科学来说，数学证明是数学发展的必要途径，通过数学证明得到一个个数学真命题，而数学真命题是一个数学分支的主要构成。显然，数学证明要想发挥应有作用，正确性是最基本的要求。泰马祖科(ThomasTymoczko)认为，在传统的数学观念中，数学证明具有三个基本的特点即有说服力、可审查性以及形式化［4］。有说服力就是上文所说的让共同体中其他数学家对该证明的正确性充分的确信，可审查是指其他的数学家能够对数学证明进行检查以确定其是否正确，形式化是指数学证明应该用形式化的数学语言书写而成。其实，这三点之间是有联系的，形式化是证明的外在形式，可审查性保证了证明的正确性，而有说服力则是可审查性的结果。形式化是可审查性的必要条件，数学内容用形式化的数学语言进行表述是现代数学的表现形式，数学共同体中的成员要对数学证明进行审查，当然需要该证明是用形式化的数学语言书写的，否则数学家可能根本就看不懂，从而就不存在审查了，从这个角度看，形式化其实是附着于可审查性的。因此，传统数学证明的三个特点的核心应该是可审查性。关于可审查性，除了要求证明要用数学共同体共同认可的数学语言进行形式化书写外，还有两点是需要强调的。其一是证明审查的主体应该是数学共同体的成员。一个证明如果是正确的，那么也就意味着其结果能够进入到数学之中成为数学知识的一部分而为数学共同体所接受，因此，一个证明是不是一个合法的证明应该由共同体成员来确定。其二，证明的长度应该是适当的，这样可以便于数学共同体的其他成员对之加以审查。如果证明过长到要一位数学家化数年甚至一辈子的时间才可以看完的话，那么这样的数学证明实际上将是难以审查的。数学证明的可审查性具有极为重要的意义，它起码从理论上保证了数学证明的正确性。数学家在完成某个数学证明后，他会对自己的证明进行反复的审查，从而尽可能发现存在的错误。然后，数学家将论文投给数学期刊，期刊编辑部会安排其他数学家对该论文进行审稿，审稿的过程也就是对数学证明审查的过程，通过该过程，如果证明中存在错误的话，审稿者可能会发现其错误所在。当论文正式发表后，阅读论文的数学家们会进一步对之进行审查，如果仍然没有发现错误，那么，证明过程及其结论就会成为数学知识的一部分从而为数学家们所吸收或内化。至此，该证明的过程和结论就真正地为数学共同体所认可。可见，数学证明的可审查性对于保证数学证明的正确性是极端重要。如果数学证明不具有可审查性的话，以传统的观点看，数学家共同体是不可能接受这样的结论进入到数学之中成为合法知识的。正如皮尔士所说的那样，数学知识是人的知识，而是人就会犯错误，因而，作为一种人的知识的数学知识就具有可谬性。大学生和中学生在做数学证明时会由于各种原因出错，数学家做数学证明时也会时常出错。数学史告诉我们，错误的证明是经常发生的即使是大名鼎鼎的数学家在进行数学证明时也无法避免犯错。例如，肯普(Kempe)在1879年发表了他对四色猜想的证明，11年后希伍德(Heawood)发现了肯普证明中的一个致命错误。1911年6月大数学家哈代(Hardy)和李特尔伍德(Litterwood)合作的一篇论文在伦敦数学会上散发，但后来他们发现其证明是错误的。1945年，拉特马赫(Rademacher)认为他已经证明出了黎曼猜想，甚至时代杂志都宣布了该结果，但后来被审查发现了错误。［5］正是由于数学证明具有可审查性，才使得许多错误的证明在公开后能够被发现。可以说，数学的健康发展，证明的可审查性功不可没。

三难以审查的数学证明的出现

传统的数学证明具有可审查性，它最大限度地保证了数学结论的无误性。数学科学从古希腊的几何到今天达数百个数学分支，数学成为一个参天大树有赖于数学内容的正确性，而这与数学证明的可审查性是分不开的。但是，数学发展到今天，竟然在数学证明上出现了不可审查的问题，以下是两个典型的例子。第一个例子是四色定理的证明。四色定理的表述如下:将平面任意地细分为不相重叠的区域，每一个区域总可以用1234这四个数字之一来标记而不会使相邻的两个区域得到相同的数字。这里所指的相邻区域是指有一整段边界是公共的，而如果两个区域只相遇于一点或有限多点就不叫相邻的。最先正式提出“四色问题”的是英国数学家凯莱，他于1872年正式向伦敦数学会提出了“四色问题”。从那以后，包括闵可夫斯基在内的不少大数学家都试图证明该猜想，但均没有成功。1976年，黑肯和阿佩尔运用计算机历时1200小时证明了“四色问题”。第二个例子是有限单群分类定理即所谓的“宏大定理”。有限单群分类定理表述如下:任何一个有限单群必定属于如下四类群中的一个:素数阶循环群、n≥5的交换群An、Lie型单群以及26个散在单群。如果从拉格朗日研究置换算起(1770年)到诺顿证实了散在群F1的唯一性为止(1981年)，前后用了200年时间，完整证明分散在大约500篇论文中，总长度达15000个印刷页。2011年四位数学家出版了一本名为《有限单群分类》的书，该书是有限单群分类证明的摘要或导读，篇幅就达350页。第一个例子代表着数学猜想的机器证明。四色定理的证明是对数学猜想进行机器证明的第一次，而在这之前，一些数学家已经运用计算机来进行许多几何定理的证明，其中就包括我国著名的数学家吴文俊先生在这方面所做的大量工作。在四色定理机器证明之后的1988年，美国数学家哈尔斯(ThomasHales)用计算机证明了开普勒猜想。与传统数学证明不同的是，这类证明并非是用形式化的数学语言书写的，而是用计算机语言表述的。实际上在黑肯和阿佩尔的四色定理证明发表后不久，数学哲学家泰马祖科就在《哲学杂志》上发表了论文“四色问题和它的哲学意义”。

论文认为，黑肯和阿佩尔运用计算机的运算和归纳所得到的结果并不能算作真正意义上的数学证明，其主要原因之一就是这样的证明不具有可审查性，他进一步提出，如果我们要承认这是一种数学证明的话，那么传统意义上的数学证明的含义就需要改变，甚至传统意义上数学的含义都需要改变。泰马祖科的论文引发了激烈的争论，一部分学者同意泰马祖科的看法，另一部分学者持反对态度，反对者的共同之处都是回避了可审查性这个数学证明重要特点的作用。例如，莱温(MargaritaLevin)否认作为数学证明特点之一的可审查性所具有的重要作用，而特勒(PaulTeller)则认为某个东西是不是一个证明与我们能不能对它进行核查是没有关系的。［6］118尽管这些反对者从很多角度对泰马祖科的观点进行批驳，但是他们无法否认黑肯和阿佩尔对四色定理证明是不能被数学家用传统的方式进行审查的事实。第二个例子代表着数学的长证明。与一般学习过中学数学甚至大学数学后对于数学证明的印象不太一样的是，今天一些数学定理的证明是需要很长的篇幅才能完成的。“宏大定理”15000页的长度也许是比较极端的，但是数百页篇幅的数学证明在今天并不鲜见，我们甚至不能排除今后还会出现其他的比“宏大定理”更“宏大”的定理证明。怀尔斯证明费马大定理用了一百多个印刷页被数学家们认为是比较简短的证明，而上文提到的哈尔斯证明开普勒猜想就用了250页的文稿和约10万行的计算机程序。究竟多长的证明才可以算做“长证明”?实际上这是一个比较模糊的概念。泰马祖科曾给出了一个界定即“一个数学家一辈子也难以审读完”的证明，显然，该界定本身也是比较模糊的。我们认为，长证明就是那些需要一个同方向数学家或数学家小组数年甚至更长时间才能审读完的数学证明。为什么长证明难以审查甚至不具有可审查性呢?以下我们进行一些分析。

首先从社会学的角度看。我们知道，数学家的工作是数学创造，是产生出新的数学知识。数学家都是社会人，荣誉、地位和财富对于数学家来说同样具有吸引力，特别是荣誉更是对于数学家有着异常强烈的吸引力。一个数学家如果用数年的时间和精力也许可以证明一个重要的数学猜想从而收获巨大的荣誉，但如果是将自己数年宝贵的时间用去审查他人的证明，他能够得到什么?怀尔斯(AndrewWiles)因为证明出费马大定理成为世人眼中的数学英雄，获得了沃尔夫奖、沃尔夫斯凯尔奖、菲尔兹特别奖以及邵逸夫数学科学奖等大奖，得到了作为数学家所能得到的最大荣誉。可是有几人知道是哪些数学家完成了对费马大定理证明的审查，这些数学家又得到了什么荣誉?

其次从证明审查的难度上看，这又可以进一步分成复杂性和困难性两个方面。首先看证明审查的复杂性。学习过中学甚至大学数学的人往往对于数学证明的印象是篇幅上不会超过一页纸并且在证明过程中只会用到数个三段论，因此，他们很难想象长证明的复杂。一个长证明会涉及很多的部分，每一部分又由逻辑推导而组成，各个部分之间存在着错综复杂的关系。在所有的数学证明中，数学家都像是在迷宫中找到一条连接已知条件和结论的通道，如果是长证明的话，数学家通过这个迷宫相对来说就更为困难。对于数学家来说是迷宫的证明，对于审查者来说同样也是迷宫。由于过长和其中的复杂性，因此，要对这样的证明进行审查是一个非常棘手的事情。贝斯勒(Bassler)分析了审查长数学证明的复杂性。他认为，审查者既要对证明进行局部的审查也要对证明进行全局性的审查，前者是一步一步地进行检查后者是从整体上进行检查，他强调光是进行局部的审查并不能保证证明的正确性［6］101－105。因此，对于长证明，不难理解数学家很少会愿意花数年甚至更长时间自觉地去进行审查。例如，对于有限单群分类定理的证明，就很少有人完整地看完所有的证明材料，甚至有一些群论数学家私下里表达了是否真的有人完整看过所有证明材料的怀疑。［7］

其次，看数学审查的困难性。由于长数学证明往往伴随着很高的难度，因此，审查这样的证明是一项很艰苦的工作。审查的过程实际上也是审查者对证明的学习理解过程，由于审查者往往面临的是新的思想和方法，因而需要审查者反复地思考。为此，审读者需要花费大量的时间和艰苦的工作。例如，2003年数学奇才佩雷尔曼(GrigoriyPerelman)完成了庞加莱猜想的证明，顶级数学家们不得不化数年的时间才完成对它的审查。再如，2012年8月底，日本数学家望月新一宣布证明了ABC猜想。该证明由四篇论文组成，总长度超500页。望月新一的证明不但长度可观，更重要的是他采用了他自己发展起来的数学工具。除了他自己，几乎没有第二个数学家能够看懂，即使是和望月新一相同研究方向的数学家也不例外。由于证明难度过大，从而使得其他的数学家在相当一段时间内对证明过程无法准确地理解，这使得对该数学证明进行审查困难重重。对于长证明审查困难的问题实际上已经引起了不少包括数学家在内的相关学者的关注。例如，内桑森(M．Nathanson)就曾在《美国数学会通告》(NoticesoftheAmericanMathematicalSociety)发文谈到了该问题，“我们怎么知道一个证明是正确的呢?只能是通过对它进行一行一行的检查。……如果一个定理的证明是短小的，那么我们确实能够检查其中是否有错。但如果该证明是难以理解并且其篇幅超过100个印刷页，或者没有人有时间和精力去详细地检查它，或者一个证明篇幅有100000页长，那么我们只能依赖该领域的大牛们去做出判断了。……在大多数进行审查的期刊中的许多论文(我认为占大多数)都没有被审查过。这些审查者大概是这样进行审查的，他看看论文，阅读一下论文的开头和结论，大致上浏览一下证明过程，如果这些看起来都没有问题的话，那么他就建议可以发表［8］”。内桑森的这段话尽管未必与实际的证明审查完全吻合，但从某种程度上确实反映了对长证明审查的困难。

四难以审查的数学证明与数学可谬性

如果我们将数学证明分成可审查的证明与不可审查的证明，因为可审查的证明能最大限度地保证其正确性，那么对于不可审查的证明，数学家们必然无法肯定其正确性。因为无法对四色定理以及其他的机器证明进行审查，定理的正确性是计算机或者运用计算机进行运算的专家(可以说是数学共同体以外的人)告诉数学家的，由于并非是数学共同体成员进行形式化的证明也并非是数学共同体成员进行审查，因此，至今仍有不少的数学家并不认可这样的证明，而不认可这样的证明也就意味着它可能并不正确。因为至今甚至都没有人完整地看完宏大定理的完整证明，因而对于很多数学家看来，证明中出现的错误也是可能的。正如在有限单群分类定理最后证明中起重要作用的阿斯伯杰(Aschbacher)所说的那样“当证明长度增加时，错误的概率也增加了。在分类定理中出现错误的概率实际上是1”［9］。机器证明和长证明的出现是与数学自身的发展以及人的证明能力有限有关的。像四色猜想这样的问题，因为数学家为此花了太多的时间而无果，人们希望能够尽快地解决这样的问题。毋庸置疑，如果有可能的话，数学家一定会通过自己的努力，用逻辑推理的方法去证明该定理。而计算机的出现为解决问题提供了一种方法。可以说是数学家自身能力的局限与计算机的出现从而导致了机器证明。长证明的出现是数学发展自然形成的。随着数学的发展，有些问题的证明需要涉及很多的内容和方法，因而显得异常复杂，需要数学家用大量的篇幅才能将其解决过程完整地表述清楚，这也正是一些猜想几十年甚至数百年难以解决的原因所在。由于证明中涉及的对象(概念、定理、方法等)过于复杂，因而在证明表述中出现各种错误将是难以避免的。可以肯定的是，像哥德巴赫猜想等一批数学难题的证明也必将是长证明。今天，从四色猜想被绝大多数数学家称为四色定理可以看出，多数数学家对于机器证明是认可的，从而可以说，今后，计算机在数学证明上将扮演一个重要的角色，机器证明也必将逐步成为一种为数学共同体认可的合法数学证明，相应地，传统的认为数学证明应该是用形式化数学语言书写的观点也将会逐步改变。另外，数学本身的发展，一些数学假设的证明也必将涉及更多的数学知识和更特别的数学方法，因此也就必然会出现了更多的长证明。伴随着机器证明和长证明的大量出现，将可能会使得未来的数学不但具有宏观上的可谬性而且更具有微观层面的可谬性。当数学中充斥着很多可谬性内容，对于数学来说意味着什么?朝气蓬勃发展的数学发展到头了?肯定不是这样。它只是意味着数学并不神圣，它不是神的创造而是人的学问。数学共同体允许可能的错误进入数学，也将会采取各种方法改正可能的错误，数学的明天一定会更加繁荣。

作者：张晓贵 单位：合肥师范学院数学与统计学院