數學歷來是一門孤獨的科學。

1986 年，安德魯·懷爾斯（Andrew Wiles）為了證明費馬大定理，遁入書齋長達七年之久。

數學家苦心孤詣得到的證明往往讓同行難以理解，有些證明至今仍有爭議。

但近年來，越來越多的數學領域被嚴格分解成各個組成部分，我們稱之為「形式化」（formalized），這就可以讓計算機來檢查和驗證數學證明。

菲爾茲獎得主、加州大學洛杉磯分校教授陶哲軒堅信，這些方法為數學領域的合作開辟了全新的可能性。

如果再加上人工智能的最新進展，在未來幾年里，數學領域可能會出現全新的工作方式。

在計算機的幫助下，一些重大問題可能會被更快解決。

陶哲軒在接受《科學美國人》的德語姊妹刊物Spektrum der Wissenschaft的采訪時闡述了他對未來的看法。

以下是采訪實錄——

「互不信任」的數學家通過AI建立合作

您在舊金山舉行的聯合數學會議上的一次演講中，似乎暗示數學家之間互不信任。您這么說是什么意思？

?

我的意思是，你很難與素未謀面的人合作，除非你能逐行檢查他們的作品。通常情況下，五個人是最多的合作人數。

隨著自動校驗器的出現，這種情況會發生怎樣的變化？

?

現在，你真的可以與數百名素不相識的人合作。你不需要信任他們，因為他們上傳代碼，Lean編譯器就會驗證。你可以做比我們通常做的更大規模的數學。

當我用所謂的多項式（PFR）猜想形式化我們最近的成果時，我與20 多人一起工作。我們把證明分成了很多小步驟，每個人都為其中的一個小步驟貢獻了證明。

我不需要逐行檢查這些貢獻是否正確。我只需要對整件事進行管理，確保一切都朝著正確的方向發展。這是一種不同的數學方式，一種更現代的方式。

陶哲軒借助Lean 4成功完成PFR猜想的證明

德國數學家、菲爾茲獎得主Peter Scholze參與了一個Lean項目，盡管他告訴我，他對計算機并不了解。

?

在這些形式化項目中，并非每個人都需要成為程序員。有些人可以只專注于數學方向，你只是把一個大的數學任務分割成許多小塊；有些人則專門負責把這些小部分轉化為形式化證明。

我們不需要每個人都成為程序員，我們只需要一些人成為程序員。這是一種分工。

Peter Scholze的液體張量實驗采用Lean 3作為項目背后的引擎

Lean將數學「形式化」

20 年前，我聽說過機器輔助證明，當時它還是一個非常理論化的領域。每個人都認為，你必須從頭開始——將公理形式化，然后做基礎幾何或代數，而要想進入高等數學，這超出了人們的想象。是什么讓形式數學變得實用？

?

變化之一是標準數學庫的開發。尤其是Lean。

有一個名為mathlib的龐大項目，所有本科數學的基本定理，如微積分和拓撲學等，都被一一收錄到這個庫中。

人們已經投入了大量的工作，將公理提升到相當高的水平。我們的夢想是把數學庫真正提升到研究生教育的水平。這樣，數學的形式化就會容易得多。

我們還期待有更好的搜索方法，因為如果你想證明某件事情，你必須能夠找到有關的已經被證實為真的東西。因此，開發真正智能的搜索引擎也是一項重大的新進展。

所以這不是計算能力的問題？

?

不，一旦我們正式確定了整個PFR項目，編譯驗證只需要半個小時。這并不是瓶頸，瓶頸在于如何讓人類使用它，如何提高可用性和用戶友好度。

現在，我們已經有了一個由數千人組成的大型社區，而且還有一個非常活躍的在線論壇來討論如何讓這門語言變得更好。

Lean是目前最先進的系統，還是有其他與之競爭的系統？

?

Lean可能是最活躍的社區。對于單作者項目來說，也許有其他一些語言略勝一籌，但總體而言，Lean更容易上手。而且它有一個非常不錯的庫和一個不錯的社區。它最終可能會被其他語言取代，但現在它是主流的正式語言。

形式化數學的困境和發展

當你談論一個不同的數學項目時，有人曾問你是否想把它形式化，你基本上是說這需要太長時間。

?

我可以將其形式化，但這需要花費我一個月的時間。現在，我認為我們還沒有到把所有事情都進行形式化的地步，你必須精挑細選。但技術會越來越好。

因此，我認為在很多情況下，更明智的做法是等到它變得更容易的時候再去做。與其現在花10倍的時間去形式化，不如等待形式化技術的發展，到只需要傳統方法一半時間的時候，再去使用。

你甚至說過要把這個系數降到1以下（形式化不比傳統方法更費時）。

?

人工智能確實有可能做到這一點。我認為，在未來，我們不用再把證明打出來，而是直接與某個GPT交互。而GPT會在你進行的過程中，嘗試用Lean將其形式化。

