當(dāng)人工智能開始檢查數(shù)學(xué)家的工作時(shí)會(huì)發(fā)生什么？

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

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

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

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

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

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

打包難題

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

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

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

但這些證明能否被形式化，并由計(jì)算機(jī)驗(yàn)證呢？2023年，維亞佐夫斯卡遇到了西達(dá)爾特·哈里哈蘭，當(dāng)時(shí)哈里哈蘭正在倫敦帝國(guó)理工學(xué)院攻讀數(shù)學(xué)碩士學(xué)位，并從事一種名為L(zhǎng)Ean的形式化流程的研究。他們開始交流想法。“我們只是兩個(gè)好奇心強(qiáng)、渴望學(xué)習(xí)的人——事情就是這樣開始的，”他說(shuō)。

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

與此同時(shí)，瑞士洛桑聯(lián)邦理工學(xué)院的數(shù)學(xué)博士生奧古斯特·波魯克斯 (Auguste Poiroux) 于 2025 年夏末幫助創(chuàng)立了初創(chuàng)公司 Math, Inc.。“我們希望能夠自動(dòng)將論文或書籍的內(nèi)容轉(zhuǎn)換為精益代碼并立即進(jìn)行檢查，”波魯克斯解釋道。

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

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

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

數(shù)學(xué)的未來(lái)

波魯和他的同事們欣喜若狂。哈里哈蘭的團(tuán)隊(duì)卻不這么認(rèn)為。“說(shuō)實(shí)話，我們非常驚訝，”哈里哈蘭說(shuō)。“這是我們的項(xiàng)目；我們花了兩年多的時(shí)間和大量精力——結(jié)果數(shù)學(xué)公司就解決了它。”

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

“當(dāng)時(shí)我們太興奮了，沒(méi)有充分考慮后果，”波魯克斯說(shuō)。“我明白，從外人的角度來(lái)看，這可能看起來(lái)像是我們故意隱瞞進(jìn)展。以后我們一定會(huì)更加謹(jǐn)慎。”

Math, Inc. 隨后著手解決第二個(gè)維亞佐夫斯卡證明，該證明涉及24 維空間中的最優(yōu)球體堆積問(wèn)題。“在這種情況下，我們只給了高斯論文，沒(méi)有其他任何東西，”波魯克斯說(shuō)。“系統(tǒng)將其轉(zhuǎn)換成了大約 12 萬(wàn)行的精益代碼。”該代碼此后已通過(guò)驗(yàn)證。

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

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

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

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

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

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