什麼是數學證明？四色猜想的證明為何震動了整個數學界？

關于是否會存在定理證明 機 ，在理論上人們是有過不同的看法的。有些人認為不可能，如著名數學家龐加萊；而有些人卻覺得是可能的，并從理論上進行了論證，如著名的數理邏輯學家塔爾斯基。同時他還指出初等代數和初等幾何範圍的定理證明是可以實現機械化的。而在希爾伯特的《幾何基礎》中，也已經蘊涵了“萬理一證”的定理證明機械化思想，隻是由于物質條件的不成熟而計人把他的這個重要思想給忽視了。然而，本世紀初數理邏輯的創立，以及40年代電子計算機的出現卻複興了這一想法，并且使之成為現實。 本世紀 50 年代，在這方面做出先驅性工作的是數理邏輯學家王浩教授，他僅用幾分鐘的時間就在計算機上證明了羅素和懷特海合著的《數學原理》中的300多條定理。這件事情為從事人工智能研究的人們着實興奮了一陣，但是這一切技術性的工作并沒有太多地引起數學界人士關于計算機對數學影響的重視，因為計算機所做的也就是人工所做的翻版。 然而70年代以後，計算機在數學中的應用卻給數學界帶來了未曾料想的影響，它使得人們開始重新思考數學的本質問題。因為曾經困擾人們百年多的四色猜想在計算機上得到了證明，而且它的證明過程是人工無法檢驗的；而以大自然中具有 自 相似形狀的物體為研究對象的分形幾何，更是計算機下的産物。事實上，越來越多的數學問題的解決需要計算機的幫助，甚至是必須的。所有這些事實與人們從 19 世紀所接取過來的豐碩成果是這樣不同，于是自然地就引起了人們對數學哲學問題的思考和讨論。 理論上的争論‍‍‍‍‍ 縱觀曆史的發展，人們 想 把推理機械化的思想很早以前就有，如柏拉圖、萊布尼茨、霍布斯、笛卡爾等等。而在近代，著名的德國數學大師希爾伯特在1899年出版的經典名著《幾何基礎》中，就已經指出了幾何定理可以 不是 逐一證明，而是一類定理可以用統一的方法一起證明。其大緻的方向是從公理化出發，通過代數化而達到機械化。隻是由于當時數學研究仍處于手工作坊時代，這個重要的機械化方向和意義沒有被數學家們及時地認識到。其實連希爾伯特自己也沒有明确地意識到。

• 希爾伯特

