數(shù)學(xué)家將來會被計算機代替嗎？如果數(shù)學(xué)只包含程序化的計算，那么答案是肯定的。但是如果你想讓計算機進行數(shù)學(xué)證明，甚至解決邏輯上的難題，你也知道這樣的問題需要直覺和想象力的跳躍，這是計算機的能力之外的事情。即使僅僅是判斷哪種問題在數(shù)學(xué)上是有趣的、無聊的或者無法研究的，貌似也不得不讓人參與其中。

在B(A)管理委員會就“證明的未來”進行辯論的小組。

計算機輔助的證明

依靠計算機的輔助來進行證明并不是新鮮的事情。第一個例子就是1976年對四色定理的證明，四色定理是指任何一個畫在平面上的地圖僅需要四種顏色，就足以保證任意兩個相鄰的國家可以用不同的顏色標注。為了證明這個說法，計算機檢驗了大量的地圖從而證明了這個定理的正確性。1998年著名的開普勒猜想，它指的是如何堆積一些圓球使得它們占據(jù)的空間最小，對這個猜想的證明我們更多的借助于計算機。

使用四種顏色上色的地圖

這些證明隱含著一個問題：沒有一個人能夠檢查計算機是否出錯。一些人會反對說，這樣的證明不能被認為是完全證明，但是其他人愿意接受這些由機器輔助完成的證明。正如Barrow-Green指出的，單個數(shù)學(xué)家不能完成的證明不一定非要計算機的輔助才能完成：一個例子是100多位數(shù)學(xué)家共同努力完成了對有限簡單群的分類。當然計算機的使用也不是一件新鮮事。Martin引用了Hardy和Ramanujan的例子，他們在二十世紀初用MajorMacMahon計算得到的表格來研究分拆函數(shù)（partition function）。

計算機做出的證明

計算機還可能以一種更加神奇的方式幫助數(shù)學(xué)研究。Automated theoremprovers（ATPs）是一種可以利用邏輯規(guī)則產(chǎn)生數(shù)學(xué)結(jié)果的程序：它能得到一個可以從假設(shè)和公理出發(fā)并按照邏輯推理得到的結(jié)果。

ATPs已經(jīng)在數(shù)學(xué)中獲得一些成功，但有趣的是，它在我們的生活中也產(chǎn)生了影響。計算機程序在廣泛的領(lǐng)域內(nèi)都得到了應(yīng)用，從控制客機或核反應(yīng)堆到心臟起搏器。為了安全和節(jié)省資金，你需要知道這樣的系統(tǒng)是否工作正常。確保這一點的一種方法是在大量情景下多次測試一個系統(tǒng)，并確保它總是做正確的事情——但這可能會耗費大量時間，更要命的是，如果不能測試所有可能的情況，測試可能仍然會錯過發(fā)現(xiàn)錯誤的機會。相反，我們可以使用ATPs，以數(shù)學(xué)方式驗證特定硬件系統(tǒng)或運行在其上的代碼是否正確，并始終按其應(yīng)該的方式運行。

ATPs仍然需要大量的人工輸入來工作，但Pitts相信，至少在計算機科學(xué)中它正引起巨大的變化。許多數(shù)學(xué)家可能會覺得這種發(fā)展有點悲哀：正如Pitts指出的，這意味著人們不再關(guān)心如何使數(shù)學(xué)論證變得優(yōu)雅。計算機不關(guān)心是否使用暴力求解的手段得到證據(jù)，例如遍歷檢查所有的可能性——其目的只是為了找到一個證明。相比之下，人類數(shù)學(xué)家總是想尋找一個更高層次的原理，可以將所有這些可能性統(tǒng)一在一個優(yōu)雅的過程中。事實上，在計算機科學(xué)中所做的證明通常是“又大又丑”。

真的不需要人類嗎 ？

但是，也許這些發(fā)展并不需要過多地關(guān)注數(shù)學(xué)家，畢竟，它們只是數(shù)學(xué)在不同領(lǐng)域的應(yīng)用。但Gowers相信，即使是在數(shù)學(xué)領(lǐng)域內(nèi)偉大的事情仍然會到來。人類數(shù)學(xué)家與計算機的區(qū)別不僅僅在于他們喜歡讓證明變得優(yōu)雅美麗，他們也希望能提供一些關(guān)于結(jié)果為什么真實可靠的看法。他們發(fā)現(xiàn)證明似乎是人類獨有的思考方式，例如不同領(lǐng)域的數(shù)學(xué)以及數(shù)學(xué)和科學(xué)之間可以在更高的層次產(chǎn)生聯(lián)系，而目前的計算機顯然是不可能做到這一點的。

但是Gowers認為，即使在人類使用的數(shù)學(xué)方法中，證明也不是完全抽象的。如果我們能真正理解我們所說的“證明”到底是什么意思，人們?nèi)绾伟l(fā)現(xiàn)證明，并創(chuàng)建一個將現(xiàn)有的數(shù)學(xué)知識合理分類的數(shù)據(jù)庫作為背景知識，那么也許有一天我們能讓計算機證明像人類數(shù)學(xué)家一樣進行證明。

