數學家可以被計算機取代嗎？_風聞

原創：中科院物理所

作者：Marianne Freiberger and RachelThomas

翻譯：Nothing

審校：loulou

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

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

計算機輔助的證明

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

使用四種顏色上色的地圖

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

計算機做出的證明

計算機還可能以一種更加神奇的方式幫助數學研究。Automated theoremprovers（ATPs）是一種可以利用邏輯規則產生數學結果的程序：它能得到一個可以從假設和公理出發並按照邏輯推理得到的結果。

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

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

真的不需要人類嗎 ？

但是，也許這些發展並不需要過多地關注數學家;畢竟，它們只是數學在不同領域的應用。但Gowers相信，即使是在數學領域內偉大的事情仍然會到來。人類數學家與計算機的區別不僅僅在於他們喜歡讓證明變得優雅美麗，他們也希望能提供一些關於結果為什麼真實可靠的看法。他們發現證明似乎是人類獨有的思考方式，例如不同領域的數學以及數學和科學之間可以在更高的層次產生聯繫，而目前的計算機顯然是不可能做到這一點的。

但是Gowers認為，即使在人類使用的數學方法中，證明也不是完全抽象的。如果我們能真正理解我們所説的“證明”到底是什麼意思，人們如何發現證明，並創建一個將現有的數學知識合理分類的數據庫作為背景知識，那麼也許有一天我們能讓計算機證明像人類數學家一樣進行證明。

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

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

這似乎限制了計算機作為數學家的能力，但如果你仔細想想，人類數學家面臨着同樣的限制。面對這些問題，我們仍然在做數學，大多數數學家就算有也只會在休息日擔心這些基礎問題。如果計算機變得像Gowers所説的那樣優秀，那麼也許有一天他們能夠自己去思考這些問題。

數學中的合作

關於有限單羣分類的工作涉及一百多位數學家的共同工作。

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

Tranah認為，這種發展應該會改變數學審查和出版的本質。目前，數學家們把他們的論文寄給學術期刊，由該領域的其他專家對其進行審查，如果這些專家認為結果正確且有趣，他們就發表論文。這些期刊充當的是數學成果的記錄員，並且充當了你在查找時要去的“圖書館”。

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

解釋和真相

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

這場辯論的核心問題是：什麼是證明？它們僅僅是真理的證明，還是應該揭示某些事情是真實的？對於許多數學家來説，解釋事物真實性的證明最有價值。這種證明能用計算機實現嗎？

原文來源：

https://plus.maths.org/content/future-proof