本站小編為你精心準(zhǔn)備了對數(shù)學(xué)證明的審查及數(shù)學(xué)可謬性參考范文，愿這些范文能點(diǎn)燃您思維的火花，激發(fā)您的寫作靈感。歡迎深入閱讀并收藏。

摘要:皮爾士、拉卡托斯和歐里斯特對于數(shù)學(xué)可謬性的論斷是從宏觀的角度進(jìn)行的。數(shù)學(xué)證明的可審查性可以最大限度地保證其正確性，但機(jī)器證明和長證明使得審查難以進(jìn)行，它們的存在也為數(shù)學(xué)可謬性提供了微觀證據(jù)。

關(guān)鍵詞:數(shù)學(xué)證明;可審查性;數(shù)學(xué)可謬性

一方面，就今天的數(shù)學(xué)哲學(xué)領(lǐng)域來說，數(shù)學(xué)可謬性已經(jīng)成為共識，盡管很多數(shù)學(xué)家們對此并不在意。另一方面，數(shù)學(xué)科學(xué)在當(dāng)代的發(fā)展出現(xiàn)了一些新的情況如信息技術(shù)在數(shù)學(xué)研究中扮演重要角色、數(shù)學(xué)與現(xiàn)實(shí)的聯(lián)系更加密切以及數(shù)學(xué)家之間合作研究程度的增加等。其中，難以審查數(shù)學(xué)證明的出現(xiàn)尤為引人注目。我們認(rèn)為，難以審查數(shù)學(xué)證明的出現(xiàn)實(shí)際上為數(shù)學(xué)可謬性提供了進(jìn)一步的證據(jù)。

一數(shù)學(xué)可謬性

長期以來數(shù)學(xué)都被賦予成一種可靠、準(zhǔn)確和客觀知識的典范。一般人皆視數(shù)學(xué)為真理，數(shù)學(xué)家們對此往往更是引以為傲。數(shù)學(xué)家克蘭茨(Krantz，S)的話是具有代表性的，他說，數(shù)學(xué)“具有一種確定性，這是其他科學(xué)所不具備的。我們賦予這個系統(tǒng)以可靠性、再現(xiàn)性以及可移植性，這是任何其他科學(xué)所做不到的”?？巳R因(Kline，M)在描述傳統(tǒng)的數(shù)學(xué)真理觀也說過:“無論什么時候，當(dāng)一個人需要一個確定性和推理正確性的例子時，他一定會求助于數(shù)學(xué)”。［1］數(shù)學(xué)哲學(xué)家們對于數(shù)學(xué)知識是否具有真理性的問題很早以前就有過認(rèn)真的思考。以美國數(shù)學(xué)家和數(shù)學(xué)哲學(xué)家皮爾士(CharlesSandersPeirce，1839—1914)、匈牙利數(shù)學(xué)哲學(xué)家拉卡托斯(ImreLakatos，1922—1974)和英國數(shù)學(xué)哲學(xué)家歐里斯特(PaulEr-nest，1944—)為代表的數(shù)學(xué)哲學(xué)家相繼地提出了數(shù)學(xué)具有可謬性的看法。簡單地說，皮爾士認(rèn)為數(shù)學(xué)可謬性的根據(jù)主要是通過將數(shù)學(xué)家的數(shù)學(xué)創(chuàng)造與科學(xué)家對于經(jīng)驗(yàn)科學(xué)的探究過程進(jìn)行對比得出的。皮爾士指出，數(shù)學(xué)家在數(shù)學(xué)創(chuàng)造過程中需要將數(shù)學(xué)命題轉(zhuǎn)換成頭腦中的圖形，思維的過程就是對圖形的操作，該過程與科學(xué)家的實(shí)驗(yàn)是很相似的。由于經(jīng)驗(yàn)科學(xué)的探究是可謬的，因而數(shù)學(xué)也將是可謬的。拉卡托斯區(qū)分了兩類系統(tǒng)即歐幾里得系統(tǒng)和擬經(jīng)驗(yàn)系統(tǒng)，邏輯主義、直覺主義和形式主義三大學(xué)派的基礎(chǔ)研究本質(zhì)上都是要將全部數(shù)學(xué)重建為歐幾里得系統(tǒng)，而它們的失敗說明了數(shù)學(xué)必然是擬經(jīng)驗(yàn)的，數(shù)學(xué)的擬經(jīng)驗(yàn)性又說明了數(shù)學(xué)的可謬性。［2］歐里斯特的數(shù)學(xué)可謬觀最先來自于拉卡托斯的數(shù)學(xué)可謬思想，并在后者的基礎(chǔ)上進(jìn)行了進(jìn)一步的分析。他將數(shù)學(xué)上的認(rèn)識論觀點(diǎn)分成絕對主義數(shù)學(xué)觀和可謬主義數(shù)學(xué)觀，而三大學(xué)派都持有絕對主義數(shù)學(xué)觀。歐里斯特通過分析指出，三大學(xué)派的絕對主義數(shù)學(xué)觀都是錯誤的，因此，數(shù)學(xué)就應(yīng)該是可謬的。［3］可以看出，歐里斯特數(shù)學(xué)可謬觀的得出與拉卡托斯在本質(zhì)上是類似的，都是通過對于絕對主義數(shù)學(xué)觀的否定而實(shí)現(xiàn)的，而皮爾士的數(shù)學(xué)可謬觀則是通過對于數(shù)學(xué)創(chuàng)造與經(jīng)驗(yàn)科學(xué)的探究之間的相似性而得出。盡管二者是從不同的途徑得出數(shù)學(xué)可謬性這個相同的結(jié)論，但二者之間也有其共同點(diǎn)，那就是它們都是從宏觀上說明數(shù)學(xué)是可謬的。根據(jù)皮爾士觀點(diǎn)，既然數(shù)學(xué)創(chuàng)造與自然科學(xué)的探究相似，那么數(shù)學(xué)本身就一定也像自然科學(xué)一樣是可謬的;而根據(jù)拉卡特斯與歐里斯特的觀點(diǎn)，可謬性本來就是數(shù)學(xué)自身的特點(diǎn)。那么，除此之外，是否還有其他的證據(jù)表明數(shù)學(xué)的可謬性呢?特別是，現(xiàn)代數(shù)學(xué)發(fā)展有沒有為數(shù)學(xué)可謬性提供更加微觀的證據(jù)呢?

