關(guān)于作者
計(jì)算機(jī)證明（3）
張建中
2013年05月08日四色猜想、費(fèi)馬猜想和歌德巴赫猜想，通常被稱為世界三大數(shù)學(xué)猜想，也是世界三大數(shù)學(xué)難題。
四色猜想于1976年由美國數(shù)學(xué)家阿佩爾(Kenneth Appel)與哈肯(Wolfgang Haken)借助計(jì)算機(jī)完成了證明，遂稱四色定理；費(fèi)馬猜想于1994年由英國數(shù)學(xué)家安德魯 懷爾斯（Andrew Wiles）完成了證明，遂稱費(fèi)馬大定理；哥德巴赫猜想尚未解決，目前最好的成果是1966年由中國數(shù)學(xué)家陳景潤給出的（稱其為陳氏定理：任何一個大于6的偶數(shù)，都可以表示成一個素?cái)?shù)及兩個素?cái)?shù)乘積之和，簡記為1+2），故歌德巴赫猜想還不能稱為哥德巴赫定理(1+1)。這三個問題的共同點(diǎn)就是說起來簡單易懂，但內(nèi)涵深邃無比，困擾了一代代全球的數(shù)學(xué)家。
1852年，英國青年古色里（Francis Guthrie）提出了四色問題猜想：對平面或球面上的任意一個地圖著色，至多用四種顏色就可以使相鄰（即有一段公共邊界而不是一點(diǎn)或有限點(diǎn)）兩個國家或地區(qū)（這里所謂的“國家”或地區(qū)是指連通的區(qū)域）的顏色不同。在這里，古色里提出的問題是“任意的地圖”，它不僅是全世界所有的可能的地圖，也包括可以想象的地圖，因而四色猜想的證明，需要給出對所有情況都適用的證明。用數(shù)學(xué)語言表示這一問題，則是“將平面任意地細(xì)分為不相重疊的區(qū)域，每一個區(qū)域總可以用1、2、3、4這四個數(shù)字之一來標(biāo)記，而不會使相鄰的兩個區(qū)域有相同的數(shù)字?！?
四色定理示意圖
1872年，英國當(dāng)時最著名的數(shù)學(xué)家凱利正式向倫敦?cái)?shù)學(xué)學(xué)會提出了這個問題，于是四色猜想成了世界數(shù)學(xué)界關(guān)注的問題，世界上許多一流的數(shù)學(xué)家都紛紛參加了四色猜想的大會戰(zhàn)。1878～1880年兩年間，著名的律師兼數(shù)學(xué)家肯普和泰勒兩人分別提交了證明四色猜想的論文，宣布證明了四色定理，大家都認(rèn)為四色猜想從此也就解決了，但被后人檢查出漏洞。經(jīng)過人們的補(bǔ)救，肯普的方法可以證明“五色定理”。在證明過程中，肯普引入了圖形可約性的概念及其檢驗(yàn)方法，經(jīng)過后人的推廣，成為最后解決四色猜想的有力武器。后來，越來越多的數(shù)學(xué)家雖然為此絞盡腦汁，但一無所獲。于是，人們開始認(rèn)識到，這個貌似容易的題目，其實(shí)是一個可與費(fèi)馬猜想相媲美的難題。
進(jìn)入20世紀(jì)，科學(xué)家們對四色猜想的證明基本上是按照肯普的想法進(jìn)行的。1913年，伯克霍夫在肯普的基礎(chǔ)上引進(jìn)了一些新技巧，美國數(shù)學(xué)家富蘭克林于1939年證明了22國以下的地圖都可以用四色著色。1950年，有人從22國推進(jìn)到35國，德國數(shù)學(xué)家希爾創(chuàng)建了“放電法”，為四色猜想的計(jì)算機(jī)證明奠定了基礎(chǔ)。1960年，有人又證明了39國以下的地圖可以只用四種顏色著色；隨后又推進(jìn)到了50國?？磥磉@種推進(jìn)仍然十分緩慢。電子計(jì)算機(jī)問世以后，由于演算速度迅速提高，加之人機(jī)對話的出現(xiàn)，大大加快了對四色猜想證明的進(jìn)程。1970年左右，問題歸結(jié)為計(jì)算幾千個不可約構(gòu)形的問題，但其計(jì)算量之大是難以想像的，因此人們?nèi)酝贰?/p> 1975年，美國伊利諾思大學(xué)數(shù)學(xué)教授阿佩爾（K.Appel）與哈肯（W.Haken）多次改進(jìn)自己的實(shí)驗(yàn)設(shè)計(jì)，開始對四色猜想進(jìn)行計(jì)算機(jī)證明。他們發(fā)展了一種放電過程，以便產(chǎn)生由可約構(gòu)形組成不可避免集，還編寫了證明可約性的程序。1976年，阿佩爾與哈肯在美國伊利諾斯大學(xué)的兩臺不同的電子計(jì)算機(jī)上，用了1200多個小時，作了100多億次判斷，分析了兩千多個構(gòu)形的可約性，并通過人工分析了約一萬個帶正電頂點(diǎn)的鄰近區(qū)域，終于用不可避免組的方法證明了四色問題，完成了四色定理的證明。四色猜想的計(jì)算機(jī)證明，轟動了世界，它不僅解決了一個歷時一百多年的難題，而且有可能成為數(shù)學(xué)史上一系列新思維的起點(diǎn)。當(dāng)兩位數(shù)學(xué)家將他們的研究成果發(fā)表時，當(dāng)?shù)氐男欧馍仙w“Four colors suffice”（四色足夠）的郵戳，以慶祝這一難題獲得解決。
阿佩爾與哈肯的證明方法是將地圖上的無限種可能情況減少為1936種狀態(tài)（稍后減少為1476種），這些狀態(tài)由計(jì)算機(jī)一個挨一個的進(jìn)行檢查。這一工作又由不同的程序和計(jì)算機(jī)獨(dú)立的進(jìn)行了復(fù)檢。1996年，Neil Robertson、Daniel Sanders、Paul Seymour和Robin Thomas使用了一種類似的證明方法，檢查了633種特殊的情況。這一新證明也使用了計(jì)算機(jī)，如果由人工來檢查的話是不切實(shí)際的。
“四色問題”的證明不僅解決了一個歷時一百多年的難題，而且成為數(shù)學(xué)史上一系列新思維的起點(diǎn)。它表明，靠人與機(jī)器合作，有可能完成連最著名的數(shù)學(xué)家至今也束手無策的工作，標(biāo)志著人類認(rèn)識能力的一個飛躍，極大地推動了以計(jì)算機(jī)為基礎(chǔ)的人工智能的發(fā)展。在“四色問題”的研究過程中，不少新的數(shù)學(xué)理論隨之產(chǎn)生，也發(fā)展了很多數(shù)學(xué)計(jì)算技巧。如將地圖的著色問題化為圖論問題，豐富了圖論的內(nèi)容。不僅如此，“四色問題”在有效地設(shè)計(jì)航空班機(jī)日程表，設(shè)計(jì)計(jì)算機(jī)的編碼程序上都起到了推動作用。不過不少數(shù)學(xué)家并不滿足于計(jì)算機(jī)取得的成就，他們認(rèn)為應(yīng)該有一種簡捷明快的書面證明方法。直到現(xiàn)在，仍有不少數(shù)學(xué)家和數(shù)學(xué)愛好者在尋找更簡潔的證明方法。
四色定理是第一個主要由計(jì)算機(jī)證明的定理，這一證明并不被所有的數(shù)學(xué)家接受，因?yàn)樗荒苡扇斯ぶ苯域?yàn)證。最終，人們必須對計(jì)算機(jī)程序的正確性以及運(yùn)行這一程序的硬件設(shè)備充分信任。首先，他們的“證明”，計(jì)算機(jī)程序就達(dá)400多頁，要用人工去檢驗(yàn)其程序有無問題是十分吃力的。因此，似乎無人愿意再去重復(fù)阿－哈的“證明”。其次，能否保證計(jì)算機(jī)在計(jì)算過程中絕對不出錯誤？第三，人們無法確定計(jì)算出現(xiàn)錯誤是計(jì)算機(jī)本身的機(jī)械或電子方面的毛病，還是“證明”過程本身邏輯有問題。缺乏數(shù)學(xué)應(yīng)有的規(guī)范成了另一個方面；以至于有人這樣評論“一個好的數(shù)學(xué)證明應(yīng)當(dāng)像一首詩——而這純粹是一本電話簿！”于是就引起了什么是“數(shù)學(xué)證明”的爭論。
有些數(shù)學(xué)家認(rèn)為數(shù)學(xué)證明只能是以人工可重復(fù)檢驗(yàn)的邏輯演繹(計(jì)算也是一種演繹)過程，否則只能稱為計(jì)算機(jī)證明，二者不能混為一談。因此，按這種觀點(diǎn)，“四色問題”只能稱已得到了計(jì)算機(jī)證明，而不能稱已得到了數(shù)學(xué)證明。但是，另一些數(shù)學(xué)家反駁說，用人工來檢驗(yàn)也可能產(chǎn)生錯誤。例如，數(shù)學(xué)史上曾有不少數(shù)學(xué)家(如意大利的Saccheri，法國的Legendre)聲稱他們已“證明”了歐幾里得第五公設(shè)(即歐氏平行公理)。但后來發(fā)現(xiàn)他們的“證明”均有問題，其主要錯誤在于他們利用了與第五公設(shè)等價的命題，因此從邏輯上說他們都犯了循環(huán)論證的錯誤。
另外人工邏輯演繹證明可以重復(fù)嗎？眾所周知，群論中有一個著名的所謂有限單群的分類定理，單群的概念是由伽羅華 (Galois)在1830年最初給出的。一百多年來數(shù)學(xué)家企圖對單群進(jìn)行分類，直至20世紀(jì)80年代，由100多位數(shù)學(xué)家組成的非正規(guī)“隊(duì)伍”，他們共同努力列出所有的單群并證明這樣的列舉是完全的。在花費(fèi)了成千上萬個小時以及發(fā)表了幾百篇論文之后，這項(xiàng)工作才得以完成，證明長達(dá)15000多頁!試問誰還愿意(或說可能)去重復(fù)他們長達(dá)15000多頁的證明?
2005 年，Gonthier 建立了四色定理的全部計(jì)算機(jī)化證明。這一證明和阿佩爾的證明雖然都用到了計(jì)算機(jī)，但是其意義則根本不同。阿佩爾的證明本質(zhì)上仍然是傳統(tǒng)證明，計(jì)算機(jī)只是起到了輔助計(jì)算的作用，而 Gonthier 的證明則是純粹的計(jì)算機(jī)證明，其每一步邏輯推導(dǎo)都是由計(jì)算機(jī)完成的。
雖然四色定理證明了任何地圖可以只用四個顏色著色，但是這個結(jié)論對于現(xiàn)實(shí)上的應(yīng)用卻相當(dāng)有限?，F(xiàn)實(shí)中的地圖常會出現(xiàn)飛地，即兩個不連通的區(qū)域?qū)儆谕粋€國家的情況（如美國的阿拉斯加州），而制作地圖時我們?nèi)詴筮@兩個區(qū)域被涂上同樣的顏色，在這種情況下，四個顏色將會是不夠用的。
四種顏色染色的中國大陸分省地圖