數學傳統上是一門孤獨的科學。1986年，安德魯·懷爾斯隱居書房七年以證明費馬大定理。由此產生的證明通常難以被同行理解，有些至今仍存在爭議。但近年來，數學的越來越大領域已被嚴格分解為各自的組成部分（“形式化”），以至於證明可以由計算機檢查和驗證。
加州大學洛杉磯分校的陶哲軒堅信，這些方法為數學領域的合作開闢了全新的可能性。如果再加上人工智慧的最新進展，未來幾年該領域可能會建立全新的工作方式。藉助計算機，大型未解決的問題可能會更接近解決。陶哲軒在接受《大眾科學》德語姊妹刊物《Spektrum der Wissenschaft》採訪時闡述了他對未來發展的看法。
[以下是經過編輯的採訪記錄。]
關於支援科學新聞
如果您喜歡這篇文章，請考慮透過以下方式支援我們屢獲殊榮的新聞報道 訂閱。透過購買訂閱，您將有助於確保有關塑造我們當今世界的發現和想法的具有影響力的故事的未來。
在您於舊金山舉行的聯合數學會議上的一次演講中，您似乎暗示數學家彼此不信任。您是什麼意思？
我的意思是，我們是信任的，但你必須親自認識某人。除非你能逐行檢查他們的工作，否則很難與從未見過面的人合作。通常最多[合作者]五個人。
隨著自動化證明檢查器的出現，這種情況正在發生怎樣的變化？
現在你可以真正與數百名你從未見過的人合作。你不需要信任他們，因為他們上傳程式碼，而Lean 編譯器會驗證它。你可以進行比我們通常做的更大規模的數學研究。當我形式化我們最近的成果，即所謂的 Polynomial Freiman-Ruzsa (PFR) 猜想時，[我與] 20 多人合作。我們將證明分解成許多小步驟，每個人都為一個小步驟貢獻了一個證明。我不需要逐行檢查貢獻是否正確。我只需要對整個過程進行管理，並確保一切都朝著正確的方向發展。這是一種不同的數學研究方式，一種更現代的方式。
德國數學家和菲爾茲獎得主彼得·肖爾茨參與了一個 Lean 專案——儘管他告訴我他對計算機不太瞭解。
在這些形式化專案中，並非每個人都需要成為程式設計師。有些人可以只專注於數學方向；你只是將一個大型數學任務分解成許多較小的部分。然後有些人專門將這些較小的部分轉化為形式證明。我們不需要每個人都成為程式設計師；我們只需要一些人成為程式設計師。這是一種勞動分工。
我大約在 20 年前就聽說過機器輔助證明，當時這是一個非常理論的領域。每個人都認為你必須從頭開始——形式化公理，然後進行基礎幾何或代數——而要達到更高的數學水平是超出人們想象的。是什麼改變使得形式數學變得實用？
一個變化是標準數學庫的開發。特別是 Lean，有一個名為 mathlib 的大型專案。本科數學的所有基本定理，例如微積分和拓撲學等等，都已被逐一放入這個庫中。因此，人們已經努力從公理達到相當高的水平。夢想實際上是將[庫]提升到研究生教育水平。那麼形式化新的[數學]領域將容易得多。還有更好的搜尋方法，因為如果你想證明某些東西，你必須能夠找到已經確認是真實的東西。因此，真正智慧的搜尋引擎的開發也是一項重大的新發展。
所以這不是計算能力的問題？
不，一旦我們形式化了整個 PFR 專案，編譯驗證它只花了大約半個小時。這不是瓶頸——瓶頸在於讓人類使用它，可用性，使用者友好性。現在有數千人的大型社群，並且有一個非常活躍的線上論壇來討論如何改進該語言。
Lean 是最先進的嗎，還是有競爭系統？
Lean 可能是最活躍的社群。對於單作者專案，可能有一些其他語言略好，但 Lean 通常更容易上手。它有一個非常好的庫和一個友好的社群。它最終可能會被替代品取代，但目前它是主要的正式語言。
當您談論另一個數學專案時，有人問您是否想將其形式化，您基本上說這需要太長時間。
我可以形式化它，但這會佔用我一個月的時間。目前我認為我們還沒有達到常規性地形式化一切的程度。你必須精挑細選。你只想形式化那些真正對你有用的東西，例如教你如何在 Lean 中工作，或者如果其他人真的關心這個結果是否正確。但技術將會變得更好。所以我認為在許多情況下，更明智的做法是等待它變得更容易。而不是花費傳統方式十倍的時間來形式化它，而是花費兩倍的時間。
您甚至談到將這個係數降到小於一。
藉助人工智慧，真正有可能做到這一點。我認為在未來，我們將不會再輸入我們的證明，而是向一些 GPT 解釋它們。GPT 會嘗試在你進行時將其形式化為 Lean。如果一切都檢查完畢，GPT 將[基本上]說，“這是你的 LaTeX 論文；這是你的 Lean 證明。如果你願意，我可以按下這個按鈕併為你將其提交給期刊。” 它在未來可能成為一個出色的助手。
到目前為止，證明的想法仍然必須來自人類數學家，不是嗎？
是的，形式化最快的方法是首先找到人類證明。人類提出想法，證明的初稿。然後你將其轉換為形式證明。將來，事情可能會以不同的方式進行。可能會有合作專案，我們不知道如何證明整個事情。但是人們對如何證明小部分有想法，他們將其形式化並嘗試將它們組合在一起。將來，我可以想象一個大型定理由 20 個人和一群人工智慧共同證明，每個人工智慧都證明小東西。隨著時間的推移，它們將被連線起來，你可以創造出一些美好的東西。那將是很棒的。在很多年之後才有可能實現。這項技術尚未成熟，部分原因是形式化現在非常痛苦。
我曾與一些人交談過，他們嘗試使用大型語言模型或類似的機器學習技術來建立新的證明。託尼·吳和克里斯蒂安·塞格迪最近與埃隆·馬斯克等人共同創立了公司 xAI，他們告訴我，在兩到三年內，數學將被“解決”，就像國際象棋被解決一樣——機器在尋找證明方面將比任何人類都更出色。
我認為在三年內，人工智慧將對數學家有用。它將成為一個偉大的副駕駛。你正在嘗試證明一個定理，並且有一個步驟你認為它是真的，但你不太清楚它是如何成立的。你可以說，“人工智慧，你能為我做這件事嗎？” 它可能會說，“我想我可以證明這一點。” 我認為數學不會被解決。如果人工智慧領域出現另一個重大突破，那是有可能的，但我要說的是，在三年內，你將看到顯著的進步，並且實際使用人工智慧將變得越來越容易。即使人工智慧可以做我們現在所做的數學型別，這也意味著我們將轉向更高型別的數學。所以現在，例如，我們一次證明一個定理。這就像個體工匠製作木偶或其他東西。你拿起一個木偶，非常仔細地繪製一切，等等，然後再拿起另一個。我們做數學的方式並沒有太大改變。但是在每一種其他型別的學科中，我們都有大規模生產。因此，藉助人工智慧，我們可以開始一次證明數百個或數千個定理。人類數學家將指導人工智慧執行各種操作。所以我認為我們做數學的方式會改變，但他們的時間框架可能有點激進。
我在 2018 年彼得·肖爾茨獲得菲爾茲獎時採訪了他。我問他，有多少人理解你在做什麼？他說大約有 10 個人。
透過形式化專案，我們注意到的是，你可以與不瞭解整個專案數學的人合作，但他們瞭解其中很小的一部分。這就像任何現代裝置一樣。沒有人能夠獨自制造一臺計算機，開採所有金屬並提煉它們，然後建立硬體和軟體。我們有所有這些專家，我們有一個龐大的物流供應鏈，最終我們可以製造智慧手機或其他東西。目前，在數學合作中，每個人都必須幾乎瞭解所有的數學，正如 [肖爾茨] 提到的那樣，這是一個絆腳石。但是透過這些形式化，可以將專案分門別類，並且只需瞭解專案的一部分即可做出貢獻。我認為我們也應該開始形式化教科書。如果教科書被形式化，你可以建立這些非常互動的教科書，你可以在非常高的層次上描述結果的證明，假設有很多知識。但是，如果有一些步驟你不理解，你可以展開它們並深入細節——如果你願意，可以一直追溯到公理。目前沒有人為教科書這樣做，因為工作量太大了。但是，如果你已經將其形式化，計算機可以為你建立這些互動的教科書。這將使一個領域的數學家更容易開始為另一個領域做出貢獻，因為你可以精確地指定一個大型任務的子任務，而這些子任務不需要理解一切。
數學證明不僅僅是檢查某件事是否正確。證明也是為了理解某些東西，對嗎？有美麗的證明，也有非常技術性的醜陋證明。一個好的證明能讓你對問題有更高的理解。因此，如果我們將其委託給機器，我們還能理解它們發現了什麼嗎？
數學家正在做的是，我們正在探索什麼是真，什麼是假，以及為什麼事情是真的。我們這樣做的方式是透過證明。每個人都知道，當它是真的時，我們必須嘗試證明它或證偽它。這需要很多時間。這很乏味。但在未來，也許我們只會問人工智慧，“這是真的還是假的？” 我們可以更有效地探索空間，我們可以嘗試專注於我們真正關心的東西。人工智慧將透過加速這個過程為我們提供很大幫助。至少目前，我們仍將是駕駛員。也許 50 年後情況會有所不同。但在短期內，人工智慧將首先自動化那些枯燥、瑣碎的事情。
人工智慧會幫助我們解決數學中尚未解決的重大問題嗎？
如果你想證明一個尚未解決的猜想，你需要做的第一件事就是將其分解成更小的部分，每個部分都有更大的可能被證明。但是你經常會將一個問題分解成更難的問題。將一個問題轉化為比它更難的問題很容易，但轉化為比它更簡單的問題則很難。人工智慧尚未表現出在這方面比人類更好的能力。
透過分解問題並進行探索，你也會在此過程中學到很多新東西。例如，費馬大定理是一個關於自然數的簡單猜想，但為證明它而開發的數學不再僅僅是關於自然數的了。因此，解決一個證明遠不止證明這一個例項。
假設人工智慧提供了一個難以理解、醜陋的證明。那麼你可以與它合作，你可以分析它。假設這個證明使用 10 個假設來得到一個結論——如果我刪除一個假設，證明仍然有效嗎？這是一門尚不存在的科學，因為我們沒有那麼多人工智慧生成的證明，但我認為未來會出現一種新型的數學家，他們將採用人工智慧生成的數學，並使其更易於理解。就像我們有理論科學和實驗科學一樣。我們透過經驗發現了很多東西，然後我們做更多的實驗，我們發現了自然規律。我們現在在數學中沒有這樣做。但我認為會有一個行業的人試圖從最初沒有任何見解的人工智慧證明中提取見解。
因此，這不會是數學的終結，而是數學的光明未來嗎？
我認為未來會出現現在根本不存在的不同數學研究方式。我可以看到專案經理數學家，他們可以組織非常複雜的專案——他們不理解所有的數學，但他們可以將事情分解成更小的部分並委託給其他人，並且他們具有良好的人際交往能力。然後是有在子領域工作的專家。有些人擅長訓練人工智慧進行特定型別的數學，還有些人可以將人工智慧證明轉化為人類可讀的東西。它將變得更像幾乎任何其他現代產業的運作方式。例如，在新聞業中，並非每個人都具備相同的技能。你有編輯、記者和商人等等——我們最終會在數學中擁有類似的東西。
我們所做的數學是與我們的大腦相匹配的數學，不是嗎？如果人工智慧在某些時候變得如此聰明，它可能會進入我們難以理解的領域。
數學已經比任何一個人類頭腦都要大了。數學家通常依賴其他人已經證明的結果。他們有點知道為什麼它是真的，他們有一些直覺，但他們無法將其完全分解到公理。但他們知道在哪裡尋找，或者也許他們認識可以做到的人。我們已經有很多定理只通過計算機驗證，其中一些大規模計算機計算已經檢查了一百萬個案例。你可以手工驗證它，但沒有人有時間去做，而且不值得。所以我認為我們會適應的。一個人不必檢查一切。讓計算機為我們做檢查，這對我來說很好。
在數學前沿，正在發生很多事情，這些事情將看似無關的領域結合在一起，根據我的天真理解，一個瞭解所有這些領域的人工智慧可以給你一個提示，說：“你為什麼不看看那裡？那可能會幫助你解決你的問題。”
人工智慧的一個非常令人興奮的潛在用途是建立聯絡，或者至少指出可能的聯絡。目前，它的成功率非常低。它可能會給你 10 個建議，其中一個是有趣的，九個是垃圾。實際上，它幾乎比隨機的還要糟糕。但這在未來可能會改變。
訓練數學人工智慧的障礙是什麼？
部分問題在於它沒有足夠的資料進行訓練。網上有已發表的論文，你可以用它們來訓練它。但我認為，很多直覺並沒有體現在期刊上發表的論文中，而是體現在與數學家的對話中，體現在講座中以及我們指導學生的方式中。有時我開玩笑說，我們需要做的是讓 GPT 接受標準的畢業教育，坐在研究生課堂上，像學生一樣提問，像人類學習數學一樣學習。
證明的已發表版本總是經過壓縮的。即使你收集了人類歷史上所有已發表的數學成果，與這些模型所訓練的資料相比，仍然很少。
人們只發表成功的故事。真正珍貴的資料來自某人嘗試做某事，但它不太奏效，但他們知道如何修復它。但他們只發表成功的事情，而不是過程。
也許你應該像醫學研究那樣，註冊努力證明某件事。研究人員會註冊它，然後即使它沒有成功，他們也必須發表它。
我們沒有那種文化。也許在未來，形式化將變得非常高效，你也許能夠即時形式化事物。也許如果你想在研究專案中使用 2040 年一些花哨的人工智慧 Lean，並且你想獲得資金來使用這個花哨的人工智慧，你必須同意記錄你嘗試和失敗的過程。然後，這可以用來訓練未來的人工智慧。或者，也許其他一些小組正在研究類似的問題，他們可以看到，“哦，另一個小組嘗試了同樣的事情，但他們失敗了”，這樣你就不會浪費時間犯完全相同的錯誤。
數學家是否浪費了很多時間？
哦，非常浪費。如此多的知識不知何故被困在個體數學家的頭腦中。只有一小部分被明確化。但是，我們越形式化，我們更多的隱性知識就會變得顯性。因此，這將帶來意想不到的好處。
本文最初發表於《Spektrum der Wissenschaft》，經許可轉載。