二數(shù)學(xué)證明可審查的必要性

數(shù)學(xué)證明被認(rèn)為是數(shù)學(xué)與自然科學(xué)之間的核心區(qū)別所在，它在數(shù)學(xué)發(fā)展中扮演著極為重要的作用。通過數(shù)學(xué)證明，一個對錯不定的數(shù)學(xué)猜想或者變成了一個數(shù)學(xué)真命題或數(shù)學(xué)定理，或者被認(rèn)定為假命題而拋棄。就數(shù)學(xué)共同體來說，數(shù)學(xué)證明發(fā)揮著讓數(shù)學(xué)家們確信某個命題是正確無誤的作用，從而可以讓他們在自己的數(shù)學(xué)研究中放心地加以運(yùn)用。就數(shù)學(xué)科學(xué)來說，數(shù)學(xué)證明是數(shù)學(xué)發(fā)展的必要途徑，通過數(shù)學(xué)證明得到一個個數(shù)學(xué)真命題，而數(shù)學(xué)真命題是一個數(shù)學(xué)分支的主要構(gòu)成。顯然，數(shù)學(xué)證明要想發(fā)揮應(yīng)有作用，正確性是最基本的要求。泰馬祖科(ThomasTymoczko)認(rèn)為，在傳統(tǒng)的數(shù)學(xué)觀念中，數(shù)學(xué)證明具有三個基本的特點(diǎn)即有說服力、可審查性以及形式化［4］。有說服力就是上文所說的讓共同體中其他數(shù)學(xué)家對該證明的正確性充分的確信，可審查是指其他的數(shù)學(xué)家能夠對數(shù)學(xué)證明進(jìn)行檢查以確定其是否正確，形式化是指數(shù)學(xué)證明應(yīng)該用形式化的數(shù)學(xué)語言書寫而成。其實(shí)，這三點(diǎn)之間是有聯(lián)系的，形式化是證明的外在形式，可審查性保證了證明的正確性，而有說服力則是可審查性的結(jié)果。形式化是可審查性的必要條件，數(shù)學(xué)內(nèi)容用形式化的數(shù)學(xué)語言進(jìn)行表述是現(xiàn)代數(shù)學(xué)的表現(xiàn)形式，數(shù)學(xué)共同體中的成員要對數(shù)學(xué)證明進(jìn)行審查，當(dāng)然需要該證明是用形式化的數(shù)學(xué)語言書寫的，否則數(shù)學(xué)家可能根本就看不懂，從而就不存在審查了，從這個角度看，形式化其實(shí)是附著于可審查性的。因此，傳統(tǒng)數(shù)學(xué)證明的三個特點(diǎn)的核心應(yīng)該是可審查性。關(guān)于可審查性，除了要求證明要用數(shù)學(xué)共同體共同認(rèn)可的數(shù)學(xué)語言進(jìn)行形式化書寫外，還有兩點(diǎn)是需要強(qiáng)調(diào)的。其一是證明審查的主體應(yīng)該是數(shù)學(xué)共同體的成員。一個證明如果是正確的，那么也就意味著其結(jié)果能夠進(jìn)入到數(shù)學(xué)之中成為數(shù)學(xué)知識的一部分而為數(shù)學(xué)共同體所接受，因此，一個證明是不是一個合法的證明應(yīng)該由共同體成員來確定。其二，證明的長度應(yīng)該是適當(dāng)?shù)?，這樣可以便于數(shù)學(xué)共同體的其他成員對之加以審查。如果證明過長到要一位數(shù)學(xué)家化數(shù)年甚至一輩子的時間才可以看完的話，那么這樣的數(shù)學(xué)證明實(shí)際上將是難以審查的。數(shù)學(xué)證明的可審查性具有極為重要的意義，它起碼從理論上保證了數(shù)學(xué)證明的正確性。數(shù)學(xué)家在完成某個數(shù)學(xué)證明后，他會對自己的證明進(jìn)行反復(fù)的審查，從而盡可能發(fā)現(xiàn)存在的錯誤。然后，數(shù)學(xué)家將論文投給數(shù)學(xué)期刊，期刊編輯部會安排其他數(shù)學(xué)家對該論文進(jìn)行審稿，審稿的過程也就是對數(shù)學(xué)證明審查的過程，通過該過程，如果證明中存在錯誤的話，審稿者可能會發(fā)現(xiàn)其錯誤所在。當(dāng)論文正式發(fā)表后，閱讀論文的數(shù)學(xué)家們會進(jìn)一步對之進(jìn)行審查，如果仍然沒有發(fā)現(xiàn)錯誤，那么，證明過程及其結(jié)論就會成為數(shù)學(xué)知識的一部分從而為數(shù)學(xué)家們所吸收或內(nèi)化。至此，該證明的過程和結(jié)論就真正地為數(shù)學(xué)共同體所認(rèn)可?？梢?，數(shù)學(xué)證明的可審查性對于保證數(shù)學(xué)證明的正確性是極端重要。如果數(shù)學(xué)證明不具有可審查性的話，以傳統(tǒng)的觀點(diǎn)看，數(shù)學(xué)家共同體是不可能接受這樣的結(jié)論進(jìn)入到數(shù)學(xué)之中成為合法知識的。正如皮爾士所說的那樣，數(shù)學(xué)知識是人的知識，而是人就會犯錯誤，因而，作為一種人的知識的數(shù)學(xué)知識就具有可謬性。大學(xué)生和中學(xué)生在做數(shù)學(xué)證明時會由于各種原因出錯，數(shù)學(xué)家做數(shù)學(xué)證明時也會時常出錯。數(shù)學(xué)史告訴我們，錯誤的證明是經(jīng)常發(fā)生的即使是大名鼎鼎的數(shù)學(xué)家在進(jìn)行數(shù)學(xué)證明時也無法避免犯錯。例如，肯普(Kempe)在1879年發(fā)表了他對四色猜想的證明，11年后希伍德(Heawood)發(fā)現(xiàn)了肯普證明中的一個致命錯誤。1911年6月大數(shù)學(xué)家哈代(Hardy)和李特爾伍德(Litterwood)合作的一篇論文在倫敦數(shù)學(xué)會上散發(fā)，但后來他們發(fā)現(xiàn)其證明是錯誤的。1945年，拉特馬赫(Rademacher)認(rèn)為他已經(jīng)證明出了黎曼猜想，甚至?xí)r代雜志都宣布了該結(jié)果，但后來被審查發(fā)現(xiàn)了錯誤。［5］正是由于數(shù)學(xué)證明具有可審查性，才使得許多錯誤的證明在公開后能夠被發(fā)現(xiàn)?？梢哉f，數(shù)學(xué)的健康發(fā)展，證明的可審查性功不可沒。

