當人工智能開始檢查數(shù)學(xué)家的工作時會發(fā)生什么？
一家初創(chuàng)公司取得了一項突破性進展，令科學(xué)界震驚：他們將現(xiàn)代證明方法轉(zhuǎn)化為編程語言，以便利用人工智能進行驗證。但并非所有人都為此歡欣鼓舞。

作者：瑪儂·比肖夫， 編輯：黛西·尤哈斯

數(shù)學(xué)領(lǐng)域或許即將迎來一個新時代——這正是部分研究者長期以來所期盼的。數(shù)學(xué)家們很快就能利用計算機快速、嚴謹?shù)仳炞C證明，確保已發(fā)表證明的正確性，并為進一步的研究奠定基礎(chǔ)。這樣的工具將有助于專家們應(yīng)對日益加速且數(shù)量龐大的數(shù)學(xué)研究。

用于檢驗數(shù)學(xué)論證（例如證明）的計算機程序已經(jīng)存在了幾十年。但是，將人類編寫的證明翻譯成計算機嚴格的編程語言——這是使用現(xiàn)有工具進行驗證的先決條件——極其耗時。這種翻譯過程被稱為形式化，有時可能需要數(shù)月甚至數(shù)年。

隨著首批大型語言模型的開發(fā)，數(shù)學(xué)家們?nèi)计鹆讼Ｍ夯蛟S有一天機器可以自動完成這種翻譯。然而，與人類語言不同，形式化編程語言不允許任何形式的變體。每一個術(shù)語、符號和引用都必須精確定義。

但現(xiàn)在，一家名為Math, Inc.的初創(chuàng)公司宣布在形式化證明方面取得了初步成功。該公司的人工智能Gauss已經(jīng)形式化了數(shù)學(xué)家瑪麗娜·維亞佐夫斯卡（Maryna Viazovska）關(guān)于高維球體排列的兩個復(fù)雜證明。維亞佐夫斯卡曾憑借其中一個證明榮獲2022年菲爾茲獎。然而，數(shù)學(xué)界對Gauss形式化證明的反應(yīng)較為冷淡，部分原因是該項目的發(fā)展并未如許多專家所愿。隨著其他人工智能和數(shù)學(xué)領(lǐng)域的初創(chuàng)公司探索形式化，這個案例或許能為數(shù)學(xué)家們在充滿不確定性的未來中可能面臨的挑戰(zhàn)提供一些啟示。

打包難題

2016年，維亞佐夫斯卡解決了困擾數(shù)學(xué)界數(shù)十年的難題，成為該領(lǐng)域的中心人物：如何以最節(jié)省空間的方式排列球體？要找到最節(jié)省空間的單一方案，首先必須證明所有其他無窮多種球體排列方式都需要更多空間。直到1998年，人們才證明金字塔形排列——就像超市里堆放的橘子——確實是三維空間中最緊湊的排列方式。

但在更高維度上，球體的排列變得復(fù)雜得多，因為更高維度允許更多的排列方式和對稱性。維亞佐夫斯卡使用了一種特別巧妙的解決方案，這種方案僅適用于八維和二十四維空間：將空間利用率最高的三維排列方式轉(zhuǎn)移到這些更高維度，然后證明轉(zhuǎn)移后產(chǎn)生的空隙恰好足以在每個維度中容納一個額外的球體。

她首先著手證明八維空間的情況，并因此榮獲2022年菲爾茲獎。她的同事，麻省理工學(xué)院的數(shù)學(xué)家亨利·科恩，說服她與幾位合作者——包括羅格斯大學(xué)的斯蒂芬·米勒、現(xiàn)任高等科學(xué)研究院的丹尼洛·拉德琴科以及當時在石溪大學(xué)的阿比納夫·庫馬爾——共同開發(fā)24維空間的證明。一周之內(nèi)，他們就成功了。

但這些證明能否被形式化，并由計算機驗證呢？2023年，維亞佐夫斯卡遇到了西達爾特·哈里哈蘭，當時哈里哈蘭正在倫敦帝國理工學(xué)院攻讀數(shù)學(xué)碩士學(xué)位，并從事一種名為LEan的形式化流程的研究。他們開始交流想法?！拔覀冎皇莾蓚€好奇心強、渴望學(xué)習(xí)的人——事情就是這樣開始的，”他說。

兩人決定將維亞佐夫斯卡的證明形式化，方法是將其中引用的每個術(shù)語、定義和定理都翻譯成 Lean 代碼。他們與同事合作，于 2025 年 6 月推出了一個網(wǎng)站，記錄他們的形式化項目。團隊將維亞佐夫斯卡的原始工作分解成許多小的子任務(wù)，并將它們記錄在網(wǎng)上，以便更廣泛的 Lean 社區(qū)可以預(yù)約參與子任務(wù)。

