阿蒂亞（Michael Atiyah）曾說過：「我們的理想是探究數學真諦，而不是利用機械執行指令的計算機推演論證。」另一位菲爾茲獎獲得者澤爾曼諾夫（Zelmanov）也表示贊同：「只有所有數學家都認可的證明方法才是真正有效的，所以我對機器證明方法的前景並不看好。」他說的有道理嗎？如果數學證明方法只有生成它的機器能夠理解，我們真的可以相信嗎？
我們的寫作工具參與了我們思想的形成過程。
——弗裡德裡希·尼採（Friedrich Nietzsche）
撰文｜Marcus du Sautoy（牛津大學數學教授）
翻譯｜王曉燕、陳浩、程國建
儘管我有點擔心計算機會讓我丟掉工作，但我不得不承認，作為一種工具，它是一個「無價之寶」。當我們需要將一系列方程合併成一個方程時，手工計算是很難保證不出錯的。但對於計算機來說，它就很擅長處理這種重複而機械且計算量龐大的任務。你只需要定義一套規則，剩下的就由計算機接手了。而且，在速度與準確性等方面，計算機是遠超過手工計算的。正因為如此，近年來計算機的作用越來越重要，其應用領域也越來越廣泛。
數學與電腦程式的算法緊密相關。因此，近半個世紀計算機常用於證明一些複雜的數學問題。20世紀70年代，計算機對「四色定理」的證明轟動了全世界。四色定理指的是「任何一張地圖只用四種顏色就能使具有共同邊界的國家著上不同的顏色。」也就是說，在不引起混淆的情況下，一張地圖至少需要四種顏色來標記。
儘管此前很多人認為五種顏色就是下限，但計算機的發明大大加快了對四色定理證明的進程。1976年，數學家凱尼斯·阿佩爾（Kenneth Appel）和沃爾夫岡·哈肯（Wolfgang Haken）在前人的基礎上用計算機證明了四色定理。阿佩爾與哈肯把地圖的無限種可能情況簡化為1936種構型，但是要靠人工逐一驗證如此之多的構型是不現實的，所以才需要藉助計算機進行驗證。計算機根據程序指令逐一瀏覽地圖並檢查其是否滿足四色定理。當時的計算機運算速度還不夠高，整個證明過程的耗時超過了1000小時。
能相信計算機嗎？
計算機只能執行指令，並無自主創造力。但是，想要證實程序中是否存在錯誤是很困難的。我們能在多大程度上相信計算機，這個問題一直困擾著人工智慧領域的學者。當我們進入由算法主導的未來時，確保代碼中沒有未被檢測出的錯誤，將成為一項艱巨的挑戰。
2006年匹茲堡大學的託馬斯·黑爾斯（Thomas Hales）教授在《數學年鑑》上發表了關於藉助計算機證明著名的數學問題—「克卜勒猜想」的論文。簡單來說，克卜勒猜想就是對在空間中如何最密集地堆積圓球的解答。出於有效利用空間以及避免壓壞水果的考慮，水果店店主一般會將水果層層交替堆疊，任意平面上的每個水果都與六個水果相鄰，構成正六邊形。像阿佩爾與哈肯一樣，黑爾斯採用的也是藉助計算機對足夠多的案例進行窮舉證明的方法。事實上，早在1998年，黑爾斯就曾宣布他的證明完成，並向《數學年鑑》評審組提交了論文、程序代碼及相關資料，但該項證明的審核驗證經歷了漫長的時間。這是因為人類大腦的物理局限性，審核人必須得充分相信計算機的能力，就好比我們第一次乘坐飛機一樣，心中難免惴惴不安。用了8年時間，數學家們證明了黑爾斯是正確的，但其確定性是99%。
對於數學純化論者來說，這1%也是不可容忍的。這就好比，要證明你是牛頓的親戚，可是家族譜系圖裡卻缺少了關鍵的一環……人們質疑計算機證明數學問題的能力，並不是因為害怕計算機在未來會使得他們丟掉工作（早些年計算機只會按人類的指令執行操作，並不具備自主學習能力），主要是因為無法確定電腦程式是否存在潛在缺陷。我們該如何去相信計算機的證明呢？
數學家們就曾被程序代碼中的缺陷困擾。1992年，牛津物理學家利用弦理論中的啟發法對高維幾何空間中可識別的代數結構數量進行了預測。對於該預測，數學家們持懷疑態度，因為他們覺得物理學不具備解釋抽象結構的能力。當有證據表明這個猜想是錯誤的時候，他們覺得自己的懷疑是有道理的。然而，後來事實證明，否定這個預測的錯誤證據正是由一個有缺陷的電腦程式生成的。所以，錯的是數學家，而不是物理學家——程序的錯誤把他們引入了歧途。幾年之後，數學家們開始努力地證明物理學家的預測是對的（這一次數學家們把計算機排除在外了）。
這樣的故事加劇了數學家們的擔憂，他們擔心計算機可能會讓我們在結構不健全的「程序地基」之上建造精巧的「數學大廈」。但坦白講，許多問題的證明往往都存在不足或錯誤，人類犯錯的可能性通常比計算機更大。包括我本人發表的一些證明，後來也被發現存在一些漏洞。錯誤可以被修正，但遺憾的是，在證明的驗證和審核階段它們並沒有被找出來。
證明的驗證和審核非常重要，它是發現缺陷和漏洞的重要環節。這就是為什麼數學界「千禧年大獎問題」的證明要經過兩年的審核驗證期—大家認為24個月的時間足夠讓錯誤暴露出來。以安德魯·懷爾斯證明「費馬大定理」為例，在其證明方法付梓之前，審驗人員發現了一個小缺陷。但懷爾斯和理察·泰勒（Richard Taylor，曾是懷爾斯的學生）奇蹟般地修正了這一缺陷。即便如此，在錯誤證明的基礎上構建數學體系的情況也是屢見不鮮的。
許多新的證明極其複雜，以至於數學家們很擔心一些潛在的錯誤難以被發現。以有限單群分類定理（classification of finite simple groups）為例，單群在有限群論中的地位，與素數在數論中的地位、原子在化學中的地位一樣，它們都是構建各自所在世界的「磚塊」。對於任意的有限群，我們可以將其分解為一系列單群，且分解方法是唯一的。通過研究這些「磚塊」，我們可以進一步發現由它們所組成的物質的結構和性質。與當年化學家尋找新元素一樣，數學家也開始了對於單群的尋找—列出一個單群的「元素周期表」，並證明這個「周期表」中包含了所有的單群。其中，「魔群」是最大的「散在單群」。「魔群定理」的證明散落在100多篇論文中，合計超過10000頁，涉及數百名數學家。單群的「元素周期表」中含有26個散在單群，對於是否存在第27個散在單群，人們總是持懷疑態度。對於這種類型的複雜證明，進行人力審核幾乎是不可能的，那麼，是否可以通過電腦程式來檢驗數學定理的證明呢？
新的問題又出現了，用電腦程式去檢驗計算機證明的步驟，是否可信？怎麼確保電腦程式中沒有缺陷？再用另一臺計算機去查證嗎？這會陷入一個永無休止的死循環。你怎麼能確定你的方法正在引導你走向真正的知識的「聖杯」？真理的產生取決於你的證明方法。
正如哲學家大衛·休謨（David Hume）指出的，大多數科學研究都建立在歸納法之上—通過觀察特定的例子來推斷出一個普遍的規律或原則。為什麼歸納法是一種產生科學真理的好方法呢？這主要是因為在歸納法裡我們可以舉出許多例子來說明。基於歸納法，曾產生了許多著名的科學理論，這反過來證實了歸納法確實是一種科學研究的好方法。
Coq證明助手
在過去，數學問題的證明和驗證過程全憑人工完成。而現在，越來越多的證明開始借力於計算機，但因為驗證的過程既煩冗又複雜，並且工作量巨大，人類大腦的局限性決定了無法採用人工驗證的方式判斷其對錯。因此，我們迫切需要一種解決方案，即通過構建新的程序來驗證計算機證明的正確性。
20世紀80年代末，法國數學家皮埃爾·於埃（Pierre Huet）和蒂埃裡·科昆德（Thierry Coquand）開始從事結構微積分（calculus of constructions）項目。該項目簡稱CoC，但很快又被稱為Coq（法語裡意為「公雞」）。這個改動一方面是為方便記憶，因為在法國一直有以動物命名開發工具的習慣；另一方面是因為Coq是其開發者之一科昆德姓氏的前三個字母。Coq為驗證數學證明而生，很快也成了驗證計算機證明的重要程序，備受青睞。
2000年，微軟研究院首席研究員喬治·貢蒂爾（Georges Gonthier）及其同事使用Coq對阿佩爾與哈肯的四色定理的計算機證明進行了驗證，因為這是史上第一個需要計算機才能完成的證明（假定Coq不存在任何缺陷）。然後，他們也使用Coq去驗證了阿佩爾和哈肯自己所寫的證明部分。
人類手工證明與計算機證明不同，手工證明過程中會跳過一些煩瑣或眾人皆知的步驟，而計算機卻依賴於明確、細化的步驟才能正確執行指令。這類似於寫小說和寫保姆指導手冊的區別。前者不需要對主人公的每一個動作都解釋得一清二楚，而後者則需要儘可能地明確和詳盡，包括一天中嬰兒的食譜，以及吃飯、睡覺、上廁所的每一個細節。
計算機用了5年的時間進一步自動識別並驗證人類證明的過程。這期間，人們驚訝地發現了在第一次證明中被忽略的數學知識。
Coq與原始的計算機證明相比，更應該信任誰呢？當然是前者。越來越多的計算機證明被Coq所驗證，使我們更加確信Coq是可靠的。這就像我們通過歸納法驗證數學中的基本公理一樣。這就像任取兩個數A和B，如果A+B都等於B+A，那麼A+B=B+A就是正確的。用一個電腦程式來驗證多個計算機證明，比編制一個特定的證明程序或者進行人工證明更值得我們信任。
貢蒂爾團隊驗證完四色定理後，緊接著開始了對奇階定理（odd order theorem）的驗證工作。奇階定理是對稱性研究最重要的指導定理之一，通常被認為是有限單群分類的基石。像化學裡的元素周期表一樣，有限單群是構成數學有限群論「元素周期表」中的基本元素，所有的對象都由有限單群構成。具有素數邊的正多邊形（如正三角形、正五邊形）是該周期表中的元素。此外，該周期表中還有一些複雜且獨特的對稱元素，如旋轉了60次的正二十面體、需要196883維線性空間才能表達的「魔群」等。「魔群」具有的元素個數超過了構成地球的原子個數。
該定理指出，任何奇階對稱結構的基本組成單元都是素數多邊形，此外再無其他結構。如果把對稱物體分為奇階和偶階兩種，那麼該定理就等於涵蓋了其中的一半，意義重大。
奇階定理的原始論文有255頁，佔據了《太平洋數學期刊》的全部篇幅。在它出版之前，大多數證明最多只有幾頁，一天內即可掌握。這個冗長複雜的證明，對每一位數學家來說都是一個挑戰。因此，其中是否存在細微的缺陷或錯誤，始終無法考證。
Coq對複雜數學定理的證明過程，一方面可以檢驗Coq的能力，另一方面能幫我們樹立足夠的信心。但將人工證明轉換成可驗證的計算機代碼這一過程並不容易。
貢蒂爾略帶靦腆地回憶道：
第一次開會討論時，我向團隊裡其他成員宣布了我的宏偉計劃，他們流露出不可思議的表情，就像是我得了妄想症。奇階定理的證明過程太過複雜，驗證它最初被認為是不可能的。做這個項目的真正原因，是為了充分理解數學理論的構建過程並使之與Coq充分融合。
會議結束後，團隊裡的一名程式設計師查看了原始證明，隨後向貢蒂爾發來一封郵件：「17萬行代碼，1.5萬個變量，4300個函數。好玩，太棒了！」微軟劍橋研究院團隊用了6年的時間完成了證明。當項目即將結束時，貢蒂爾興奮地說，經過無數個不眠之夜，他終於可以放鬆一下了。
貢蒂爾說：「數學是最偉大的浪漫主義學科之一，即便是天才，也得掌握所有知識才能激發靈感，理解一切。」但是，人類的大腦存在物理上的局限性。他希望他們所做的一切能夠叩開人類與機器彼此信任、持續合作的新時代「大門」。
人腦的極限
年輕的數學家們開始意識到，數學研究變得更為艱難了：學科分支越發密集，問題越發複雜。攻讀博士學位的3年時間，只夠去理解導師所給題目的含義。隨後，再花費數年時間去研究、探索，運氣不錯的話，會得到一些研究成果。然而，你發表的論文卻面臨著沒人能審核它。
審核別人發表的論文是得不到太多報酬的，但期刊論文的審核必須經過同行的評審。職稱評定也以公開發表在《數學年鑑》或《l扞HES數學期刊》這類文獻中的論文積分為基準。因此，有一個像Coq證明助手這樣的系統就非常重要了。
一些數學家認為我們目前正處在一個新舊時代的交替期——數學的發展雖然受到人類大腦局限性的制約，但藉助於計算機，我們對數學的探索已遠遠超出了人腦的思維範疇。
偉大的數學家們能夠用他們睿智的頭腦，藉助於紙和筆這些極其簡單的工具，構造出像「魔群」這樣具有196883維的對稱體，這是人類的奇蹟。但數學家們終將會老去，就像中世紀的泥瓦匠，其精湛的技藝將伴隨身體的死亡而從人世間消失。如果很難找到通往「新奇蹟」的方向，人們終將失去創造的原動力。
費馬大定理的證明長達數百頁，跨越3個世紀，這說明人類擁有足夠的耐心。當你努力去證明一個極其複雜的猜想時，隱約會有一種突破人類大腦物理極限的感覺。數學是無限的，而人的能力是有限的。但即便如此，我們常會為自己所做的努力感到吃驚，因為我們用數學的方式證明了「數學海洋的廣闊無邊」。
有一個問題幾乎困擾了我15年之久。每次推演時，總是在即將得到解決方案的關鍵時刻，我的大腦容量就不夠用了，它給我「即將宕機！」的警告。距離成功僅一步之遙，卻難以取得突破。就像現象與本質之間隔著一張「漁網」，它制約著我們，讓我們難以衝出迷霧，得到光明。當幾代數學家致力於黎曼假設的證明而不得其解時，人們開始懷疑，是否這樣的證明已超越人腦的極限。
著名數學家哈代多年來一直試圖證明黎曼假設，後來他自嘲道：「每個傻瓜都能提出有關質數的問題，而最聰明的人卻無法解答。」奧地利數學家、邏輯學家庫爾特·哥德爾（Kurt Gdel）有過論證：數學中包含了許多沒有經過證明的真理。能否用新的公理去證明那些未被證明的真理呢？哥德爾早在1951年就發出了警示，他認為我們可能會越來越難以掌控現代數學的發展方向：
人們創造出了一套龐雜且仍在擴展的公理系統，但人們研究它的目的越來越說不清楚……的確，在現代數學中，這些更高層次的理論成果實際上無法投入使用，這有可能與它們無法證明某些基本定理有關，例如黎曼假設。
鑑於我們可能即將觸及人類自身能力的極限，一些數學家已意識到，如果希望人類文明持續進步，我們將需要更多的機器輔助。就好比登上珠穆朗瑪峰之巔，我們可能只需要一個氧氣罐，但如果人機不能結合，我們永遠無法登上月球。
以色列數學家多倫·澤爾伯格（Doron Zeilberger）認為：數學家只用鉛筆和紙張工作的日子即將結束。20世紀80年代以來，他一直使用計算機撰寫論文。他將自己的由AT＆T（美國電話電報公司）生產的計算機命名為「Shalosh B. Ekhad」（希伯來語中3B1的意思），並堅持將這位機器夥伴作為論文的聯合作者。澤爾伯格認為，人們之所以不願倚重人機合作的方式，是因為「狹隘的人本主義」在作祟，這種偏執與其他形式的偏執一樣，阻礙了人類發展的腳步。
大多數數學家認為他們孜孜以求的目標非常深奧，是計算機難以企及的。換言之，他們不僅希望能得到真理，並且希望探求真理背後更多的內涵。如果計算機在無法真正理解數學的情況下就能驗證數學真理，他們會覺得非常荒謬。
獲得菲爾茲獎的數學家麥可·阿蒂亞（Michael Atiyah）曾說過：「我們的理想是探究數學真諦，而不是利用機械執行指令的計算機推演論證。」另一位菲爾茲獎獲得者澤爾曼諾夫（Zelmanov）也表示贊同：「只有所有數學家都認可的證明方法才是真正有效的，所以我對機器證明方法的前景並不看好。」當然，我們也不會認可只有一位數學家採用的證明方法。澤爾曼諾夫說的有道理嗎？如果數學證明方法只有生成它的機器能夠理解，我們真的可以相信嗎？
起初，多倫·澤爾伯格對這種觀念也非常理解，但最終對其不屑一顧。他承認，讓他樂此不疲的是在整個數學證明過程中得到所有的證據。對他來說，這就是生活，而生活是錯綜複雜的。他相信如果人的頭腦可以找到一個證據，那麼它一定是顯而易見的：
二三十年後，人類可以通過計算機輕鬆完成大多數事情。在數學領域裡，利用計算機完成很多工作已經變成現實。現在，人類很多剛發表的論文就已過時了，其實完全可以用算法來替代人類完成這些工作。現如今我們遇到的很多問題已經變得毫無意義，但是我們還是繼續在做，僅僅因為這是人類可以做的事情。
對於數學領域的現狀來說，這是相當令人沮喪的評估。但這是真的嗎？我當然覺得有些論文進入期刊是因為我們需要出版物，但這並不總是壞事。為了做某事而做某事所帶來的意想不到的成果已經多次證明，無目標驅動的研究有時是收集真正的新見解的最佳方式。
像許多業界同人一樣，喬丹·艾倫伯格（Jordan Ellenberg）認為人類未來在數學領域中仍然會發揮至關重要的作用：
我們非常擅長搞定計算機無法做到的事情。想像一下未來，如果目前所知道的一切定理都可以通過計算機得到證明，那我們就可以去探索計算機無法解決的其他問題，這有可能成為未來的「數學」。
但人類的許多研究成果不是向前而是橫向平行延伸的。在某些領域我們確實達到了臨界點，想要超越珠穆朗瑪峰的高度就必須藉助一臺機器。這對保守派來說是一種震撼的觀念衝擊（也可能包括我自己）。他們不願承認的是，人類再也不可能僅使用筆和紙來探求數學的奧義了。
作者簡介：
馬庫斯·杜·桑託伊（Marcus du Sautoy），英國皇家學會院士，美國數學學會院士，牛津大學西蒙尼公眾理解科學教授，大英帝國勳章獲得者，英國皇家學會麥可·法拉第獎獲得者，倫敦數學協會貝維克獎獲得者。桑託伊被譽為科學王國的大使，他創造了「流行數學」的概念，將複雜的數字和數學概念用形象生動、通俗易懂的語言表達出來。他常為《泰晤士報》和《衛報》寫文章，也為電臺和電視臺作評論，同時與英國BBC廣播公司保持長期合作。2001年，他贏得了倫敦數學會的貝維克獎(Berwick Prize)。2004年，他被英國《周日獨立報》評為英國最傑出的科學家之一。