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

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

計(jì)算機(jī)輔助的證明

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

使用四種顏色上色的地圖

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

計(jì)算機(jī)做出的證明

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

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

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

真的不需要人類嗎 ？

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

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

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

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

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

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

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

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

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

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

解釋和真相

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

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