如果一切順利，GPT 會說：「這是你的LaTeX論文，這是你的Lean證明，如果你愿意，我可以按下這個按鈕，幫你把它提交給期刊」。未來，它可能會成為一個出色的助手。

到目前為止，證明的想法仍然必須來自人類數學家，不是嗎？

?

是的，形式化的最快方法就是先找到人類的證明。人類提出想法和證明的初稿，然后再把它轉換成形式化的證明。

在未來，也許情況會有所不同。可能存在一些我們不知道如何證明整個事情的合作項目，但人們已經有了如何證明小部分內容的想法，他們會把這些想法形式化，并嘗試把它們組合在一起。

我可以想象，將來一個大定理會由20個人和一群AI共同證明。隨著時間的推移，它們會建立聯系，你就能創造出一些奇妙的東西。

這將是偉大的，但要實現這一點，還需要很多年。技術還不成熟，部分原因是形式化現在非常痛苦。

馬斯克等人共同創辦的xAI公司，他們告訴我，兩三年后，數學將像國際象棋一樣被「解決」——機器將比人類更擅長尋找證明。

?

我認為，三年后，AI將對數學家有用，它將成為一個出色的co-pilot（副駕駛員）。

你試圖證明一個定理，有一步你認為是正確的，但你不太明白它是如何正確的，你可以說，「人工智能，你能幫我做這個嗎？」 它可能會說 「我想我能證明這一點」。

但我不認為數學會被「解決」。如果AI再有重大突破，那是有可能的。

但我想說的是，在三年內，你會看到顯著的進步，而且實際使用人工智能會變得越來越容易管理。

舉例來說，現在我們一次證明一件事。這就像工匠們在制作木制玩偶之類的東西。你拿起一個玩偶，非常仔細地給所有東西上色，然后再拿起另一個。

我們做數學的方式并沒有多大改變。但其他所有學科中都存在批量生產。

有了AI，我們可以一次證明數百或數千條定理，人類數學家將指導AI做各種事情。因此，我認為研究數學的方式將會改變，但他們（xAI）的時間框架可能有點激進。

2018年Peter Scholze獲得菲爾茲獎時，我采訪了他。我問他，有多少人理解你在做什么？他說大約有10人。

在形式化項目中，我們注意到，你可以與那些不理解整個項目但理解其中一部分的人合作。

這就像任何現代設備一樣。沒有一個人可以獨立制造一臺計算機，開采所有的金屬并加以提煉，然后制造硬件和軟件。我們擁有不同方向的專家，我們有龐大的物流供應鏈，最終我們可以制造出智能手機或其他產品。

現在，在數學合作中，每個人都必須知道幾乎所有的數學知識，正如Scholze提到的，這是一個絆腳石。

但是，有了形式化驗證的方法，我們就有可能把一個項目分門別類，只需要知道其中的一部分就能為項目做出貢獻。

我認為我們還應該開始將教科書形式化，這樣可以有更強的交互性。

你可以假定其中包含很多知識，從非常高層次的意義上描述一個結果的證明。但如果有一些步驟你不理解，你可以擴展它們并深入細節，可以一直深入到公理級別。

然而現在沒有人在教科書中這樣做，因為太費事了。但如果你已經將其形式化，計算機就可以為你創建這些交互式教科書。

這將使一個領域的數學家更容易開始為另一個領域做出貢獻，因為你可以精確地指定一個大任務的子任務，而不需要理解所有的東西。

數學家與AI互動

數學證明不僅僅是為了證明某件事情是正確的，也是為了理解某些東西，對嗎？有優美的證明，也有技術性很強但卻丑陋的證明。好的證明能讓你對問題有更深的理解。那么，如果我們把這個任務交給機器，我們還能理解它們發現的東西嗎？

?

數學家正在做的是，探索什么是真的，什么是假的，以及為什么事情是真的。我們的方法就是通過證明。

每個人都知道，當它是真的時候，我們必須去嘗試證明它或反駁它，這需要很多時間，也很乏味。

但在未來，也許我們只需要問AI「這是真的還是假的」？

這樣我們就能更有效地探索這個空間，我們就能把精力集中在我們真正關心的事情上。AI將加速這一過程，為我們提供很大幫助。

我們仍然要自己「駕駛」，AI只是co-pilot，至少現在是這樣，也許50年后情況會有所不同。但在短期內，人工智能將首先把無聊、瑣碎的事情自動化。

人工智能能否幫助我們解決數學中尚未解決的重大問題？

如果你想證明一個尚未解決的猜想，首先要做的一件事就是把它分解成更小的部分，每個部分都有更大的機會被證明。

但你往往會把一個問題分解成更難的問題。將一個問題轉化為更難的問題比轉化為更簡單的問題要容易得多。在這方面，人工智能并沒有表現出比人類更好的能力。