三難以審查的數(shù)學(xué)證明的出現(xiàn)

傳統(tǒng)的數(shù)學(xué)證明具有可審查性，它最大限度地保證了數(shù)學(xué)結(jié)論的無誤性。數(shù)學(xué)科學(xué)從古希臘的幾何到今天達(dá)數(shù)百個數(shù)學(xué)分支，數(shù)學(xué)成為一個參天大樹有賴于數(shù)學(xué)內(nèi)容的正確性，而這與數(shù)學(xué)證明的可審查性是分不開的。但是，數(shù)學(xué)發(fā)展到今天，竟然在數(shù)學(xué)證明上出現(xiàn)了不可審查的問題，以下是兩個典型的例子。第一個例子是四色定理的證明。四色定理的表述如下:將平面任意地細(xì)分為不相重疊的區(qū)域，每一個區(qū)域總可以用1234這四個數(shù)字之一來標(biāo)記而不會使相鄰的兩個區(qū)域得到相同的數(shù)字。這里所指的相鄰區(qū)域是指有一整段邊界是公共的，而如果兩個區(qū)域只相遇于一點(diǎn)或有限多點(diǎn)就不叫相鄰的。最先正式提出“四色問題”的是英國數(shù)學(xué)家凱萊，他于1872年正式向倫敦數(shù)學(xué)會提出了“四色問題”。從那以后，包括閔可夫斯基在內(nèi)的不少大數(shù)學(xué)家都試圖證明該猜想，但均沒有成功。1976年，黑肯和阿佩爾運(yùn)用計算機(jī)歷時1200小時證明了“四色問題”。第二個例子是有限單群分類定理即所謂的“宏大定理”。有限單群分類定理表述如下:任何一個有限單群必定屬于如下四類群中的一個:素數(shù)階循環(huán)群、n≥5的交換群An、Lie型單群以及26個散在單群。如果從拉格朗日研究置換算起(1770年)到諾頓證實(shí)了散在群F1的唯一性為止(1981年)，前后用了200年時間，完整證明分散在大約500篇論文中，總長度達(dá)15000個印刷頁。2011年四位數(shù)學(xué)家出版了一本名為《有限單群分類》的書，該書是有限單群分類證明的摘要或?qū)ёx，篇幅就達(dá)350頁。第一個例子代表著數(shù)學(xué)猜想的機(jī)器證明。四色定理的證明是對數(shù)學(xué)猜想進(jìn)行機(jī)器證明的第一次，而在這之前，一些數(shù)學(xué)家已經(jīng)運(yùn)用計算機(jī)來進(jìn)行許多幾何定理的證明，其中就包括我國著名的數(shù)學(xué)家吳文俊先生在這方面所做的大量工作。在四色定理機(jī)器證明之后的1988年，美國數(shù)學(xué)家哈爾斯(ThomasHales)用計算機(jī)證明了開普勒猜想。與傳統(tǒng)數(shù)學(xué)證明不同的是，這類證明并非是用形式化的數(shù)學(xué)語言書寫的，而是用計算機(jī)語言表述的。實(shí)際上在黑肯和阿佩爾的四色定理證明發(fā)表后不久，數(shù)學(xué)哲學(xué)家泰馬祖科就在《哲學(xué)雜志》上發(fā)表了論文“四色問題和它的哲學(xué)意義”。

