圖論中的四維猜想

圖論中的四維猜想

數(shù)學(xué)不是一門經(jīng)驗(yàn)科學(xué)，大多數(shù)問(wèn)題都沒(méi)有經(jīng)驗(yàn)。甚至敘述起來(lái)最簡(jiǎn)單的問(wèn)題或定理,都需要一定的概念(理性)支持,而且很難用經(jīng)驗(yàn)的方法來(lái)證實(shí)。典型的問(wèn)題有三角形內(nèi)角和為180°,雖然這些概念都很直觀,但是,對(duì)無(wú)窮多三角形無(wú)法一一用經(jīng)驗(yàn)方法證明,甚至發(fā)現(xiàn)這個(gè)問(wèn)題也需要理性的思考,而一般人根本想都想不到。另一個(gè)問(wèn)題就是熟知的哥德巴赫(C.Goldbach,1690-1764)猜想。雖然哥德巴赫在試驗(yàn)的方法下通過(guò)驗(yàn)證提出猜想,但它首先必須先有素?cái)?shù)的概念。雖然人們窮其一生可對(duì)有限的情形進(jìn)行驗(yàn)證,但這并非證明,因?yàn)轵?yàn)證只能對(duì)有限的情形說(shuō)對(duì)或不對(duì),而不能對(duì)無(wú)窮多情形說(shuō)對(duì)。因此數(shù)學(xué)的證明本質(zhì)上是非經(jīng)驗(yàn)的(除非通過(guò)經(jīng)驗(yàn)的辦法提出反例),而且正面的證明是“用有限駕馭無(wú)窮”?？低袪?G.Cantor,1845-1918)說(shuō),在數(shù)學(xué)的領(lǐng)域中,設(shè)問(wèn)的藝術(shù)有時(shí)要比解題的藝術(shù)更重要。愛因斯坦也說(shuō)過(guò)類似的話。物理學(xué)的問(wèn)題大都有經(jīng)驗(yàn)的來(lái)源,例如,怎樣做交換超導(dǎo)體?它的前提首先是實(shí)驗(yàn)室中已發(fā)現(xiàn)超導(dǎo)現(xiàn)象。數(shù)學(xué)的問(wèn)題則大不相同,絕大多數(shù)問(wèn)題是內(nèi)生的。許多人都認(rèn)為追根溯源數(shù)學(xué)概念是從經(jīng)驗(yàn)中歸納得出的,但是,數(shù)學(xué)發(fā)展到今天,已經(jīng)脫離開實(shí)際很遠(yuǎn)了。對(duì)于非本專業(yè)的人來(lái)說(shuō),理解一個(gè)簡(jiǎn)單的數(shù)學(xué)問(wèn)題都是十分困難的,例如龐加萊猜想:3維單連通閉流形一定是3維球面。就牽涉到維數(shù)、單連通、閉、流形、3維球面等五個(gè)概念,而且3維球面根本在現(xiàn)實(shí)世界中也是摸不著、看不見的東西,無(wú)從談到經(jīng)驗(yàn),只能靠數(shù)學(xué)家的想象以及由此產(chǎn)生出的抽象的、嚴(yán)密的理論。當(dāng)然,在現(xiàn)實(shí)生活中,人們從實(shí)踐中也的確提出過(guò)一些經(jīng)驗(yàn)問(wèn)題。四色問(wèn)題就是其中最為典型的一個(gè)。這種問(wèn)題在數(shù)學(xué)問(wèn)題的汪洋大海中往往顯不出它的重要性,因此常常被邊緣化。由于這種問(wèn)題提法簡(jiǎn)單明確,通常被許多數(shù)學(xué)愛好者以及一些數(shù)學(xué)家看成是對(duì)數(shù)學(xué)智力的挑戰(zhàn)。當(dāng)有修養(yǎng)的數(shù)學(xué)家也遇到困難時(shí),往往會(huì)有一些大數(shù)學(xué)家認(rèn)真對(duì)待這類問(wèn)題,甚至由此導(dǎo)致問(wèn)題的解決。這種經(jīng)驗(yàn)來(lái)源的問(wèn)題雖然本身并非主流,一旦被大數(shù)學(xué)家重視,經(jīng)過(guò)他們的研究、發(fā)展及推廣,往往會(huì)形成繁茂的數(shù)學(xué)分支,進(jìn)入數(shù)學(xué)的主流當(dāng)中。本文就試圖通過(guò)四色問(wèn)題的解決過(guò)程來(lái)闡明一個(gè)經(jīng)驗(yàn)來(lái)源的數(shù)學(xué)問(wèn)題如何解決,如何發(fā)展壯大形成圖論的核心分支。一、德條件的四色問(wèn)題四色問(wèn)題來(lái)源于繪制地圖的實(shí)踐。當(dāng)繪制一幅地圖時(shí),往往需要用不同顏色將相鄰區(qū)域區(qū)別開來(lái),這樣四種顏色是否就夠了呢?這里的相鄰區(qū)域是指具有公共邊界的區(qū)域。當(dāng)兩個(gè)區(qū)域僅在有限的點(diǎn)處鄰接時(shí),用同一種顏色即可。1852年,葛斯瑞(FrancisGuthrie,1831-1899)在給一張英國(guó)地圖染色時(shí)猜想:對(duì)任意地圖染色,四色足夠。,他曾寫信問(wèn)弟弟弗雷德里克(FrederickGuthrie)能不能給出數(shù)學(xué)證明。弗雷德里克無(wú)法解答,便拿去請(qǐng)教著名數(shù)學(xué)家德·摩根(A.DeMorgan,1806-1871)。德·摩根雖證明了地圖上不存在五個(gè)國(guó)家彼此都相鄰的事實(shí),但是地圖所需色數(shù)不等于相鄰國(guó)家數(shù)的最大值。證明四色問(wèn)題需要更有力的數(shù)學(xué)方法。同年10月23日,德·摩根致信當(dāng)時(shí)最偉大的數(shù)學(xué)家、物理學(xué)家哈密頓(W.R.Hamilton,1805-1865),然而得到的答復(fù)卻是對(duì)染色問(wèn)題“不感興趣”。之后,為引起其他數(shù)學(xué)家的關(guān)注,德·摩根繼續(xù)用各種方式傳播四色問(wèn)題。目前所發(fā)現(xiàn)的第一個(gè)正式的文字記錄,是他在1860年4月14日發(fā)表的一篇書評(píng)(,p.92)。除德摩根外,英國(guó)大數(shù)學(xué)家凱萊(A.Cayley,1821-1895)對(duì)四色問(wèn)題的早期傳播也做出了巨大貢獻(xiàn)。1878年6月13日,他在倫敦?cái)?shù)學(xué)會(huì)上當(dāng)場(chǎng)發(fā)問(wèn)是否有人證明了四色問(wèn)題。次年,他還在《英國(guó)皇家地理學(xué)會(huì)會(huì)報(bào)》發(fā)表論文,第一次從數(shù)學(xué)的角度明確陳述了這一猜想,并指出了證明的困難所在,最后他表示“還不能給出證明”。大數(shù)學(xué)家對(duì)四色問(wèn)題的關(guān)注自然也激發(fā)了其他人的求解欲望。在那個(gè)時(shí)候,一種普遍的觀點(diǎn)卻是四色問(wèn)題應(yīng)該不會(huì)太難,或許很快就能解決。然而,事實(shí)證明并非如此。四色問(wèn)題從猜想到定理歷經(jīng)三代證明:1976年阿佩爾(K.Appel,1932-)和哈肯(W.Haken,1928-)的計(jì)算機(jī)輔助證明,不過(guò)這個(gè)證明在長(zhǎng)達(dá)20年內(nèi)未能獲得一致認(rèn)同,原因在于證明中使用了計(jì)算機(jī),且無(wú)法用手算核實(shí);而理應(yīng)用手算核實(shí)的部分又極其繁瑣以至于沒(méi)有人能夠獨(dú)立進(jìn)行驗(yàn)證。鑒于此,1994年,西繆爾(P.Seymour,1950-)、羅伯遜(N.Robertson,1938-)、桑德斯(D.P.Sanders)和托馬斯(R.Thomas)做出了屬于他們自己的證明。二代證明雖然也使用了計(jì)算機(jī),但它達(dá)到了單獨(dú)人工復(fù)核的標(biāo)準(zhǔn),且在幾分鐘內(nèi)就能用計(jì)算機(jī)輔助驗(yàn)證,從而消除了人們對(duì)一代證明有效性的懷疑,有力地肯定了四色定理的正確性。盡管如此,隱藏在計(jì)算機(jī)內(nèi)部的邏輯步驟終究不夠透明。2005年,貢蒂埃(GeorgesGonthier)的形式證明就是一種把所有邏輯步驟都寫出了的證明,這第三代證明不僅強(qiáng)烈肯定四色定理確是一個(gè)定理,而且對(duì)數(shù)學(xué)和計(jì)算機(jī)科學(xué)都有著十分重要的意義。每一代證明都不是在平地上創(chuàng)造出業(yè)績(jī)的,許多先驅(qū)者的工作為他們鋪平了道路。第三代證明基本上是對(duì)第二代證明的邏輯步驟的機(jī)器檢驗(yàn)和確認(rèn);第二代證明是對(duì)第一代證明的修正;第一代證明則是建立在肯普(A.B.Kempe,1849-1922)的思想方法基礎(chǔ)上的。下面分別概述四色定理的這三代證明及其思想傳承關(guān)系。二、可約性理論的起源在四色定理的一代證明中,從邏輯上講,第一步是用放電法構(gòu)造不可避免集;第二步是證明不可避免集中每一個(gè)構(gòu)形的可約性。然而在歷史上,首先得到的是許多可約性論據(jù)。肯普以后,美國(guó)數(shù)學(xué)家伯克霍夫(G.D.Birkhoff,1884-1944)首先取得了可約性理論的一些進(jìn)展。其后,德國(guó)數(shù)學(xué)家希什(H.Heesch,1906-1995)提出了放電法,最終由阿佩爾和哈肯借助計(jì)算機(jī)證明了四色定理。下面簡(jiǎn)要概述為一代證明直接做出貢獻(xiàn)的數(shù)學(xué)家們的工作。1.色問(wèn)題的有限集1879年,肯普宣稱“證明”了四色定理。但11年后被發(fā)現(xiàn)有缺陷。這立即引起許多大數(shù)學(xué)家的注意,其中包括伯克霍夫、麥克萊恩(S.MacLane,1909-2005)、惠特尼(H.Whitney,1907-1989)等大數(shù)學(xué)家。事實(shí)上,“幾乎每一位大數(shù)學(xué)家都曾在某個(gè)時(shí)候試圖解決四色猜想,且都曾暫時(shí)認(rèn)為自己成功了”。然而,與肯普一樣,他們的論證同樣經(jīng)不起時(shí)間的考驗(yàn)。不過(guò),肯普的“證明”卻為后世數(shù)學(xué)家提供了解決問(wèn)題的突破口,其中蘊(yùn)含了解決四色問(wèn)題的必不可少的思想和方法。四色問(wèn)題的難點(diǎn)之一是涉及無(wú)窮:研究對(duì)象是無(wú)窮多個(gè)任意地圖。利用歐拉公式,肯普證明任意地圖都伴隨有一個(gè)至少需要同樣多顏色的正規(guī)地圖,于是,問(wèn)題就變成對(duì)正規(guī)地圖證明四色足夠。盡管如此,還是無(wú)法避免無(wú)窮多的困擾。對(duì)此,肯普使用了歸謬法:先假設(shè)存在需5種顏色才能染色的正規(guī)地圖,然后尋找矛盾,從而證明四色足夠。在尋找矛盾的論證過(guò)程中,肯普隱約地引入了兩個(gè)概念:不可避免性和可約性。第一個(gè)概念源于正規(guī)地圖的性質(zhì)。任意正規(guī)地圖至少有一國(guó)具有2、3、4或5個(gè)鄰國(guó),換言之,2個(gè)、3個(gè)、4個(gè)和5個(gè)鄰國(guó)的“構(gòu)形”是不可避免的。所謂可約性,是指從正規(guī)地圖中移去某個(gè)子圖,所得新圖的可四色性蘊(yùn)含原圖的可四色性。這樣的正規(guī)地圖就稱為可約的;而被移去的子圖就叫做可約構(gòu)形?？掀盏某錾敕ㄊ?只要能證明不可避免集中的每個(gè)構(gòu)形都是可約的,四色問(wèn)題就證出來(lái)了。接下來(lái),對(duì)于事先假定的五色地圖,他分成以下四種情況檢查構(gòu)形的可約性:(i)2個(gè)鄰國(guó);(ii)3個(gè)鄰國(guó);(iii)4個(gè)鄰國(guó);(iv)5個(gè)鄰國(guó)。顯然,如果都可約,就與需要5種顏色產(chǎn)生矛盾,從而證明四色定理成立。然而,他提出的“肯普鏈”方法只是正確證明了(i)-(iii)三種情況,遇到(iv)時(shí)卻失敗了,原因是兩次使用肯普鏈而導(dǎo)致疏漏。這個(gè)缺陷由希伍德(P.J.Heawood,1861-1955)在1890年首先指出(希伍德通過(guò)修補(bǔ)肯普的證明得到了著名的五色定理)?！岸ɡ怼敝匦伦兓亍安孪搿薄拇?數(shù)學(xué)家便意識(shí)到,四色問(wèn)題可能要比預(yù)想的難得多。19世紀(jì)末是四色問(wèn)題發(fā)展的一個(gè)分水嶺?？掀针m然未能成功,但他的證明路線為后人指明了方向:尋找可約構(gòu)形的不可避免集。1913年,伯克霍夫發(fā)現(xiàn)了大量新的可約構(gòu)形,而且這些構(gòu)形比肯普所發(fā)現(xiàn)的要大得多。盡管如此,它們?nèi)匀徊蛔阋孕纬梢粋€(gè)不可避免集。在這種搜集可約構(gòu)形以形成一個(gè)不可避免集的道路上,四色問(wèn)題進(jìn)展很慢。那個(gè)時(shí)候,一些人開始認(rèn)識(shí)到困難仍出在肯普未能證明的(ⅳ),具體說(shuō)就是(ⅳ)分得還不夠細(xì)。希什首要的技術(shù)貢獻(xiàn)是他猜測(cè)存在一個(gè)有限的可約構(gòu)形的不可避免集。1950年,他指出,不僅可以找到這樣一組不可避免集,而且其中構(gòu)形的個(gè)數(shù)應(yīng)有一個(gè)上限——約1萬(wàn)!也就是要把情況分細(xì)到可以證明的地步,大約要分1萬(wàn)種情況才行!阿佩爾和哈肯在宣布他們的主要結(jié)論之前,就特別指出:“我們的工作受到了希什,研究四色問(wèn)題的啟發(fā),特別是他猜想[1969,11頁(yè),216頁(yè)]存在一個(gè)可4色的可約構(gòu)形的有限集合S,使得每一個(gè)可平面圖至少包含S中的一個(gè)構(gòu)形……1970年,希什還得到了一個(gè)未發(fā)表的結(jié)論……他稱之為四色問(wèn)題的有限化?！毕Ｊ策€是繼肯普之后第一位公開宣稱四色問(wèn)題能夠通過(guò)尋找可約構(gòu)形的不可避免集來(lái)證明的數(shù)學(xué)家。他在前人工作的基礎(chǔ)上大大發(fā)展了可約構(gòu)形理論,提出了構(gòu)造可約構(gòu)形不可避免集的更為普遍的方法,其主要思想就是確定一個(gè)具有下述性質(zhì)的構(gòu)形集合S:首先,每一個(gè)平面圖必定包含S中某一構(gòu)形;其次,假定平面圖包含S中某一構(gòu)形且其余部分可用至多4種顏色著色,那么通過(guò)調(diào)整著色的方式就能擴(kuò)展到整個(gè)平面圖上來(lái)。他關(guān)于A-可約、B-可約、C-可約、D-可約構(gòu)形的概念是由伯克霍夫等人的工作發(fā)展而來(lái)的。希什還是第一位使用計(jì)算機(jī)研究四色問(wèn)題的數(shù)學(xué)家。他知道把證明構(gòu)形可約性的現(xiàn)有方法形式化:他觀察到其中至少有一種方法(是對(duì)肯普所用方法的直接推廣)在原則上是計(jì)算機(jī)所能做的純機(jī)械過(guò)程。1969年,希什發(fā)明了一種放電法,用來(lái)尋找構(gòu)形的不可避免集。如果一個(gè)圖不可四色,那么它必定存在某個(gè)局部障礙。放電的目的就是把這些局部障礙列一個(gè)清單出來(lái),而這些局部障礙實(shí)際上恰是肯普所謂的“不可避免的構(gòu)形”。希什的這項(xiàng)成就為計(jì)算機(jī)輔助尋找可約構(gòu)形鋪平了道路。此外,值得一提的是,希什對(duì)哈肯個(gè)人也有很大幫助和影響,他將自己許多未發(fā)表的思想都介紹給了哈肯。1972年,阿佩爾開始與哈肯合作。與希什一樣,他們也意識(shí)到離開計(jì)算機(jī)的輔助是不行的。但比希什英明的是,他們充分考慮了檢驗(yàn)可約性所需機(jī)時(shí)和存儲(chǔ)空間問(wèn)題。這樣,他們一方面在希什約化理論的基礎(chǔ)上繼續(xù)簡(jiǎn)化問(wèn)題,另一方面利用計(jì)算機(jī)的試算以及人機(jī)對(duì)話獲得有益的信息,其目的是希望進(jìn)一步縮減不可避免集中構(gòu)形的個(gè)數(shù),使證明可約性所需時(shí)間和空間降到可以接受的程度。1976年初,阿佩爾和哈肯找到了一種新的放電程序,構(gòu)造了一個(gè)含有1936個(gè)構(gòu)形的不可避免集。為驗(yàn)證這些構(gòu)形的可約性,他們一方面修改科赫(J.Koch)的可約性程序,一方面利用伯克霍夫的更一般性的約減步驟改進(jìn)程序,最終在IBM360計(jì)算機(jī)上耗費(fèi)1200小時(shí)驗(yàn)證了構(gòu)形的可約性。1976年6月,他們?cè)凇睹绹?guó)數(shù)學(xué)會(huì)通報(bào)》上宣布證明了四色定理1。第二年,《伊利諾斯數(shù)學(xué)雜志》刊出他們的論文“每個(gè)平面地圖都可四色”,。全文長(zhǎng)達(dá)139頁(yè),另附有計(jì)算機(jī)程序的微縮膠片400頁(yè),共分兩個(gè)部分:第Ⅰ部分“放電”,描述了用來(lái)構(gòu)造不可避免集的放電方法,給出了證明的全部策略;第Ⅱ部分“可約性”,刻畫了計(jì)算機(jī)程序的實(shí)現(xiàn)過(guò)程,并列出了1482個(gè)可約構(gòu)形的不可避免集2。2.阿佩爾和哈肯的證明b對(duì)計(jì)算機(jī)實(shí)驗(yàn)的初步證明阿佩爾和哈肯的工作意義已經(jīng)超過(guò)了證明一個(gè)數(shù)學(xué)難題本身,它告訴人們計(jì)算機(jī)不僅可以用來(lái)計(jì)算,還能用于數(shù)學(xué)的邏輯證明。然而他們的方法本質(zhì)上是一種窮舉檢驗(yàn)法,令人滿意的答復(fù)絕不是由于“檢驗(yàn)了千百萬(wàn)種情況,且它們都對(duì)”。這種史無(wú)前例地使用計(jì)算機(jī)輔助證明的做法成了爭(zhēng)論的焦點(diǎn)!哲學(xué)家提莫志克(A.T.Tymoczko,1943-1996)是懷疑論者的一位代表。他認(rèn)為一個(gè)證明至少應(yīng)具備以下三個(gè)特征:“(a)有說(shuō)服力(convincing);(b)可被檢查(surveyable);(c)可被形式化(formalizable)”。他認(rèn)為阿佩爾和哈肯的證明不滿足(b),理由是證明細(xì)節(jié)隱藏在計(jì)算機(jī)內(nèi),沒(méi)有誰(shuí)能夠?qū)λM(jìn)行復(fù)核。他表示,如果數(shù)學(xué)允許使用計(jì)算機(jī)進(jìn)行“實(shí)驗(yàn)”,數(shù)學(xué)將會(huì)面臨走向經(jīng)驗(yàn)科學(xué)的危險(xiǎn)。如果承認(rèn)阿佩爾和哈肯的證明有效,那就是強(qiáng)迫大家改變“數(shù)學(xué)證明”的含義:將計(jì)算機(jī)實(shí)驗(yàn)視為確定數(shù)學(xué)結(jié)論的一種新方法。有關(guān)數(shù)學(xué)證明的探討詳見斯瓦特(T.Swart),戴維斯(P.J.Davis)和赫什(R.Hersh)以及羅塔(G-G.Rota,1932-1999)。懷疑論者除了抱怨證明不“可被檢查”外,還指出證明“不夠透明”。代表人物有著名數(shù)學(xué)作家、評(píng)論家斯圖爾特(LanStewart)以及數(shù)學(xué)家布朗(G.Spencer-Brown)。雪上加霜的是,20世紀(jì)80年代初開始傳言一代證明中出現(xiàn)了重要錯(cuò)誤,導(dǎo)致這種傳言的原因是人們誤解了施密特(U.Schmidt)復(fù)核證明時(shí)的一個(gè)結(jié)論。1985年,日本的佐伯(S.Saeki)也發(fā)現(xiàn)過(guò)一個(gè)構(gòu)形描述上的小錯(cuò)誤。不過(guò),幸好這些錯(cuò)誤并非本質(zhì)的,很快就得到了糾正。除此之外,不包括一些打印錯(cuò)誤,沒(méi)有再發(fā)現(xiàn)任何致命的錯(cuò)誤。1989年,阿佩爾和哈肯專門為四色定理的證明撰寫了一部專著——《每一個(gè)可平面圖是可四色的》。書中補(bǔ)充了證明的細(xì)節(jié),并修正了已發(fā)現(xiàn)的所有錯(cuò)誤,同時(shí)附上了所有縮微膠片的印刷版,整個(gè)證明長(zhǎng)達(dá)741頁(yè)。這是他們最后一次對(duì)四色定理證明的整理。盡管如此,一代證明的“兩大派別”依舊相持不下:一方面是懷疑論者,他們反對(duì)計(jì)算機(jī)輔助證明;另一方面是支持者,他們接受計(jì)算機(jī)向數(shù)學(xué)領(lǐng)域提供的巨大幫助。但無(wú)論哪一方,他們的評(píng)述都不是指向阿佩爾和哈肯本身,而是針對(duì)無(wú)法復(fù)核整個(gè)證明而言。簡(jiǎn)言之,一代證明無(wú)法單獨(dú)人力完成并進(jìn)行驗(yàn)證,因此還不能算作一個(gè)完美的數(shù)學(xué)證明。三、數(shù)學(xué)證明的興起1976年,阿貝爾和哈肯雖然使用計(jì)算機(jī)輔助證明了四色定理,但是他們的證明并未獲得普遍認(rèn)可,主要原因有二:一是使用計(jì)算機(jī)的部分無(wú)法用手算核實(shí);二是應(yīng)該用手算核實(shí)的部分因過(guò)于繁瑣,無(wú)人能夠獨(dú)立完成。這些不太令人滿意的地方導(dǎo)致人們對(duì)定理的真實(shí)性持以懷疑態(tài)度,甚至上升到了對(duì)數(shù)學(xué)證明含義的哲學(xué)探討?？杀氖?時(shí)至今日,很多人卻以為就只有這么一代證明!事實(shí)上,第一代證明以后,數(shù)學(xué)家們并沒(méi)有放棄尋求嚴(yán)格的數(shù)學(xué)證明,也因此推動(dòng)了圖論整個(gè)學(xué)科的發(fā)展,使得這門學(xué)科中大多數(shù)問(wèn)題都與染色問(wèn)題有關(guān)。20世紀(jì)80、90年代,羅伯遜、西繆爾、桑德斯和托馬斯一直致力于研究染色問(wèn)題,取得了大量驚人的結(jié)果。1994年,西繆爾等四人宣布得到了一種更為簡(jiǎn)化的證明。他們以阿佩爾和哈肯的證明為基礎(chǔ),做出了屬于他們自己的證明。這代證明不僅證實(shí)了阿佩爾和哈肯的方法能夠證明四色定理,而且澄清了長(zhǎng)期以來(lái)人們對(duì)四色定理真實(shí)性的種種置疑,肯定了它的正確性。1.對(duì)錯(cuò)誤證明的審查1994年,西繆爾在瑞士蘇黎世召開的國(guó)際數(shù)學(xué)家大會(huì)上宣布,他和另外三位數(shù)學(xué)家對(duì)阿佩爾和哈肯的證明進(jìn)行了修正。會(huì)上,西繆爾肯定了阿佩爾、哈肯的巨大成就,同時(shí)指出了造成如此大非議的主要原因。為驗(yàn)證定理的正確性,西繆爾等四位數(shù)學(xué)家原打算復(fù)核證明,但進(jìn)行了大約一周以后,他們就放棄了。因?yàn)檫@種做法比給出新證明還要困難。西繆爾說(shuō):“我們決定用阿佩爾和哈肯的方法做出我們自己的證明,細(xì)節(jié)是屬于我們自己的創(chuàng)新,這樣做可能更容易,也更有意義?！?,p.184)于是就出現(xiàn)了所謂的第二代證明,這二代證明實(shí)際上是對(duì)一代證明的修正。2.可約性的證明a和b西繆爾等人證明四色定理的基本思想與阿佩爾、哈肯的大致相同。但為了避免陷入阿佩爾和哈肯的復(fù)雜論證,他們事先證明了希什關(guān)于不可避免性的一個(gè)猜想。進(jìn)而,他們盡量“簡(jiǎn)化了”整個(gè)證明過(guò)程。與一代證明相比,這種簡(jiǎn)化體現(xiàn)在:(a)使可約構(gòu)形的不可避免集盡可能小。(b)使放電法則的數(shù)目盡可能少。(c)使計(jì)算機(jī)程序的運(yùn)行時(shí)間盡可能短。(d)使證明的非計(jì)算機(jī)部分(即寫在紙上的那些)盡可能簡(jiǎn)單。但遺憾的是這些目標(biāo)有的相互沖突。例如,可以把兩個(gè)或多個(gè)法則替換為一個(gè)法則,但要以增加不可避免集中構(gòu)形的個(gè)數(shù)為代價(jià)。這種矛盾迫使他們必須對(duì)(a)和(b)做折中考慮。除此之外,他們還遇到了需“付出更高代價(jià)”的地方,即選擇可約性的證明方法。(,pp.24-25)盡管這有點(diǎn)像修正主義,但他們的努力終究沒(méi)有白費(fèi)。1995年5月25日,西繆爾等人將修正后的證明提交給了《組合學(xué)雜志》(B輯)。1997年正式發(fā)表出來(lái)。它成為四色定理的第二代證明。這個(gè)證明只有43頁(yè),較長(zhǎng)達(dá)741頁(yè)的第一代證明而言,二代證明的確簡(jiǎn)化了不少:放電法則從486個(gè)減至20個(gè);不可避免構(gòu)形從1482個(gè)減至633個(gè);圖著色算法由4次時(shí)間算法優(yōu)化為2次時(shí)間算法;證明所需機(jī)時(shí)由1200小時(shí)縮短到24小時(shí);而且第二代證明達(dá)到了人工復(fù)核的要求;如果用計(jì)算機(jī)驗(yàn)證,只需5分鐘就能完成!更重要的是,第二代證明已經(jīng)沒(méi)有第一代證明的缺點(diǎn),也就是第二代證明已經(jīng)完全沒(méi)有第一代證明中只有計(jì)算機(jī)才能完成的驗(yàn)證過(guò)程。換言之,第二代盡管也要用計(jì)算機(jī),但這種證明對(duì)人來(lái)講是更透明的,每一步都可以轉(zhuǎn)換成人可理解的證明,雖然它還不完全是一個(gè)標(biāo)準(zhǔn)的數(shù)學(xué)證明。時(shí)至今日,四色問(wèn)題還沒(méi)有一個(gè)通常意義下的數(shù)學(xué)證明。四、數(shù)學(xué)定理的形式證明盡管二代證明肯定了一代證明的有效性,但這前兩代證明中仍然存在一些不盡人如意的地方。2005年,也就是西繆爾的二代證明宣布十年之后,英國(guó)劍橋研究院的高級(jí)研究員貢蒂埃成功給出四色定理的第三代證明。這第三代證明并非數(shù)學(xué)證明,而是所謂的形式證明(formalproof)。對(duì)于一個(gè)定理,有了形式證明同有了數(shù)學(xué)證明一樣,是一條被證明的定理。更確切來(lái)講,有了形式證明的定理獲得了更強(qiáng)的支持,因?yàn)榇蠖鄶?shù)數(shù)學(xué)定理只有數(shù)學(xué)證明而沒(méi)有形式證明,反過(guò)來(lái),一個(gè)有形式證明的定理必定是建立在更廣意義上的數(shù)學(xué)證明(即包括通常意義下的數(shù)學(xué)證明,也包括計(jì)算機(jī)協(xié)助下的數(shù)學(xué)證明)基礎(chǔ)上的。從這個(gè)意義上來(lái)講,形式證明的提法對(duì)數(shù)學(xué)和計(jì)算機(jī)科學(xué)有著十分重要的意義,特別是:(1)它強(qiáng)烈肯定四色定理的確是一個(gè)定理。(2)對(duì)于大量的、已有數(shù)學(xué)證明的數(shù)學(xué)定理,如何找出一個(gè)形式證明,這給數(shù)學(xué)家與計(jì)算機(jī)科學(xué)家提供了一個(gè)新的、廣闊的研究領(lǐng)域。對(duì)于十分繁復(fù)的數(shù)學(xué)證明,如何設(shè)計(jì)計(jì)算機(jī)程序來(lái)驗(yàn)證它是否正確?從數(shù)學(xué)發(fā)展來(lái)看,幾十頁(yè)上百頁(yè)的證明已經(jīng)司空見慣。華裔數(shù)學(xué)家陶哲軒在從組合學(xué)、數(shù)論到調(diào)和分析、偏微分方程到數(shù)理統(tǒng)計(jì)等七、八個(gè)領(lǐng)域已發(fā)表200多篇論文,每篇都超過(guò)50頁(yè)。單群分類的定理幾千頁(yè);幾何測(cè)度論的大定理1728頁(yè)。這就使某些人置疑數(shù)學(xué)定理乃至大多數(shù)數(shù)學(xué)家的工作。因此,這種程序是極為重要的。數(shù)學(xué)發(fā)展必然要走向全盤自動(dòng)化,特別是其中可機(jī)械化的工作。中國(guó)數(shù)學(xué)家吳文俊在這方面開了一個(gè)頭。但形式化證明是另一個(gè)發(fā)展方向。形式化證明,簡(jiǎn)單說(shuō),就是完全符號(hào)化,把所有邏輯步驟都寫出來(lái)的證明,這樣,它比通常證明要長(zhǎng)上幾十倍甚至幾百倍,而且都是用符號(hào)表示出來(lái),通過(guò)推理規(guī)則來(lái)推理。通常的數(shù)學(xué)證明使用公理化,概念都有明確的定義。形式證明不僅包括這些,而且包括符號(hào)串,構(gòu)成規(guī)則、推演規(guī)則以及邏輯公理,這些我們稱之為形式化過(guò)程。由于形式化過(guò)程十分繁瑣,形式證明只在50年前才開始嶄露頭角。形式證明的元年恰巧是四色定理形式證明前50年——1954年。這一年,數(shù)學(xué)家M.戴維斯(M.Davis)用普林斯頓高等研究院的馮·諾伊曼(J.vonNeumann,1903-1957)主持研制的計(jì)算機(jī)(Johniac)證明一個(gè)平凡的數(shù)學(xué)定理,偶數(shù)加偶數(shù)是偶數(shù)。五年之后,王浩取得突破,證明羅素(B.Russell,1872-1970)、懷特海(A.N.Whitehead,1861-1947)的名著《數(shù)學(xué)原理》中幾百條數(shù)理邏輯的定理。當(dāng)然,數(shù)理邏輯的定理易于證明在于它已經(jīng)充分形式化。1968年荷蘭數(shù)學(xué)家布呂言(N.G.deBruijn,1918-)設(shè)計(jì)了第一個(gè)驗(yàn)證數(shù)學(xué)證明正確性的計(jì)算機(jī)程序,并用來(lái)驗(yàn)證一些數(shù)論的命題。其后通過(guò)形式化,證明一些簡(jiǎn)單的數(shù)學(xué)定理,如微積分基本定理、代數(shù)基本定理、二次互反律等。這里我們還應(yīng)該提到1986年形式證明數(shù)理邏輯的大定理——哥德爾(K.G?del,1906-1978)第一不完全性定理。對(duì)于數(shù)學(xué)定理形式證明的真正突破是2004年貢蒂埃形式證明四色定理。他的思路分成兩部分:首先是寫下西繆爾的證明的形式部分,其次還要寫下另一個(gè)不同的程序來(lái)驗(yàn)證上述證明是正確的。主要困難在于,即使語(yǔ)言足夠豐富,也很難產(chǎn)生出形式證明。這正好是第三代證明的創(chuàng)新所在。為了克服這個(gè)困難,數(shù)學(xué)家不僅僅注意局部的明顯性與正確性,而且還必須對(duì)整體證明的結(jié)構(gòu)有足夠清楚認(rèn)識(shí),而這正是數(shù)學(xué)家的眼光。他必須能夠發(fā)現(xiàn)結(jié)構(gòu)的對(duì)稱性、能夠簡(jiǎn)化、能夠推廣,而這是計(jì)算機(jī)做不到的。因此,通過(guò)數(shù)學(xué)證明的定理很多仍然沒(méi)有形式證明,這也正是形式證明必須要有數(shù)學(xué)家的創(chuàng)新之處。從某種意義上來(lái)講,這不僅僅是一個(gè)形式化過(guò)程,更是一個(gè)新的程序設(shè)計(jì),同時(shí)還要有自己的或新的驗(yàn)證程序來(lái)驗(yàn)證它正確。這樣形式證明才得以完成。第三代證明的有效性是由不同程序進(jìn)行復(fù)核的客觀數(shù)學(xué)事實(shí),而程序本身的正確性可以通過(guò)運(yùn)行多種輸入程序憑實(shí)驗(yàn)確定。貢蒂埃認(rèn)為他的成功可