在分解問題和探索問題的過程中，你也會學到很多新東西。例如，費馬大定理是一個關于自然數的簡單猜想，但為證明它而發展的數學卻不一定是關于自然數的了。因此，解決證明問題遠不止證明這一個實例。

假設人工智能提供了一個難以理解的、丑陋的證明。那么你就可以使用它，分析它。假設這個證明使用了10個假設來得到一個結論，你可以這樣思考——如果我刪除一個假設，這個證明還有效嗎？

這是一門還沒有真正存在的科學，因為我們還沒有那么多人工智能生成的證明，但我認為將會出現一種新型數學家，他們會利用人工智能生成的數學，使其更易于理解。

就像我們有理論科學和實驗科學一樣。我們通過經驗發現了很多東西，但隨后我們做了更多實驗，發現了自然規律。

我們現在的數學還做不到這一點。但我認為，未來會有一批人試圖從人工智能證明中提取洞察力，而這些證明最初并沒有任何洞察力。

因此，與其說這是數學的終結，不如說是數學的光明未來？

?

我認為會有不同的方法來研究數學，只是這些方法目前還不存在。

我可以看到項目經理式的數學家，他們可以組織非常復雜的項目，他們不能理解全部的數學，但他們可以把事情分成小塊，然后委托給其他人，他們有很好的人際交往能力。

此外，還有一些在子領域工作的專家。有些人擅長在特定類型的數學上訓練人工智能，有些人則能將人工智能的證明轉化為人類可讀的東西。

數學領域的運作方式將變得更像幾乎任何其他現代行業。比如，在新聞業，并不是每個人都擁有相同的技能，于是有各種職業分工，編輯、記者、商務經理等等。這個領域最終也會出現類似的情況。

我們所研究的數學就是與我們的大腦相匹配的數學，不是嗎？如果未來人工智能變得如此聰明，會不會讓人類數學家難以理解？

?

數學已經超越了任何一個人類的思維。數學家通常依賴別人已經證明的結果。他們知道為什么它是真的，他們有一些直覺，但他們不能把它分解成公理。但他們知道去哪里找，或者他們知道誰能找到。

我們已經有很多定理只能通過計算機來驗證，一些龐大的計算機計算已經檢查了一百萬個案例。你可以手工驗證，但沒人有時間去做，也不值得。

所以，我認為我們會適應的。一個人沒有必要檢查所有的東西。讓電腦來幫我們核對，這對我來說很好。

在數學的最前沿，有很多看似毫不相干的領域的東西被整合在一起，根據我粗淺的理解，一個了解所有這些領域的人工智能可以給你一個提示，然后說：「你為什么不看看那里呢？這也許能幫你解決問題」。

?

利用人工智能建立聯系或至少指出可能的聯系，這是一個非常令人興奮的潛在用途。現在，它的成功率很低。它可能會給你10 建議，其中1個是有趣的，9個是垃圾。實際上，這幾乎比隨機還糟糕。但這在未來可能會改變。

訓練數學人工智能會遇到哪些問題？

?

部分問題在于它沒有足夠的數據來進行訓練。網上有一些發表的論文，可以用來訓練。但我認為，很多靈感并不是在期刊上的論文中捕捉到的，而是在與數學家的對話、講座以及我們給學生提供建議的過程中捕捉到的。

有時我開玩笑說，我們需要做的是讓GPT接受標準的研究生教育，坐在研究生課堂上，像學生一樣提問，像人類學習數學一樣學習。

公開發表的證明總是濃縮的。即使把人類歷史上發表過的所有數學知識都算上，與這些模型所需要的訓練數據相比，仍然是小巫見大巫。

?

人們只發表成功的故事，但真正珍貴的數據來自于嘗試。可能起初不太成功，但解決的過程更有價值。然而，大家只公布成功的研究結果，不公布研究的過程。

也許我們應該對證明某事的努力進行登記，就像醫學研究一樣。研究人員將證明進行登記，即使沒有成功，他們也必須將其公布于眾。

?

我們沒有這種文化。也許在未來，形式化會變得非常高效，你可以實時地將事情形式化。

如果你想在一個研究項目中使用某個2040年的高級人工智能Lean，并想獲得資金來使用這個高級人工智能，你必須同意你的嘗試和失敗過程都會被記錄下來。

然后，這可以用來訓練未來的人工智能。或者，其他小組也在研究類似的問題，他們可以看到「哦，其他小組也嘗試過同樣的事情，但他們失敗了」，這樣你就不必浪費時間犯一模一樣的錯誤了。

數學家是否在浪費大量時間？

?

的確如此。如此多的知識不知何故被困在個別數學家的頭腦中，只有極少部分被清楚地呈現。我們越是形式化，越多的隱性知識就會顯性化，這將帶來意想不到的好處。

本文轉自 新智元 ，作者：新智元

原文鏈接:??https://mp.weixin.qq.com/s/1C5b4EI5PU51DJ4ryCV4aQ??