論文認(rèn)為，黑肯和阿佩爾運(yùn)用計算機(jī)的運(yùn)算和歸納所得到的結(jié)果并不能算作真正意義上的數(shù)學(xué)證明，其主要原因之一就是這樣的證明不具有可審查性，他進(jìn)一步提出，如果我們要承認(rèn)這是一種數(shù)學(xué)證明的話，那么傳統(tǒng)意義上的數(shù)學(xué)證明的含義就需要改變，甚至傳統(tǒng)意義上數(shù)學(xué)的含義都需要改變。泰馬祖科的論文引發(fā)了激烈的爭論，一部分學(xué)者同意泰馬祖科的看法，另一部分學(xué)者持反對態(tài)度，反對者的共同之處都是回避了可審查性這個數(shù)學(xué)證明重要特點(diǎn)的作用。例如，萊溫(MargaritaLevin)否認(rèn)作為數(shù)學(xué)證明特點(diǎn)之一的可審查性所具有的重要作用，而特勒(PaulTeller)則認(rèn)為某個東西是不是一個證明與我們能不能對它進(jìn)行核查是沒有關(guān)系的。［6］118盡管這些反對者從很多角度對泰馬祖科的觀點(diǎn)進(jìn)行批駁，但是他們無法否認(rèn)黑肯和阿佩爾對四色定理證明是不能被數(shù)學(xué)家用傳統(tǒng)的方式進(jìn)行審查的事實(shí)。第二個例子代表著數(shù)學(xué)的長證明。與一般學(xué)習(xí)過中學(xué)數(shù)學(xué)甚至大學(xué)數(shù)學(xué)后對于數(shù)學(xué)證明的印象不太一樣的是，今天一些數(shù)學(xué)定理的證明是需要很長的篇幅才能完成的?！昂甏蠖ɡ怼?5000頁的長度也許是比較極端的，但是數(shù)百頁篇幅的數(shù)學(xué)證明在今天并不鮮見，我們甚至不能排除今后還會出現(xiàn)其他的比“宏大定理”更“宏大”的定理證明。懷爾斯證明費(fèi)馬大定理用了一百多個印刷頁被數(shù)學(xué)家們認(rèn)為是比較簡短的證明，而上文提到的哈爾斯證明開普勒猜想就用了250頁的文稿和約10萬行的計算機(jī)程序。究竟多長的證明才可以算做“長證明”?實(shí)際上這是一個比較模糊的概念。泰馬祖科曾給出了一個界定即“一個數(shù)學(xué)家一輩子也難以審讀完”的證明，顯然，該界定本身也是比較模糊的。我們認(rèn)為，長證明就是那些需要一個同方向數(shù)學(xué)家或數(shù)學(xué)家小組數(shù)年甚至更長時間才能審讀完的數(shù)學(xué)證明。為什么長證明難以審查甚至不具有可審查性呢?以下我們進(jìn)行一些分析。