Gowers認為，到本世紀末，人類數(shù)學(xué)家很有可能真的將自己從證明中解放出來。一旦計算機能夠很好地證明一些結(jié)果，它們也就能夠很好地決定要證明哪些結(jié)果，從而完全擺脫了人類的指導(dǎo)。

如果你熟悉哲學(xué)，那么一個反對的聲音會立刻浮現(xiàn)在你的腦海中。計算機除了使用公理化的數(shù)學(xué)方法別無選擇。他們的邏輯推斷需要基于一套公理和規(guī)則，你可能質(zhì)疑這些公理和規(guī)則應(yīng)該是什么。更重要的是，庫爾特·哥德爾在20世紀30年代證明了任何一個形式系統(tǒng)，只要包括了簡單的初等數(shù)論描述，而且是自洽的，它必定包含某些系統(tǒng)內(nèi)所允許的方法既不能證明真也不能證偽的命題。

這似乎限制了計算機作為數(shù)學(xué)家的能力，但如果你仔細想想，人類數(shù)學(xué)家面臨著同樣的限制。面對這些問題，我們?nèi)匀辉谧鰯?shù)學(xué)，大多數(shù)數(shù)學(xué)家就算有也只會在休息日擔心這些基礎(chǔ)問題。如果計算機變得像Gowers所說的那樣優(yōu)秀，那么也許有一天他們能夠自己去思考這些問題。

數(shù)學(xué)中的合作

關(guān)于有限單群分類的工作涉及一百多位數(shù)學(xué)家的共同工作。

除了計算機之外，還有另一種技術(shù)影響我們研究數(shù)學(xué)的方式。正如Barrow-Green指出的，數(shù)學(xué)從來不是一個人單打獨斗的工作。幾千年來，我們的證明標準發(fā)生了變化，因此人們不斷地重新審視得到的結(jié)果，提出新的證明和看待它們的新方法。如今，技術(shù)使人們可以同時為一個結(jié)果進行集體工作。這些協(xié)作證明的一個例子是上面提到的有限單群的分類，它于2004年完成，涉及了遍布世界各地的100多名數(shù)學(xué)家——這在紙質(zhì)信件的時代肯定是不可能實現(xiàn)的。另一個例子是Gowers建立的polymather項目，它允許數(shù)學(xué)家通過在線發(fā)布他們對問題的想法或評論他人的想法進行合作。

Tranah認為，這種發(fā)展應(yīng)該會改變數(shù)學(xué)審查和出版的本質(zhì)。目前，數(shù)學(xué)家們把他們的論文寄給學(xué)術(shù)期刊，由該領(lǐng)域的其他專家對其進行審查，如果這些專家認為結(jié)果正確且有趣，他們就發(fā)表論文。這些期刊充當?shù)氖菙?shù)學(xué)成果的記錄員，并且充當了你在查找時要去的“圖書館”。

Tranah認為，如今，這些期刊只不過是“垃圾郵件”，作為他們工作的記錄，實際上只對論文作者及其機構(gòu)有益。當數(shù)學(xué)家們尋找新的結(jié)果時，他們不會等待可能長達數(shù)年的論文審查期。相反，他們會選擇論文預(yù)印本網(wǎng)站，在正式發(fā)表論文之前，這些服務(wù)器會發(fā)布論文，并使用數(shù)學(xué)家的聲譽和他們自己的專業(yè)知識來評估論文的價值。因此，傳統(tǒng)的同行評審過程可能會被群體評審過程所取代。有趣的論文將吸引許多數(shù)學(xué)家的在線關(guān)注，隨著時間的推移，他們將在論文中添加更正和評論。這樣的過程將把好論文和壞論文分開，并確保它們是正確的。出版商將不再需要麻煩同行評論，從而節(jié)省時間和金錢。

解釋和真相

了解如何建立證明對每個人都至關(guān)重要。計算機科學(xué)家需要這些信息，以便他們能夠創(chuàng)建更強大的自動化系統(tǒng)。歷史學(xué)家和哲學(xué)家正在嘗試洞察數(shù)學(xué)文化，以及尋找在數(shù)學(xué)界被認為有效的東西。數(shù)學(xué)家們想學(xué)習如何研究更多的數(shù)學(xué)。理解想法是如何建立起來的正是我們和朋友喝咖啡的時候所討論的事。這比學(xué)術(shù)文獻中出現(xiàn)的最后的證明要有力得多，我們幾乎不知道這些證明是如何被發(fā)現(xiàn)的。

這場辯論的核心問題是：什么是證明？它們僅僅是真理的證明，還是應(yīng)該揭示某些事情是真實的？對于許多數(shù)學(xué)家來說，解釋事物真實性的證明最有價值。這種證明能用計算機實現(xiàn)嗎？