本文發表於《大眾科學》的前部落格網路，反映了作者的觀點，不一定反映《大眾科學》的觀點
在我的上一篇專欄文章中 我敘述了在1990年代，兩位數學家如何以我的名字命名一個幾何物件“霍根曲面”，以報復我的“證明的消亡”。這篇專欄文章給了我一個機會，重新審視我1993年那篇有爭議的文章，該文章認為計算機的進步、數學日益增長的複雜性以及其他趨勢正在削弱傳統證明的地位。在撰寫專欄文章時，我意識到霍根曲面產生的證明與我的“證明消亡”論題相矛盾。我給幾位專家發了電子郵件，詢問他們認為我的“證明消亡”論題的現狀如何。以下是計算機科學家斯科特·阿倫森、數學物理學家彼得·沃伊特和數學軟體巨頭斯蒂芬·沃爾夫勒姆的回覆。（有關我與他們的問答連結，請參閱“延伸閱讀”）。如果/當他們有更多評論時，我會新增更多評論。 –約翰·霍根
斯科特·阿倫森的回應（他也剛剛釋出在他的部落格上）：
約翰，我喜歡你，所以我很不願意這麼說，但過去四分之一個世紀對你關於“證明消亡”的論題並不友好！ 那些給你發憤怒信件的數學家們說得有道理：數學界並沒有發生任何值得如此戲劇性標題的根本性變化。 基於證明的數學仍然非常健康，例如，自從你的文章發表以來，龐加萊猜想得到了解決，埃爾德什差異問題、卡迪森-辛格猜想、卡塔蘭猜想、素數中的有界間隙、確定性多項式時間內的素性測試等等——僅僅從我略知一二的極小部分領域中挑選了一些例子。
關於支援科學新聞業
如果您喜歡這篇文章，請考慮透過以下方式支援我們屢獲殊榮的新聞業 訂閱。透過購買訂閱，您正在幫助確保有關塑造我們當今世界的發現和思想的具有影響力的故事的未來。
數學實踐中存在著演變性的變化，就像一直以來那樣。 自2009年以來，網站MathOverflow讓數學家可以就一個晦澀的參考文獻或證明中一個頑固的步驟查詢全球集體智慧，並獲得近乎即時的答案。 同時，“多數學者”專案也取得了一定的成功，他們試圖利用部落格和其他社交媒體，透過大規模協作來推進長期存在的未解決數學問題。
雖然人類仍然坐在駕駛座上，但人們一直在努力增加計算機的作用，並取得了一些顯著的成功。 這些成功包括托馬斯·黑爾斯在1998年對開普勒猜想（關於橙子最密集的堆積方式）的計算機輔助證明——現在已經從頭到尾完全透過機器驗證，《數學年刊》拒絕發表傳統數學和計算機程式碼的混合物之後。 它還包括威廉·麥丘恩在1996年對代數中的羅賓斯猜想的解決方案（計算機生成的證明只有半頁，但涉及的替換非常奇怪，以至於60年來沒有人發現它們）；以及“另一個極端”，2016年由馬林·休勒和合作者對布林畢達哥拉斯三元組問題的解決方案，其大小為200太位元組（當時是“數學史上最長的證明”）。
有一天，計算機可能會取代人類在數學研究的所有方面——但也有可能，當它們能夠做到這一點時，它們也將能夠取代人類在音樂、科學新聞和所有其他領域的工作！
新的證明概念 ——包括機率證明、互動式證明、零知識證明，甚至量子證明——自1993年以來在理論計算機科學家中得到了進一步發展。 然而，到目前為止，這些新型證明仍然要麼完全是理論性的（如量子證明），要麼用於密碼協議，而不是用於數學研究。 （例如，零知識證明現在在某些加密貨幣中發揮著重要作用，例如Zcash。）
在許多數學領域（包括我自己的理論計算機科學），證明變得越來越長，任何一個人都難以理解。 這導致一些人提倡一種分離方法，即人類數學家只相互討論模糊的直覺和高層次的概念，而繁瑣的細節驗證則留給計算機。 然而，到目前為止，以機器可檢查的格式編寫證明所需的大量時間投入——幾乎沒有新的見解回報——阻止了這種方法的廣泛採用。
是的，數學中存在非嚴格的方法，這些方法繼續在物理學、工程學和其他領域廣泛使用，就像一直以來那樣。 但是，只要有嚴格的證明可用，這些方法都沒有取代證明作為黃金標準的地位。 如果我不得不推測原因，我會說：如果你使用非嚴格的方法，那麼即使你清楚在什麼條件下你的結果可以被信任，其他人也可能不太清楚。 此外，即使研究社群中只有一部分人關心嚴謹性，該部分人所依賴的任何早期工作也需要是嚴格的——從而在該方向上施加持續的壓力。 因此，給定的研究領域變得越協作，嚴謹性就越重要。
在我看來，一個世紀前，康托爾、弗雷格、皮亞諾、希爾伯特、羅素、策梅洛、哥德爾、圖靈等人在數學基礎方面的闡明，仍然是人類思想最偉大的成就之一，與進化論、量子力學或任何其他事物並駕齊驅。 誠然，這些偉人設定的理想仍然主要是理想化的。 當數學家說一個定理已被“證明”時，他們的意思仍然像以往一樣，更像是：“我們已經達成社會共識，所有思路都已到位，可以進行嚴格的形式證明，該證明可以由機器驗證……剩下的唯一任務是大量的死記硬背編碼工作，我們沒有人打算永遠做下去！” 同樣真實的是，數學家作為人類，會受到你可能期望的各種弱點的影響：聲稱已經證明了他們沒有證明的東西，為誰證明了什麼而爭吵，指責他人缺乏嚴謹性，同時自己卻虛偽地放縱。 但正如愛和誠實仍然是美好的理想，無論它們被違反多少次一樣，數學的嚴謹性也是如此。
彼得·沃伊特的回應
回想四分之一個世紀前的這場辯論，最讓我震驚的是變化如此之小。 現在有很多資金和注意力都集中在資料科學、機器學習、人工智慧等方面，但除了更多的學生在這些領域找到工作之外，對純數學研究的影響微乎其微。 一個變化是網際網路提供了更好的訪問高質量數學研究材料和討論的途徑，例如講座影片、MathOverflow上的討論以及我的同事約翰·德容的Stacks Project。 這種變化使人們像以往一樣進行交流，只是更有效率。
與此同時，計算機在數學定理的證明的建立和檢查中仍然很少發揮作用。 圍繞望月新一宣稱證明abc猜想的激烈辯論提供了一個有趣的案例。 理解和檢查證明的問題涉及到該領域最優秀的人才，他們正在為理解而進行艱難的鬥爭，而計算機化的證明檢查根本沒有發揮任何作用。 沒有證據表明計算機軟體現在比1993年更接近與彼得·舒爾茨和其他專家競爭，這些專家致力於分析望月新一的論證。 如果這個故事未來有新的積極發展，那將是來自有血有肉的數學家，而不是科技行業的伺服器農場，在更深入的理解方面取得進展。
斯蒂芬·沃爾夫勒姆的回應。 當我聯絡Mathematica和其他產品的創始人沃爾夫勒姆時，一位公關人員發給我一個連結，指向沃爾夫勒姆最近的文章“邏輯、可解釋性和理解的未來”。這篇文章充滿了關於數學、邏輯、證明、計算和一般知識本質的挑釁性斷言。沃爾夫勒姆首先聲稱，他已經繪製出了所有可能邏輯公理的空間，他認為，這表明我們通常依賴的公理並非以某種方式是最優或必要的，而是任意的。我的理解是，可能的數學空間雖然是無限的，但可能比通常認為的更無限。沃爾夫勒姆還暗示，藉助他的一項發明Wolfram Language，計算機證明不必是黑匣子，它們生成結果，但幾乎不產生理解。以下是他對此的看法：
在某種程度上，我認為將證明通常呈現給人類理解，而程式通常只被認為是供計算機執行的東西，這是一種歷史的怪癖……[O]我在過去幾十年努力的主要目標之一是改變這種狀況——並在Wolfram Language中開發一種真正的“計算通訊語言”，在這種語言中，計算思想可以用一種計算機和人類都容易理解的方式進行交流。
但沃爾夫勒姆警告說，我們永遠會遇到理解的極限
在數學中，我們習慣於構建我們的知識堆疊，以便每個步驟都是我們可以理解的。但實驗數學——以及諸如自動定理證明之類的事物——清楚地表明，有些地方是我們無法具備這種特徵的。我們會稱之為“數學”嗎？我認為我們應該稱之為“數學”。但這與我們過去一千年主要使用的傳統不同。這是一個我們仍然可以構建抽象，並且仍然可以構建新的理解水平的傳統。但在這之下的某個地方，將存在各種各樣的計算不可約性，我們將永遠無法真正將其帶入人類理解的領域。
卡爾·達爾克的回應： 達爾克是一位數學家，我之前曾與他通訊。請訪問他的網站這裡。
科學的終結（你最喜歡的話題之一）和形式證明的終結之間可能存在相似之處。兩者都可以更準確地改述為不可避免的收益遞減規律。我們不期望在這些領域中的任何一個領域發生正規化轉變，儘管漸進式進步始終是可能的，但其實現的成本卻越來越高。數學和科學的低垂果實在文藝復興時期被採摘，到1960年，中間的樹枝也被剝光了。 為了到達樹冠，我們動用計算機，就像用高空作業車將我們送到樹的更高處一樣，但這項技術幫助了我們，它並沒有取代我們。人仍然必須用手摘水果， 而且我不希望這種情況在短期內發生改變。
在粒子物理學中，證實希格斯玻色子的超大型強子對撞機可能是有史以來建造的最大機器，但 人類必須解釋資料；對撞機本身並沒有發現任何東西。同樣，計算機幫助數學家進行研究，但我們必須自己構建形式證明。你提到了大衛·霍夫曼曲面，計算機提供了直覺，但數學家編寫了證明。
“實驗幾何實驗室”是另一個例子。比爾·戈德曼部分說道：“嘗試解釋數學的練習……實際上幫助我們發現了新的結果，即使計算機本身在發現過程中並沒有真正發揮太多作用。對計算機進行程式設計以生成幾何影像所需的細節程度可以提高研究人員對遊戲中思想的理解。”
除了計算機之外，合作也是關鍵，通常是在國際範圍內。成千上萬的科學家和工程師共同努力證實了希格斯玻色子，同樣地，數百名數學家合作證明了費馬大定理。安德魯·懷爾斯獲得了榮譽，他的貢獻不應被低估，但他站在巨人的肩膀上。即使在計算機的幫助下，一個人的大腦也幾乎無法容納，更不用說創造，一個現代證明。這個Nova特輯列出了使懷爾斯證明成為可能的所有數學家；跳轉到結尾並觀看它滾動播放。 http://www.pbs.org/wgbh/nova/proof/wiles.html
所有這一切都對研究生產生了影響，正如我在1990年發現的那樣。我的學術顧問告訴我，在伯克利獲得博士學位的平均時間是7.5年。我感到茫然。我願意花費十分之一的生命來獲得博士學位嗎？而我的儲蓄賬戶正在減少，我妻子的生物鐘也在滴答作響？事實證明，我不願意；我獲得了碩士學位，找到了一份程式設計師的工作，並組建了家庭。博士學位的標準是，而且一直都是，原創研究，帶有“有趣的”原創研究的潛臺詞，由該領域的專家判斷。然而，新的成果越來越難獲得。
這在純數學中尤其如此，但也可能適用於其他領域。在某個時候，博士學位的標準可能不得不轉變——也許是對正在進行的研究的貢獻，即使它尚未產生任何成果，或者可能是為了清晰或教育目的而對現有材料進行重新包裝，就像樂隊翻唱一首已有的歌曲一樣。我無法預測這將走向何方，但很少有研究生可以將他們生命中的8年或10年投入到博士課程中，尋找太陽下的新事物，同時他們還要兼職以維持生計。
延伸閱讀:
身心問題 （免費線上書籍）