首先從社會學(xué)的角度看。我們知道，數(shù)學(xué)家的工作是數(shù)學(xué)創(chuàng)造，是產(chǎn)生出新的數(shù)學(xué)知識。數(shù)學(xué)家都是社會人，榮譽(yù)、地位和財富對于數(shù)學(xué)家來說同樣具有吸引力，特別是榮譽(yù)更是對于數(shù)學(xué)家有著異常強(qiáng)烈的吸引力。一個數(shù)學(xué)家如果用數(shù)年的時間和精力也許可以證明一個重要的數(shù)學(xué)猜想從而收獲巨大的榮譽(yù)，但如果是將自己數(shù)年寶貴的時間用去審查他人的證明，他能夠得到什么?懷爾斯(AndrewWiles)因?yàn)樽C明出費(fèi)馬大定理成為世人眼中的數(shù)學(xué)英雄，獲得了沃爾夫獎、沃爾夫斯凱爾獎、菲爾茲特別獎以及邵逸夫數(shù)學(xué)科學(xué)獎等大獎，得到了作為數(shù)學(xué)家所能得到的最大榮譽(yù)。可是有幾人知道是哪些數(shù)學(xué)家完成了對費(fèi)馬大定理證明的審查，這些數(shù)學(xué)家又得到了什么榮譽(yù)?