到了本世紀初，數理邏輯的發展為推理過程的機械化提供了基礎。無論命題演算還是謂詞演算都建立了公理系統，這就使得推理過程形式化。于是從一些很簡單明白的公理出發，使用一些很簡單的機械推理規則，便可一步一步地把人們日常使用的、乃至數學中所使用的極複雜的推理規則推導出來。換句話說，人們日常使用的極複雜的推理規則，可以 化 歸為一些簡單的、機械的推理動作。最終的這些推理動作是這樣的簡單，以至于機械也可以實現，數理邏輯的成果讓人們認識到，可利用機器來部分地代替人類頭腦進行思維，正如可以利用機器來代替人類的體力勞動一樣。 這種對推理過程認識的深化，自然地就導緻有些數理邏輯學家提出關于定理證明 機 的想法。即∶有可能制造出一種機器以代替人類思維，代替人類進行推理。但是也有人反對，最有代表性的如當時一代數學大師龐加萊就對這個想法大加責難，還帶有諷刺般地說： 現在已經有屠宰機器，當 把 牲畜趕到機器的一端時，機器便把這些牲畜宰殺成罐頭，從另一端輸送出來；現在有人竟然想制造一部機器，當把定理的前件送到機器的一端後，便可以把定理的結論從機器的另一端輸送出來（或者公理、定義送到一端後，各式各樣的定理便從另一端輸送出來），這種想法是注定不可能實現的。 龐加萊的看法絕不僅僅是他一個人特有的想法，實際上是代表了當時數學界流行的、占統治地位的思想。試想一想，在這種想法流行的時候，特别還是那麼有聲望的大人物所反對的想法，人們還會想方設法制造電子計算機去實現定理證明嗎？ 然而随着數理邏輯對推理過程本質研究的漸漸被認識，反對制造定理證明機的人們在日益減少，而支持的人卻越來越多。本世紀50年代，塔爾斯基首先從理論上證明了∶在初等幾何以及初等代數的定理證明是可以機械化的。不過他給出的機械化方法過于繁複，在實踐中真正實現起來是相當困難的。正是因為這樣，所以他的結果給人以這樣一個感覺∶定理證明能機械化的設想是個例外，因為大部分初等幾何及初等代數以外的結果都是不能機械化的。另外，塔爾斯基還提出了制造證明機的設想。無疑這種理論上的闡明是重要的，就如圖靈從理論上證明電子數字計算機是可能的一樣，它讓人覺得自己的實踐和試驗不是盲目的。 科技的進步為人們的這些設想提供着物質基礎，終于人們制造出了證明定理的機器。 五十年代中期，美國開始利用計算機進行證明數學定理的嘗試。 1959年，王浩用計算機證明了羅素和懷特海所著的《數學原理》這一經典著作中的300 多條定理，一共隻用了9分鐘的機器時間。這件事在數學界（特别是數理邏輯界）引起了轟動。他所使用的方法就是羅素和懷特海的技術，因為在《數學原理》中有許多标準的技巧是可以很快地變為機械的手續。接着J.A.Robinson發展了并使之成為一種标準的方法。這個結果就導緻許多人對定理機器證明的前途看好，甚至有人還在1958年做出預測說，在10年之内計算機将發現并證明一個重要的數學新定理。也有人設想，前人像皮亞諾、懷特海、羅素、希爾伯特以及圖靈等的夢想都将實現，然而事情的進展并沒有人們預想的那樣順利，不過随着時間的推移，這些設想終究成為了現實。 首先是20世紀70年代，美國的數學家阿佩爾和黑肯借助于計算機證明了著名的四色猜想，震動了數學界。它标志着計算機證明數學定理有着很好的 前景 。盡管如王浩先生的說法，四色猜想的證明是一種使用計算機的特例機證，但是它是一個 由 人沒有能夠解決的數學問題。而且它的證明又非傳統上的形式，于是就引起了人們繼數學基礎研究、希爾伯特探讨數學證明之後的又一次對數學證明的思考：什麼是數學證明？ 而上世紀70年代，在國際上掀起的一股研究以"非"字當頭的科學中，由曼德布羅特創立的分形幾何學，更是得力于計算機的強大功能。計算機在這裡并不是證明定理，而是幫助人們提出猜想，引發思考。我們當如何看待這門學科呢？有人認為它不是數學。但也有更多的人認為它是一門數學學科，特别是物理學家，因為分形幾何正在成為研究大自然中許多複雜現象的有力工具。雙方争執的焦點是"什麼是數學"這個基本的數學哲學問題。 四色猜想證明的曆史‍‍‍‍‍ 1976年1月，困擾了無數智者100多年的四色猜想由人機合作終于獲得了解決。面對這一事實，有人帶着些驚喜、有人帶着些遺憾、也有人帶着些懷疑，畢竟它不是數學家們所希望的那種傳統演繹證明定理的方式。 四色問題‍
四色問題是一個屬于拓撲學的問題，它的粗略描述可以追溯到1840 年。當時數學家莫比烏斯在給學生的講課中提到。在平面上很容易指出四個區域，其中每兩個區域都有一個公共的邊界線，并要求學生證明：在平面上決不可能指出五個區域都具有上述性質。從這個論斷的證明中，可得出莫比烏斯假設∶平面或球面上的每張地圖都可以用四種顔色來着色。 明确提出四色問題的是倫敦大學學院畢業不久的學生弗朗塞斯·古斯裡（1852）。他在一封給他兄弟弗雷 贅 克的信中說∶ 看來，每幅地圖都可以隻用四種顔色着色，使得有共同邊界的國家着上不同的顔色。 這是原始四色問題的描述。由于他的兄弟無法解決，所以就這個問題的證明去請教他的老師——英國著名的數學家、邏輯學家德·摩根，據說德·摩根當天就寫了封信給當時正在英國三一學院執教的著名數學家、物理學家哈密頓。然而這兩位數學家實際上都沒有能夠解決這個看上去非常簡單的問題。 後來英國著名的數學家凱萊于1878年倫敦數學家會議上正式公布了這個問題。他呼籲與會者去解決這一問題。就這樣，和費馬大定理一樣，這個表面 看似 明易懂，其實很奇特的問題進入了數學家的圈子。從此受到了數學界人士的普遍重視以及數學愛好者們的興趣。以後，宣布證明了四色問題的聲明源源不斷，可是一經檢查，總是有或大或小的、難以彌補的缺陷。 在衆多聲稱證明了這一論斷的解答中，最值得一提的是1879年有一位名叫肯普的會員（同時也是律師）提交的一篇論文。凱萊和當時其他的一些數學家檢查後确定證明是正确的。誰知過了10年，也即在1890年，年僅 29歲的英國數學家希伍德在證明中 卻 發現了漏洞。這樣，四色猜想依然固我，沒有被解決。直到如今才借助于計算機給予解 快 。 肯普的證明是有 錯誤 ，然而他的證明思路非常有價值。因為一方面 20 世紀的人們正是沿着他的證明思路，逐漸改進而借助于計算機最終解決了四色問題；另一方面，希伍德在肯普方法的基礎上還證明了"五色定理"，特别是對歐拉示性數為K時的曲面上的地圖着色數P_k給出了上界： 四色問題的解決‍ 前面已經提及，肯普的證明有錯誤，但包含了許多天才的思想。 肯普是采用反證法證明四色猜想的，具體思路是∶ 如果有需要五種顔色的地圖，則此種地圖中必定有一個最小的，也就是在需要五種顔色的地圖中有一個區域數目是最少的（這種地圖稱為最小五色地圖）。于是隻要證明這種最小的地圖是不存在的，問題就可以獲得解決。因為假如給定了這樣的一種地圖，最後總能夠對它進行"歸約"而找到一種更小的地圖，而這幅地圖也需要五種顔色。為此，肯普先把問題轉化為隻研究一種所謂的正規地圖，在這種地圖中由有兩個鄰國、三個鄰國、四個鄰國及五個鄰國組成的一組構形是不可避免的，也即他需要證明總得有一個國家其鄰國數小于等于5。在這個條件下，肯普把上述論證又簡化成四條引理: （1）每一 地圖 都含有五個或五個以下鄰域的區域； （2）最小的五色地圖不可能含有恰好有兩個或恰好有三個鄰域的區域（因為如果那樣我們将能夠找到一個更小的需要五種顔色的地圖）； （3）同樣地，這樣的地圖不 可能 含有恰好有四個鄰域的區域； （4）這樣的地圖不可能含有恰好有五個鄰域的區域。 對這四種情況經過檢查看是否有"可約構形"出現，如果都有，矛盾就出現了。肯普對于引理1）一3）證明得很成功，但是在4）上卻失敗了。 20世紀的數學家們從肯普跌倒的地方開始了艱難的跋涉。 首先是美國數學家伯克霍夫。1913年他在肯普的基礎上引進了一些新技巧，這促進了富蘭克林于1939年證明22國以下的地圖都可以用四色着色；1950年溫（Winn）又把22國改進為35國；再接着是1968年奧爾（他是唯一的一本關于四色問題專著的作者）把數目提高到39國；1975 年又報道，對 52 國以下的地圖四色猜想都成立。從時間上可以看出，四色問題解決的進展是極其地緩慢。其中一個一直難以解決的困難，是肯普證明中關于五個鄰國時可約構形的判斷問題。具體地說是如何把 4）中的情況分得足夠細。 在四色問題的解決之路上，數學家H.希什也做出了很大的貢獻。他從1936 年就開始對四色問題進行研究，且始終堅信四色問題可以通過尋找可約構形的不可避免組得到解決。到1950年他從不斷的試驗中猜測，如果把情況分細到可以證明的地步，則這個組裡的構形可能需要大約一萬多種情況才行。要對如此多的構形逐一證明，工作量之大是非人力所能完成的。恰逢電子計算機在計算速度、精确度等方面都得到了驚人的進展，希什敏銳地意識到，若把證明構形可約的方法形式化，在理論上有一部分是可以通過計算機解決的。于是他很快就試着利用人機結合去解決，這也是早期人工智能的一種嘗試。 最初他與其學生是圍繞着怎樣用計算機檢查圖形是否可約構形進行的。盡管希什曾猜測可能要分一萬種情況，可是誰也不知道是否真得需要有一萬種，況且即使是對一種不太複雜的情況，若要檢查也要用上百個小時，而對較複雜的情況，無論是在時間上，還是在存儲上，計算機都不能承受。 美國伊利諾斯大學的黑肯教授在總結以往各種證法後指出，如果運用現有的一切數學方法，不可能給出四色猜想一個傳統上的證明，而在還沒有一個更強有力的計算機之前，能否給出一個計算機證明也是沒有把握的。就在這樣的信念下，黑肯對希什的方法作了重要的改進，接着是與阿佩爾合作着手研究四色問題。兩人一方面從理論上繼續簡化問題，另一方面又利用計算機的試算和人機對話。從中獲得有益的啟示。後來二人連手設計了一個能做出特殊類型放電過程的計算機程序，并經過上機不斷地反複試驗、不斷地修改，特别是在計算機專家科克的參與下，最後終于在1976年1月6日，由三人找到了一個合适的可行程序，證得了可約構形的不可避免組。于是百年來讓人們苦苦思索的這個叙述簡單明了的四色猜想，在IBM360機上運行達1200多小時後得到了證明。他們是利用"窮舉檢驗"法分情況檢查的，當時一共分了1482種情況，經查證它們都是可約構形。 四色猜想的證明是如此的繁複，盡管在 1977 年的一次數值數學與計算機會議上，有人又官布了一個相對簡單的證明，可是也要用50機時。所以它不像數學中上其它問題的證明，獲得數學家們的一緻贊揚，而是引起了許多的争議。 争議‍ 從四色猜想的解決過程可以看到，它是衆多數學家合作的結晶，是對曆史上智者探索的完善。阿佩爾等人是采用彙編語言編寫程序解決了四色問題、其程序之複雜到如今都還有人時不時地檢查出錯誤，雖然是不影響全局的；而且就目前的解決方法來看，其工作量之大是人力所永遠無法達到的。面對四色問題的這種複雜的、又是借助于計算機的證明，人們給以各種各樣的反應。正如國際上的數學家們所認為的，阿佩爾和黑肯等人的貢獻并不在于證明了四色問題，而在于借用電子計算機完成了這個至今人還沒有能夠解決的問題。但是，也有一些數學家反對四色猜想已經成為一個定理，于是自然地就引發一場争論。這場争論的焦點集中在計算機證明的可靠性和四色猜想的計算機證明是不是數學證明的問題。 關于機器證明的可靠性問題 反對四色定理的人認為∶如果一個定理不能用手工進行檢查，無法核實其證明是否可靠，就不能接受它是一個定理。計算機用了 1200個小時才證明了四色定理，這是用手工幾代人也無法檢查完的。事實上，在1961年，就有人聲稱借助于計算機找出了一個不可免完備集，其中的構形全是可約的（果然如此的話，四色猜想當然獲證）。但是，惠特尼和塔特卻各自獨立地發現，有一個構形的可約性被計算機誤算了，從而那個證明是錯誤的。事實上，自從黑肯和阿佩爾在 1976 年解決四色猜想之後，人們一直都在不斷地從證明中發現一些錯誤，慶幸的是這些錯誤都可以被修正而不影響證明的全局。但是誰也無法保證，有一天不會從中找出一個緻命的錯誤；機器中的硬件或軟件的錯誤。這就是機器證明的可靠性問題。 但是，贊成四色猜想是一個定理的人卻認為∶ 機器的可靠性主要是工程技術和物理學鑒定的事情，這是一門深奧的自然科學，它向我們保證，計算機的工作是可靠的，就象電子顯微鏡的工作是可靠的一樣。 美國著名數學家瑟斯頓在《數學的證明和進展》一文中談道： 實際上，一個可以運作的計算機程序，其正确性和完備性标準比起數學界關于可靠的證明的标準要高出幾個數量級。 關于四色猜想的計算機解決是不是數學證明的問題 不承認四色猜想的計算機解決是屬于數學證明的人認為，沒有一個數學家曾看到過四色猜想的證明，也沒有一個數學家看到過它的證明的證據，沒有數學家全面地驗證過四色猜想的證明。如著名蘇格蘭數學家波塞爾在其文章《切合實際的數學觀》一文中提到的： 如果這樣的一個問題（例如四色問題）利用某種聰明的新思想解決了，那是很了不起的。但是、如果解決的方法隻是一個現存方法的反複使用，那就隻能證明解決者的聰明罷了。如果解決的方法包括用計算機來證明特殊情況，那也是糟糕的，按我的觀點，這樣的解根本不屬于數學科學。 不加驗證地接受計算機給出的信息，還不如接受另一個數學家的告誡。事實上，例行公事似的編制程序十分乏味，極可能造成程序的錯誤。如果讓部分論證隐藏在計算機的鐵盒中，我們就不可能得到所認為的證明中的實質東西——我們自己對問題的了解。 1988年的紐約時報上還刊登了這樣一篇文章：《沒人能檢驗的證明算是數學證明嗎？》。 贊成者認為，機器證明是有可靠性問題，但是，有的數學定理被數學家證明了，但過了幾十年，人們又發現其證明是錯誤的，這說明人工證明也有一個可靠性問題。所以隻對機器證明提出可靠性問題是不公平的。 而另一方面，電子計算機正越來越多地介入到數學中的各個領域裡來。特别是近年在數學中的某些領域，有許多的問題如果不借助于大型的計算機，常常是無法解決的，如關于大數素性的檢驗、關于一個有限單群的構造性的證明等問題。 總之，圍繞着四色猜想的計算機解決，人們提出了許多重大的問題∶技術上的和哲學上的。四色猜想的計算機證明之意義，決不僅僅在于一個曆時多年的難題的解決。就從目前的趨勢看，它很可能将成為數學發展史上一系列新思想的引子。分形幾何的創立就是一個說明。