當人工智能開始檢查數學家的工作時會發生什么？

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

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

數學領域或許即將迎來一個新時代——這正是部分研究者長期以來所期盼的。數學家們很快就能利用計算機快速、嚴謹地驗證證明，確保已發表證明的正確性，并為進一步的研究奠定基礎。這樣的工具將有助于專家們應對日益加速且數量龐大的數學研究。

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

隨著首批大型語言模型的開發，數學家們燃起了希望：或許有一天機器可以自動完成這種翻譯。然而，與人類語言不同，形式化編程語言不允許任何形式的變體。每一個術語、符號和引用都必須精確定義。

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

打包難題

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

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

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

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

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

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

Math, Inc.公司了解到了Hariharan及其同事的項目，并與他們取得了聯系。“2025年秋季，Math, Inc.公司的人告訴我們，他們已經將我們項目的部分內容正式化，并與我們分享了一些成果，”Hariharan回憶道，他現在是卡內基梅隆大學的博士生。“之后就失去了聯系。我們不知道他們的進展如何，甚至不知道他們是否還在繼續。”

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

最終，該軟件似乎能夠將數學表達式翻譯成精益代碼，并在無需人工干預的情況下自動進行檢查。“我們以維亞佐夫斯卡的八維證明為例進行測試，”波魯克斯說，“結果系統突然輸出了完整的形式化證明。這完全出乎我們的意料。”

數學的未來

波魯和他的同事們欣喜若狂。哈里哈蘭的團隊卻不這么認為。“說實話，我們非常驚訝，”哈里哈蘭說。“這是我們的項目；我們花了兩年多的時間和大量精力——結果數學公司就解決了它。”

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

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

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

Math, Inc. 目前正與 Hariharan 及其他專家合作，進一步推進自動形式化，并使其覆蓋更多數學領域。“在許多領域，Lean 仍然缺少必要的構建模塊——我們目前還無法對這些領域的證明進行形式化，”Poiroux 說。

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

“當我們的模型能夠完全理解數學時，它們就可以用完全不同的方式思考數學，”波魯克斯說，“并有可能得出全新的結果。”

本文最初發表于《科學光譜》（Spektrum der Wissenschaft），經授權轉載。原文為德語，由人工智能輔助翻譯，并經編輯審閱。

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

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