其次從證明審查的難度上看，這又可以進(jìn)一步分成復(fù)雜性和困難性兩個方面。首先看證明審查的復(fù)雜性。學(xué)習(xí)過中學(xué)甚至大學(xué)數(shù)學(xué)的人往往對于數(shù)學(xué)證明的印象是篇幅上不會超過一頁紙并且在證明過程中只會用到數(shù)個三段論，因此，他們很難想象長證明的復(fù)雜。一個長證明會涉及很多的部分，每一部分又由邏輯推導(dǎo)而組成，各個部分之間存在著錯綜復(fù)雜的關(guān)系。在所有的數(shù)學(xué)證明中，數(shù)學(xué)家都像是在迷宮中找到一條連接已知條件和結(jié)論的通道，如果是長證明的話，數(shù)學(xué)家通過這個迷宮相對來說就更為困難。對于數(shù)學(xué)家來說是迷宮的證明，對于審查者來說同樣也是迷宮。由于過長和其中的復(fù)雜性，因此，要對這樣的證明進(jìn)行審查是一個非常棘手的事情。貝斯勒(Bassler)分析了審查長數(shù)學(xué)證明的復(fù)雜性。他認(rèn)為，審查者既要對證明進(jìn)行局部的審查也要對證明進(jìn)行全局性的審查，前者是一步一步地進(jìn)行檢查后者是從整體上進(jìn)行檢查，他強(qiáng)調(diào)光是進(jìn)行局部的審查并不能保證證明的正確性［6］101－105。因此，對于長證明，不難理解數(shù)學(xué)家很少會愿意花數(shù)年甚至更長時間自覺地去進(jìn)行審查。例如，對于有限單群分類定理的證明，就很少有人完整地看完所有的證明材料，甚至有一些群論數(shù)學(xué)家私下里表達(dá)了是否真的有人完整看過所有證明材料的懷疑。［7］

其次，看數(shù)學(xué)審查的困難性。由于長數(shù)學(xué)證明往往伴隨著很高的難度，因此，審查這樣的證明是一項(xiàng)很艱苦的工作。審查的過程實(shí)際上也是審查者對證明的學(xué)習(xí)理解過程，由于審查者往往面臨的是新的思想和方法，因而需要審查者反復(fù)地思考。為此，審讀者需要花費(fèi)大量的時間和艱苦的工作。例如，2003年數(shù)學(xué)奇才佩雷爾曼(GrigoriyPerelman)完成了龐加萊猜想的證明，頂級數(shù)學(xué)家們不得不化數(shù)年的時間才完成對它的審查。再如，2012年8月底，日本數(shù)學(xué)家望月新一宣布證明了ABC猜想。該證明由四篇論文組成，總長度超500頁。望月新一的證明不但長度可觀，更重要的是他采用了他自己發(fā)展起來的數(shù)學(xué)工具。除了他自己，幾乎沒有第二個數(shù)學(xué)家能夠看懂，即使是和望月新一相同研究方向的數(shù)學(xué)家也不例外。由于證明難度過大，從而使得其他的數(shù)學(xué)家在相當(dāng)一段時間內(nèi)對證明過程無法準(zhǔn)確地理解，這使得對該數(shù)學(xué)證明進(jìn)行審查困難重重。對于長證明審查困難的問題實(shí)際上已經(jīng)引起了不少包括數(shù)學(xué)家在內(nèi)的相關(guān)學(xué)者的關(guān)注。例如，內(nèi)桑森(M．Nathanson)就曾在《美國數(shù)學(xué)會通告》(NoticesoftheAmericanMathematicalSociety)發(fā)文談到了該問題，“我們怎么知道一個證明是正確的呢?只能是通過對它進(jìn)行一行一行的檢查。……如果一個定理的證明是短小的，那么我們確實(shí)能夠檢查其中是否有錯。但如果該證明是難以理解并且其篇幅超過100個印刷頁，或者沒有人有時間和精力去詳細(xì)地檢查它，或者一個證明篇幅有100000頁長，那么我們只能依賴該領(lǐng)域的大牛們?nèi)プ龀雠袛嗔??！诖蠖鄶?shù)進(jìn)行審查的期刊中的許多論文(我認(rèn)為占大多數(shù))都沒有被審查過。這些審查者大概是這樣進(jìn)行審查的，他看看論文，閱讀一下論文的開頭和結(jié)論，大致上瀏覽一下證明過程，如果這些看起來都沒有問題的話，那么他就建議可以發(fā)表［8］”。內(nèi)桑森的這段話盡管未必與實(shí)際的證明審查完全吻合，但從某種程度上確實(shí)反映了對長證明審查的困難。

四難以審查的數(shù)學(xué)證明與數(shù)學(xué)可謬性