與此同時，瑞士洛桑聯(lián)邦理工學(xué)院的數(shù)學(xué)博士生奧古斯特·波魯克斯 (Auguste Poiroux) 于 2025 年夏末幫助創(chuàng)立了初創(chuàng)公司 Math, Inc.?！拔覀兿Ｍ軌蜃詣訉⒄撐幕驎膬?nèi)容轉(zhuǎn)換為精益代碼并立即進行檢查，”波魯克斯解釋道。

Math, Inc.公司了解到了Hariharan及其同事的項目，并與他們?nèi)〉昧寺?lián)系?！?025年秋季，Math, Inc.公司的人告訴我們，他們已經(jīng)將我們項目的部分內(nèi)容正式化，并與我們分享了一些成果，”Hariharan回憶道，他現(xiàn)在是卡內(nèi)基梅隆大學(xué)的博士生?！爸缶褪チ寺?lián)系。我們不知道他們的進展如何，甚至不知道他們是否還在繼續(xù)?！?/p>

“我們團隊規(guī)模很小，”波伊魯克斯說，“我們意識到無法同時改進我們的系統(tǒng)并推進哈里哈蘭的項目。所以我們專注于人工智能。”在接下來的幾周里，Math, Inc. 團隊成員進一步開發(fā)了他們基于代理的語言模型，名為 Gauss。

最終，該軟件似乎能夠?qū)?shù)學(xué)表達式翻譯成精益代碼，并在無需人工干預(yù)的情況下自動進行檢查?！拔覀円跃S亞佐夫斯卡的八維證明為例進行測試，”波魯克斯說，“結(jié)果系統(tǒng)突然輸出了完整的形式化證明。這完全出乎我們的意料?！?/p>

數(shù)學(xué)的未來

波魯和他的同事們欣喜若狂。哈里哈蘭的團隊卻不這么認為?！罢f實話，我們非常驚訝，”哈里哈蘭說?！斑@是我們的項目；我們花了兩年多的時間和大量精力——結(jié)果數(shù)學(xué)公司就解決了它?！?/p>

哈里哈蘭和他的同事原本計劃將部分形式化成果作為學(xué)生本科畢業(yè)論文的基礎(chǔ)?！暗蚁?，事情就是這樣。人工智能具有顛覆性，”哈里哈蘭說道。

“當時我們太興奮了，沒有充分考慮后果，”波魯克斯說?！拔颐靼?，從外人的角度來看，這可能看起來像是我們故意隱瞞進展。以后我們一定會更加謹慎?！?/p>

Math, Inc. 隨后著手解決第二個維亞佐夫斯卡證明，該證明涉及24 維空間中的最優(yōu)球體堆積問題?！霸谶@種情況下，我們只給了高斯論文，沒有其他任何東西，”波魯克斯說?！跋到y(tǒng)將其轉(zhuǎn)換成了大約 12 萬行的精益代碼?！痹摯a此后已通過驗證。

Math, Inc. 目前正與 Hariharan 及其他專家合作，進一步推進自動形式化，并使其覆蓋更多數(shù)學(xué)領(lǐng)域?！霸谠S多領(lǐng)域，Lean 仍然缺少必要的構(gòu)建模塊——我們目前還無法對這些領(lǐng)域的證明進行形式化，”Poiroux 說。

當數(shù)學(xué)的大部分內(nèi)容能夠被形式化時，新的可能性將會出現(xiàn)。Math, Inc. 的系統(tǒng)不僅僅是翻譯機器：它們能夠檢測并糾正論文中的細微錯誤，這種能力預(yù)示著未來人工智能或許會掌控整個數(shù)學(xué)領(lǐng)域——甚至在研究方面超越人類。

“當我們的模型能夠完全理解數(shù)學(xué)時，它們就可以用完全不同的方式思考數(shù)學(xué)，”波魯克斯說，“并有可能得出全新的結(jié)果?！?/p>

本文最初發(fā)表于《科學(xué)光譜》（Spektrum der Wissenschaft），經(jīng)授權(quán)轉(zhuǎn)載。原文為德語，由人工智能輔助翻譯，并經(jīng)編輯審閱。

版權(quán)與許可
MANON BISCHOFF是一位理論物理學(xué)家，也是《科學(xué)美國人》的德語姊妹刊物《科學(xué)光譜》的編輯。

https://www.scientificamerican.com/article/what-happens-when-ai-starts-checking-mathematicians-work/