---

??新智元報道??

數(shù)學歷來是一門孤獨的科學。

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

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

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

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

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

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

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

以下是采訪實錄——

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

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

隨著自動校驗器的出現(xiàn)，這種情況會發(fā)生怎樣的變化？

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

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

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

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

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

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

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

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

變化之一是標準數(shù)學庫的開發(fā)。尤其是Lean。

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

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

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

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

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

現(xiàn)在，我們已經(jīng)有了一個由數(shù)千人組成的大型社區(qū)，而且還有一個非?；钴S的在線論壇來討論如何讓這門語言變得更好。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

我們?nèi)匀灰约骸格{駛」，AI只是co-pilot，至少現(xiàn)在是這樣，也許50年后情況會有所不同。但在短期內(nèi)，人工智能將首先把無聊、瑣碎的事情自動化。

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

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

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

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

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

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

就像我們有理論科學和實驗科學一樣。我們通過經(jīng)驗發(fā)現(xiàn)了很多東西，但隨后我們做了更多實驗，發(fā)現(xiàn)了自然規(guī)律。

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

因此，與其說這是數(shù)學的終結(jié)，不如說是數(shù)學的光明未來？

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

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

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

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

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

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

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

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

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

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

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

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

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

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

人們只發(fā)表成功的故事，但真正珍貴的數(shù)據(jù)來自于嘗試?？赡芷鸪醪惶晒Γ鉀Q的過程更有價值。然而，大家只公布成功的研究結(jié)果，不公布研究的過程。

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

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

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

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

數(shù)學家是否在浪費大量時間？

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

https://www.scientificamerican.com/article/ai-will-become-mathematicians-co-pilot/