如果我們將數(shù)學(xué)證明分成可審查的證明與不可審查的證明，因?yàn)榭蓪彶榈淖C明能最大限度地保證其正確性，那么對于不可審查的證明，數(shù)學(xué)家們必然無法肯定其正確性。因?yàn)闊o法對四色定理以及其他的機(jī)器證明進(jìn)行審查，定理的正確性是計算機(jī)或者運(yùn)用計算機(jī)進(jìn)行運(yùn)算的專家(可以說是數(shù)學(xué)共同體以外的人)告訴數(shù)學(xué)家的，由于并非是數(shù)學(xué)共同體成員進(jìn)行形式化的證明也并非是數(shù)學(xué)共同體成員進(jìn)行審查，因此，至今仍有不少的數(shù)學(xué)家并不認(rèn)可這樣的證明，而不認(rèn)可這樣的證明也就意味著它可能并不正確。因?yàn)橹两裆踔炼紱]有人完整地看完宏大定理的完整證明，因而對于很多數(shù)學(xué)家看來，證明中出現(xiàn)的錯誤也是可能的。正如在有限單群分類定理最后證明中起重要作用的阿斯伯杰(Aschbacher)所說的那樣“當(dāng)證明長度增加時，錯誤的概率也增加了。在分類定理中出現(xiàn)錯誤的概率實(shí)際上是1”［9］。機(jī)器證明和長證明的出現(xiàn)是與數(shù)學(xué)自身的發(fā)展以及人的證明能力有限有關(guān)的。像四色猜想這樣的問題，因?yàn)閿?shù)學(xué)家為此花了太多的時間而無果，人們希望能夠盡快地解決這樣的問題。毋庸置疑，如果有可能的話，數(shù)學(xué)家一定會通過自己的努力，用邏輯推理的方法去證明該定理。而計算機(jī)的出現(xiàn)為解決問題提供了一種方法。可以說是數(shù)學(xué)家自身能力的局限與計算機(jī)的出現(xiàn)從而導(dǎo)致了機(jī)器證明。長證明的出現(xiàn)是數(shù)學(xué)發(fā)展自然形成的。隨著數(shù)學(xué)的發(fā)展，有些問題的證明需要涉及很多的內(nèi)容和方法，因而顯得異常復(fù)雜，需要數(shù)學(xué)家用大量的篇幅才能將其解決過程完整地表述清楚，這也正是一些猜想幾十年甚至數(shù)百年難以解決的原因所在。由于證明中涉及的對象(概念、定理、方法等)過于復(fù)雜，因而在證明表述中出現(xiàn)各種錯誤將是難以避免的?？梢钥隙ǖ氖?，像哥德巴赫猜想等一批數(shù)學(xué)難題的證明也必將是長證明。今天，從四色猜想被絕大多數(shù)數(shù)學(xué)家稱為四色定理可以看出，多數(shù)數(shù)學(xué)家對于機(jī)器證明是認(rèn)可的，從而可以說，今后，計算機(jī)在數(shù)學(xué)證明上將扮演一個重要的角色，機(jī)器證明也必將逐步成為一種為數(shù)學(xué)共同體認(rèn)可的合法數(shù)學(xué)證明，相應(yīng)地，傳統(tǒng)的認(rèn)為數(shù)學(xué)證明應(yīng)該是用形式化數(shù)學(xué)語言書寫的觀點(diǎn)也將會逐步改變。另外，數(shù)學(xué)本身的發(fā)展，一些數(shù)學(xué)假設(shè)的證明也必將涉及更多的數(shù)學(xué)知識和更特別的數(shù)學(xué)方法，因此也就必然會出現(xiàn)了更多的長證明。伴隨著機(jī)器證明和長證明的大量出現(xiàn)，將可能會使得未來的數(shù)學(xué)不但具有宏觀上的可謬性而且更具有微觀層面的可謬性。當(dāng)數(shù)學(xué)中充斥著很多可謬性內(nèi)容，對于數(shù)學(xué)來說意味著什么?朝氣蓬勃發(fā)展的數(shù)學(xué)發(fā)展到頭了?肯定不是這樣。它只是意味著數(shù)學(xué)并不神圣，它不是神的創(chuàng)造而是人的學(xué)問。數(shù)學(xué)共同體允許可能的錯誤進(jìn)入數(shù)學(xué)，也將會采取各種方法改正可能的錯誤，數(shù)學(xué)的明天一定會更加繁榮。

作者：張曉貴 單位：合肥師范學(xué)院數(shù)學(xué)與統(tǒng)計學(xué)院