西風 發自 凹非寺
量子位 | 公眾號 QbitAI
陶哲軒最新演講公開，AI含量爆表。
在IMO 2024現場，「陶神」帶來了洋洋灑灑1個小時的精彩分享，主題就叫：AI與數學
。
他怎麽看AI和數學的關系？怎麽理解機器學習、大模型等在數學領域的套用與發展？
所有觀察和觀點都毫無保留分享：
借助AI，可以想象未來可以取一類1000個問題同時處理，你真的可以開始以一種前所未有的規模進行數學研究。
除此之外，「陶神」還由古至今講述了機器輔助計算的傳統與演變。
AI等一系列機器在數學研究中的妙用並非空口無憑：
畢達哥拉斯三元陣列的問題只能使用電腦解決
克卜勒猜想最終也是借由電腦輔助證明
機器學習在紐結理論中的套用：已經能夠幫助猜測兩種不同統計數據之間的聯系
他本人還透露，自己用GPT-4
找解題靈感；用GitHub Copilot
輔助證明，大概有20%機率，它能寫出接近正確的下一步證明。
不光是在演講中講AI，陶哲軒最近釋出的幾個貼文也都和AI息息相關。
網友紛紛安利：
他沒有支持或反對AI炒作，而只是理性開放地評估了這些工具及其能力，還有未來可能發生的事。
量子位在不改變原意的基礎上，對「陶神」這次最新的演講內容進行了編譯整理。
「陶神」從機器輔助計算的傳統開始講起，又接著講了大致以下幾個板塊的內容：
電腦起初最基本的用途
機器在科學計算中的套用
現代用機器進行數學研究的創造性方法：證明助手、機器學習、大語言模型
長期以來就有機器輔助計算的傳統
你們都聽說過AI以及它如何改變一切。早些時候有一個DeepMind釋出了一個AlphaGeometry，現在可以回答一些IMO幾何問題。
我將更多地討論這些工具是如何開始改變數學研究的
。
這與數學競賽不同，不是設定三個小時什麽的來解決一個問題，而是需要幾個月甚至更長時間，有時解決不了問題，那就必須改變問題。這絕對不同於數學競賽，盡管在技能上有些重疊。
這一切都非常令人興奮，它正在開始具有變革性。但另一方面，也有一種連續性的感覺，我們實際上已經使用電腦和機器來做數學運算很長時間了，而我們進行這些運算的方式的本質正在發生變化。
但實際上，這是遵循了長期以來機器輔助的傳統。
那麽，問題來了。我們使用機器來做數學已經有多久了？答案是數千年。
這是羅馬人曾經用來做數學的機器，算盤是早期的機器，甚至還有一些更早的。聽起來可能有點無聊，這些並不是非常智慧的機器。
電腦呢？我們使用電腦做數學多久了？大約是三四百年。這有點奇怪，因為你知道，我們的電子電腦直到20世紀三四十年代才出現。
但在電子電腦之前，電腦曾經是機械式的，電腦也曾指進行計算的人，是一種職業。
曾經有人力「電腦集群」，人使用加法機計算彈道學等問題，計算能力的基本單位不靠CPU，而是kilgirl，即1000名女性1小時可以完成多少計算任務，當時男人們都在打仗。
電腦最基本的用途是制作表格
人們很早就在使用電腦，正如我之前所說，實際上早在17世紀甚至更早之前就開始使用了。
那時電腦最基本的用途是制作表格（table），你可能聽說過納皮爾的對數表
。
如果你想計算正弦、余弦等，你會使用電腦生成這些表格。我高中上課時仍會學習如何使用這些表格，它們剛剛被淘汰。
當然，現在我們有小算盤和現代電腦。
我的意思是，在數學研究中，我們依賴於表格，現在我們稱它們為資料庫
，但它們本質上還是一樣的東西。
在數學中有許多重要的成果最初是透過表格發現的。
例如，數論中最基本的成果之一——質數定理
。它大致告訴你在一個大數x之前有多少個質數，這一發現歸功於勒壤得和高斯等人。
當時他們雖未能證明它，但由於高斯和其他人使用了早期的計算裝置，他們推測這一理論是正確的。實際上，高斯自己就像一個電腦一樣
，計算表格並嘗試找出規律。
之後還出現了另一個重要猜想——Birch and Swinnerton-Dyer猜想
，這裏不詳述。這個猜想也是人類透過檢視大量關於曲線的數據表格然後首次發現的。
如今，包括我在內的許多數學家使用的一個表格，是所謂的Online Encyclopedia of Integer Sequences
（OEIS），它收集了大量數學序列數據。
也許你遇到過它，像「1, 1, 2, 3, 5, 8,13」，你知道這是費氏數列，OEIS是一個資料庫，有成千上萬這樣的序列。
在數學研究中，數學家經常會遇到一些自然出現的數位序列，這些序列可能依賴於變量n，如空間的維數、集合的基數等。
你可以計算這些序列的前五個、六個或十個數位，然後將其輸入到OEIS中進行比較。如果幸運的話，這個序列可能已經被別人放在那裏了，可能來源於對某個完全不同的數學問題的研究。
這樣的發現可以大大提示兩個問題之間可能存在的聯系，許多研究就是這樣開始的。
機器在科學計算中的套用
機器在數學領域的另一個重要套用是科學計算
（scientific computation）。
當你需要執行大規模計算時，你會將大量的算術運算任務丟給電腦。自1920年代以來，這一做法已廣泛被采用。
也許第一個真正進行科學計算的人是亨德瑞克·勞侖茲
。
我記得是荷蘭人想要建一個巨大的堤壩，委托他想弄清楚水流會怎樣變化。所以他們必須建立模型和一些流體方程式，勞侖茲實際上使用了一群人類「電腦」來解決這個問題，采用了浮點運算。
他意識到，如果你想讓很多人很快地完成大量計算，你應該用浮點數來表示各種不同大小的數位。當然，我們現在使用電腦來模擬各種事物。
如果你在解決許多線性方程式或者不同的方程式，你可能想進行一些組合計算，也可以解決代數問題。你在IMO中看到的許多幾何問題原則上都可以透過科學計算來解決。
有一些代數軟體包，你可以將任何幾何問題，比如涉及10個點和一些線和圓的問題，轉化為一個包含20個實數和20個未知數的方程式系統，然後輸入到如Sage
或Maple
等軟體中。
不過，隨著問題規模的擴大，解決問題的計算復雜性可能會呈指數級或雙指數級增長，會超出傳統電腦代數軟體包的處理能力。
因此直到最近，還不可能僅用標準的電腦代數軟體包來暴力解決這些問題。但現在有了AI的輔助，情況可能有希望改變。
另一種強大的科學計算型別是所謂的SAT求解器
，可以用來解決某種邏輯謎題。
例如，你有1000個或真或假的陳述，而且你知道如果第三個陳述是真的，第六個陳述也是真的，那麽第七個陳述必然是假的。如果你給出了一系列這樣的約束條件，SAT求解器就會嘗試利用所有這些資訊，來得出例如能否證明這些陳述中的某些是對還是錯等結論。
還有一個更高級的版本稱為SMT求解器
。如果你有一些變量x、y、z，並且假設一些定律等等，你可以將這些定律和一些其它事實輸入進去，嘗試簡單暴力地在有限的假設中得出結論。
這些非常強大，但也不能很好地擴充套件。再次強調，問題的復雜度可能使運算時間呈指數增長，因此一旦超過大約1000個命題，對這些求解器來說，再執行就變得非常非常困難。
不過，電腦實際上可以解決一些問題。
例如，一個成功案例是在組合數學中的套用，我認為人類在沒有幫助的情況下解決這個問題是不可能的，也許只能透過電腦解決。
問題關於畢達哥拉斯三元組
（勾股陣列）：
將自然數塗成紅色或藍色兩種顏色，無論怎樣塗色，是否總有一種顏色包含畢達哥拉斯三元組abc？
此問題以前並未得到驗證，直到一台大型電腦進行計算之後才被解決。
現在我們知道，你無需檢查所有自然數。
對於自然數1到7824，可以將其分為兩種顏色，其中任何一種顏色中都不包含畢達哥拉斯三元組。但對於自然數1到7825，是一定會包含的。
我認為這是當時世界上最長的證明，現在是第二長的證明了。這個證明需要4個CPU年的計算時間，並且最終生成了一個包含200TB數據的證明檔，該檔後來被壓縮至86GB。
所以這是使用電腦的一種相當明顯的方式。
現在使用電腦研究的三種創意方式
最近幾年，我們開始用更具創造性的方式使用電腦，特別是將它們與彼此以及更傳統的資料庫、表格、科學計算相結合。
我們使用機器學習
神經網路以不同於人的方式來發現新的聯系，找出不同型別的數學之間的相關方式。
最引人註目的是大語言模型
，它可以進行自然語言對話，像ChatGPT、Claude等，有時它們可以產生解決問題的有效方法。
還有另一種技術被數學家們使用——形式證明助手
（formal proof assistants）。
這些工具本質上是程式語言，就像你使用電腦語言編寫可執行程式碼一樣，形式證明助手是用來檢驗事物的語言，它們幫助你驗證某個論證是否真實，並從數據中得出結論。
最近這些工具的使用變得相對易用，且正在助力許多有趣的數學計畫，這些計畫在沒有形式證明助手的幫助下是不可能實作的。
未來，它們將與我提到的其它工具很好地結合起來。
所以我想談談使用現代電腦和機器進行數學研究的方法，從證明助手開始。
證明助手
第一個真正的電腦輔助證明也許是四色定理
的證明。
這個定理在1976年得到了證明：任何一張地圖只用四種顏色進行著色，就能使相鄰區域的顏色不相同。
△圖源維基百科
他們證明四色定理的方式基本上是對國家數量進行歸納。你需要展示如果你有一張龐大的地圖，那麽就會存在一些國家的子圖，他們列出了大約1000到2000個特殊的子圖，每一個龐大的國家圖在某種意義上都必須包含這些子圖中的至少一個，這是他們必須檢查的一件事。
然後他們必須檢查每當你有一個子圖時，你可以用更簡單的東西替換這個子圖，如果你能用四種顏色來著色這個更簡單的東西，你就能給主圖著色。
還有可簡化性，對於這些子圖中的每一個都要進行檢查。
這些任務中的一些可以由電腦完成，還有一些任務是人工花費數小時手動檢查的。
我認為，這是一個需要重新審視的過程，它非常乏味，並且過程並不完美，存在許多小錯誤。按照現代的電腦證明標準，這並不是一個可以被電腦驗證的證明。
這種情況直到90年代才有所改變，那時出現了一個使用大約700個子圖的更簡單的證明。
2005年，使用Coq
證明輔助工具，實作了完全形式化的電腦可驗證證明。
我們可以看到，從首次證明出現到我們實際上能夠完全透過電腦驗證之間有一個巨大的差距。
另一個著名的例子是關於球體最密堆積的幾何問題——克卜勒猜想
。
克卜勒猜想稱，在三維空間中，最密的球體排列方式是面心立方堆積（FCC）和六方最密堆積（HCP）。這兩種排列方式的球體占據的體積比約為74.048%，這是所有可能的排列方式中最大的。
△圖源維基百科
怎麽確定這種堆積方式是否是最好的？這成為一個特別難的問題，並沒有一個完全對人類可讀的猜想證明。
問題在於，對於無窮多的球體，密度是一個漸進的事情，所以它不是一個先驗的有限問題，你不能僅僅把它扔給電腦來解決。
但是你可以試著把它簡化為有限的問題。
每次進行堆積時，它會將空間細分為被稱為Voronoi區域的多面體。球的Voronoi多面體就是所有距離該球中心最近的點所組成的區域，這些多面體都有特定的體積，你還可以計算它們的面數和表面積等，並因此獲得這些統計數據。
Toth在20世紀50年代提出了一種策略。他觀察到某些加權不等式基於有限多個Voronoi多面體的體積能得到球堆積密度的上界
。
你可以嘗試建立這些多面體之間的關系，比如，如果一個多面體非常大，可能會迫使附近的多面體變得非常小，因此你可以嘗試找到一些連線一個多面體的體積與另一個多面體的體積的不等式。
許多研究者嘗試過這種方法，有些甚至聲稱成功，但沒有一個得到認可能作為確切的證明。
最終，這個問題由Thomas Hales
及其合作者解決。他采用了基本相同的策略，但加入了許多技術性調整。
他們把Voronoi單元改進得更精細，並不只是簡單測量體積，而是創造了一個綜合得分，將體積和多個小的臨時調整結合起來。他的目標是在這些不同得分之間建立線性不等式，從而最終得到密度的上限，並希望精確地達到最優密度。
這種方法極具靈活性，但也因為可嘗試的方案過多而顯得過於復雜。
Thomas Hales和其學生Samuel Ferguson
意識到，每次他們在解決最小化問題時遇到困難，都能調整評分函式來回避這些困難。函式變得更加復雜，每次更改都可能花費很長時間。
更糟糕的是，這個函式與之前論文中的內容略有不相容，就需要回頭去修改之前的論文。
最初，他們並沒有計劃依賴電腦，但隨著計畫變得越來越復雜，必須越來越多地依賴電腦處理
。
到1998年，他們最終宣布該計畫成功，從一個精心選擇的包含150個變量的最佳化問題中，透過線性規劃計算得出了克卜勒猜想的證明。
證明包括了250頁的筆記和3GB的電腦程式、數據和結果。
這個證明在稽核過程中遇到了重大困難。它被送出給了一些頂尖的數學期刊，評審過程耗時四年，由一個專家小組負責。
在評審結束時，他們表示對證明的正確性有99%的把握，但他們無法確認電腦計算的正確性
。他們采取了一種非常不尋常的做法，即在發表論文時添加了一個註釋來說明這一點。後來，他們撤銷了這個註釋。
當時，是否接受電腦輔助證明作為正式證明存在很大爭議。現在，我們對此更加自信，但即便在論文發表後，關於其是否真正構成證明仍有疑問。
因此，這可能是第一個真正需要將問題完全按照基本原則形式化的高知名度案例。為此，Hales開發了一種語言，稱之為Flyspeck計畫
。
他最初估計需要20年來形式化他們的證明，但實際上，在21位合作者的幫助下，他僅用了12年時間就完成了。最終，這一成果在2014年公布。
因此，我們現在對這一結果充滿信心。
我們已經開始探索更好的工作流程來進行形式化，雖然這一過程仍然很繁瑣，但正在逐步改進。
Peter Scholze
是一位非常傑出的年輕數學家，他因許多成就而聞名，尤其是建立了一個被稱為「濃縮數學
」的數學領域。
這個領域利用代數、範疇論及其它代數工具，來解決傳統上抵抗代數方法的泛函分析和函式空間理論等問題。
Scholze建立了包括所謂的濃縮abelian群和向量空間的一整套範疇。他的主要觀點是，我們在研究生課程中學習的所有關於函式空間的分類都是不準確的，或者它們不是最自然的，而他提出的分類具有更好的內容。
然而，有一個非常重要的消失定理他需要證明。這個定理的證明涉及到某個範疇理論群的非常技術性的計算。因此，這成為了他理論的基礎。
他在一篇部落格文章中討論了這一結果，提到他花了一整年時間沈迷於這個定理的證明，幾乎陷入瘋狂。最終，他們設法將論證印刷在紙上，但沒有人敢深入探查這些細節，所以他仍然有持續的疑慮。
有了這個定理，這種濃縮公式在泛函分析中的套用才站得住腳。這極為基礎且重要，因此，99.9%的確定性還不夠。
世界各地有許多關於濃縮數學的研究小組，但他們都未能完成這個定理的證明。這個證明過程並不有趣，所以他說這可能是他最重要的成就，但必須確保其正確性。
後來，使用了一種更現代的、稱為Lean
的程式語言。
Lean是近些年發展起來的一種語言，它是一個眾包計畫，旨在開發龐大的數學庫。與其從數學的基本公理推導一切，這個庫已經證明了許多中間結果，如本科數學課程中可能會看到的基礎群論、拓撲學等主題，這些已經被形式化了。
但為了形式化這個理論，他們不得不添加許多額外內容，盡管數學庫還不完整，仍有很多領域，如同調代數、層理論等需要添加到庫中，但在短短18個月內，他們形式化了這個定理。
證明基本正確，盡管存在一些小的技術問題，但沒有發現重大錯誤，他們找到了一些簡化的技巧，有些技術步驟過於復雜而難以形式化，因此他們被迫尋找了一些捷徑。
實際上，這個計畫的價值更多的是間接的。
首先，他們大大豐富了Lean數學庫。現在，這個數學庫可以處理大量的抽象代數，遠遠超過了以前的能力。此外，還有其它支持軟體被建立起來，例如blueprint
（藍圖）。
直接形式化一個龐大的證明，比如50頁的證明，真的很痛苦，你必須把整個證明記在腦海中。
正確的工作流程是，你拿一個大的證明，首先編寫一個blueprint，它將這個證明分解成數百個小步驟。每一步都可以單獨形式化，然後再將它們全部組合起來。你的團隊中不同的人可以在不同的步驟中形式化論證不同部份。
這個計畫的另一個成果是，現在我們有了一個由數萬行程式碼組成的形式化證明。目前正在努力將這個證明轉換為人類可讀的格式。此外，還開發了一些工具，可以將用Lean這種語言編寫的證明轉換回人類可讀的形式。
例如，這裏有一個拓撲問題的證明，它已被成功轉換為人類可以理解的格式。
因此，這些文本都是從形式化證明中電腦生成的。它看起來像是人類編寫的證明，使用了相同型別的數學語言，但更具互動性。
你可以點選任何位置，系統會告訴你當前的假設、你正在嘗試證明什麽、變量是什麽。如果某個步驟太簡短，你可以展開它以了解其來源，並且可以深入到你想要的公理。
我認為這是非常好的創新，我相信未來我們編寫的教科書將采用這種互動式風格，首先進行形式化，然後你將擁有比現有教科書更具互動性的版本。
受此啟發，我自己也開始了一個形式化的計畫。
去年，我與包括Tim Gowers在內的幾個人一起解決了一個組合學問題。它涉及到一個具有「小倍增」性質的二進制Hamming立方體的子集，這個子集的大小有一定的限制。
我們在相對較短的時間內將其形式化，證明大約有33頁長。
實際上，這可能仍是迄今為止最快完成形式化的實際研究論文，在三周內由大約20人的團隊完成，利用了Scholze計畫中開發的所有這些blueprint。
因此，它使得證明任務變得更加開放，協作性更強，你還可以獲得精美的視覺化效果。
正如我所說，你要做的第一件事是把你的大定理分解成許多小塊。我們得到的定理稱為PFR
，對應於這裏圖表底部的一個小圈。
然後我們引入了所有這些其它證明，PFR證明必須依賴於幾個先前的證明
。
因此，存在一個依賴圖，它們的顏色取決於你是否已經形式化它們。綠色圈是一個已經用形式化證明的，藍色圈是尚未被形式化證明，但已準備好被形式化，比如所有定義都已到位。白色圈，即使證明還沒有被形式化，必須有人編寫。
因此，你得到了這個任務樹，而這個計畫的美妙之處在於你可以讓所有這些人獨立地在這張圖的不同部份上協作。
參與者中有些人甚至不是數學家，他們是電腦程式設計師，但他們非常擅長做這些小型拼圖式的事情。每個人都選擇了他們認為能做的一個圈，並最終在三周內完成了整個計畫，這是一個非常激動人心的計畫。
你知道，在數學領域，我們通常不會與這麽多人合作，我見過的最多是5個人。這是因為當你在一個大計畫上合作時，你必須信任每個人的數學都是正確的，超過一定規模，這就變得不可行。
但有了這樣一個計畫，Lean編譯器會自動檢查
，你不能上傳任何無法編譯的內容，所以你可以與你從未見過的人合作。
這是一個例子，我認為這將成為未來進行數學研究的一種越來越普遍的方式。
雖然工具正在改進且變得更加使用者友好，但仍然很痛苦，且需要具備一定的編程專業知識。
另一方面，如果你需要修改你的證明，比如，這個定理中原來有一個12，後來要把12改進成11，從而得到了一個稍強一些的定理。
通常情況下，如果你這麽做，你必須重寫整個證明，或者嘗試將12替換為11但接下來還必須檢查在此過程中是否有其它錯誤。
但實際上，當我們對這個過程進行形式化後，只用了幾天時間就把12改為11，我們只是在某個地方將12改為11，然後Lean在大約五個地方報錯。
目前實際上有不少大型證明形式化計畫正在進行中，也許最大的是Kevin Buzzard
的計畫，他剛剛獲得了一筆巨額資金用於將費馬大定理
在Lean中形式化。
他說這個計畫最重要的部份將需要五年時間來完成，但他沒有聲稱五年內能完成全部，很有趣。
所以這是形式化證明助手的一個套用。
機器學習
接下來我將談談機器學習。
機器學習使用神經網路來預測各種問題的答案，這些答案可以在許多領域中使用。不過，我將跳過我最初討論的使用神經網路猜測偏微分方程式解的方法。
我想談談機器學習在結理論
中的套用。
結理論是數學中一個相當有趣的領域，它匯集了許多不同的數學分支。
結就是空間中閉合的一圈繩索或曲線。如果有辦法可以連續地將一個結變形為另一個結，並且在這個過程中繩索不允許自我交叉，那麽這兩個結就被認為是等價的。
△圖源維基百科
因此，結理論中的基本問題是：兩個結何時是等價的？兩個結，是否有辦法將一個轉變為另一個？
通常解決這個問題的方法是開發所謂的結不變量
。
這些可以是各種數值，有時也包括多項式，你可以將這些數值或多項式附加到一個結上，無論你如何連續變形結，這些數值都不會改變。因此，如果兩個結具有不同的不變量，它們就不能被認為是等價的。
存在許多型別的結不變量。有一種稱為簽名的不變量，你可以平展結並計算交叉點無論交叉是向上還是向下，並據此建立一個特定的矩陣等。
有一些著名的多項式，如瓊斯多項式、亞歷山大多項式，這些與許多數學領域有關。
還有一種是所謂的雙曲不變量，來自幾何學。
你可以取結的補空間，這通常被稱為雙曲空間，它具有一定的幾何結構，有距離概念，你可以保留它的體積和其它一些不變量。因此，這些不變量是實數或復數，每個結都帶有一些組合不變量，如簽名、雙曲幾何不變量等。
這裏有一系列帶有各種雙曲變量的結，有些被稱為雙曲體積等。
盡管已知存在兩種不同的方法來生成關於結的統計數據，但之前沒有人能發現這兩種方法之間有任何聯系或共同點。
直到最近，人們開始使用機器學習來解決這個問題。
他們建立了包含數百萬個結的資料庫
，然後在這個資料庫上訓練了一個神經網路。結果發現，訓練後的神經網路能夠利用所有的雙曲幾何不變量，並且在大約90%的情況下能正確預測簽名。
因此，他們建立了這個黑盒子，它能告訴你簽名以某種方式隱藏在這些幾何變量中，但它並不告訴你這是如何做到的。這仍然很有用，因為一旦你有了這個黑盒子，你就可以隨意操作它。
接下來他們進行的實際上是一種非常簡單顯著性分析。這個黑盒子接收大約20種不同的輸入，其中一種是你的變量型別，並輸出一個結果，即簽名。
在他們發現20個輸入中，只有三個實際上在輸出中起了重要作用，包括縱向平移以及子午線平移的實部和復部。
一旦他們確定了哪些變量最重要，他們可以直接將簽名與這三個特定輸入進行比較，然後人類判斷來確定。
透過觀察這些圖表，他們提出了一個猜想，結果是錯誤的，他們實際上又使用神經網路來證明它是錯誤的。
透過失敗，他們又提出了一個修正版本，是一個解釋了這一現象的正確命題。因此，他們擁有了一個理論解釋，闡述了為什麽簽名與這些特定的統計數據如此密切相關
。
我認為這體現了機器學習在數學領域套用的增長趨勢。它雖然不能直接解決問題，但能提供許多有價值的線索
，指明數據間潛在的聯系以及研究的方向，建立這些聯系的工作仍需人類來完成。
大語言模型
最後，我們有大語言模型，這些是最引人註目的，可能也是最有新聞價值的。你知道，神經網路已經存在了20年，語言模型大概存在了5年左右，但它們只是最近才達到了與人類相似的輸出水平。
你們可能都聽說過GPT-4。GPT-4釋出時，有一篇非常著名的論文描述了它的能力，並且它確實匹配這些能力。
這是一個來自2022年IMO的稍微簡化版本的問題，對於這個特定的問題，系統給出了一個完整且正確的解決方案。
但這是一個精選的例子
，他們測試了數百個IMO級別的問題，成功率大約是1%
。所以他們能夠解決特定的問題，且必須以正確的方式格式化問題才行。盡管如此，這仍然非常了不起。
另一方面，這些工具的有趣之處在於，人類覺得困難的事情，AI有時可以很容易地做到，但人類覺得容易的事情，AI經常會表現很糟糕，這是一種非常正交的解決問題的方式。
在另一篇論文中，他們要求模型做一個基本的算術計算「7x4+8x8」，模型的答案是120，但當它逐步解釋時，又得出了答案是92。這說明，雖然AI在某些情況下能找到正確答案，但處理過程並不總是準確無誤。
因此，人們正在嘗試各種方法，將這些模型與更可靠的軟體連線，不需要自己做計算，可將計算任務交給Python。
你還可以強制模型只產生正確的答案，只在一種證明助手語言中輸出，如果它無法編譯，你就將其退回給AI，AI必須重新嘗試。或者你可以直接教它做IMO題的技巧，比如嘗試簡單的例子，矛盾證明等。
所以人們正在嘗試各種方法，雖然還沒有能力解決大多數數學問題，更不用說數學研究問題，但目前正在取得進展。
除了直接解決問題外，它們還可以作為靈感來源，我自己也使用過這些模型，嘗試過各種問題。
有一個問題，GPT-4給我推薦了10種方法，其中5種我已經嘗試過明顯無效，但有一種之前我沒註意到的技術是生成特定問題的函式，我意識到這是正確的方法。所以，它在某種程度上是有用的，現在還不完美，但也不是完全無用。
還有另一種AI輔助實際上對證明助手非常有用
。
正如我所說，編寫形式化證明是一項非常繁瑣的任務。這就像電腦語言一樣，你必須準確無誤地編寫語法，如果漏掉一個步驟，它就無法編譯。
我使用了一個叫做GitHub Copilot的工具，你可以寫下一半的證明，它會嘗試猜測下一行是什麽。大約20%的猜測是接近正確的，然後你可以接受它並繼續。
在這個例子中，我試圖證明這裏的命題，灰色行是Copilot建議的內容。結果顯示第一行是無用的，但第二行有用。因此，你不能僅僅接受輸入，因為它不一定能編譯透過。
但是，如果你已經大致了解程式碼的工作原理，這將為你節省大量時間。
現在還有實驗在嘗試讓AI提出一個證明方案，然後你將其反饋給編譯器，如果編譯錯誤，你就將錯誤資訊反饋回去。
我們已經開始嘗試證明那些四五行長的內容，可以透過這種方法進行約束。當然，像數千行的大型證明還遠遠不能立即形式化，但它已經是一個有用的工具了。
目前機器發展處於哪一階段？
那麽，我們現在處於什麽階段呢？
有人希望在未來幾年內我們可以使用電腦直接解決數學問題，我認為我們距離這一目標還很遠。
對於非常狹窄的問題，你可以設定專門的AI來處理一小部份問題。但即便如此，它們也不是完全可靠的。它們可能有用，但仍然有限。
至少在未來幾年裏，它們主要還是用於輔助
，不只是我們熟悉的蠻力計算輔助，人們正在嘗試各種創新方法，希望AI能夠非常擅長生成有見地的猜測。
我認為這是一個特別令人興奮的方向。
我們已經看到了關於結的一個小例子，AI已經能夠猜測兩種不同統計數據之間的聯系。因此，你只需建立這些龐大的數據集並將它們輸入到AI中，它們就會自動生成不同數學物件之間的許多有價值的聯系。
我們還沒有真正知道如何做到這一點，部份是因為我們沒有這些大型數據集，但我認為這最終是可能做到的。
證明定理是一個痛苦且費時的過程，我們通常一次只能證明一個定理，或者如果效率高的話，可能是兩個或三個。但是借助AI，你可以想象將來不僅僅是試圖解決一個問題，而是取一類1000個問題，然後對AI說：「好的，我要求你用這種技術來解決這1000個問題。」
使用這種技術，我能解決多少問題？如果我結合它們，我能做到什麽？你可以開始探索問題的空間，而不是單獨解決每個問題。
這是一個需要幾十年時間，透過成百上千篇論文慢慢摸索各種技術能做什麽、不能做什麽的過程。
但有了這些工具，你真的可以開始以一種前所未有的規模進行數學研究。
因此，未來將非常令人興奮。我的意思是，我們仍將以傳統方式證明定理。
事實上，我們必須這樣做，因為如果我們自己不知道如何操作，我們將無法指導這些AI。但我們將能夠做很多我們現在無法做到的事情。
參考連結：
[1]https://www.youtube.com/watch?v=e049IoFBnLA
[2]https://www.reddit.com/r/singularity/comments/1f0o9vo/terence_tao_says_ai_could_solve_mathematical/
