數學家安德魯·懷爾斯於1995年發表了費馬大定理的証明。圖片來源：英國《自然》網站

費馬大定理是過去半個世紀最著名的數學成果之一。9月4日，人工智能（AI）公司Anthropic宣布，其Claude模型僅用11天，就將英國數學家安德魯·懷爾斯1995年完成的費馬大定理証明轉化為計算機可逐步驗証的形式化証明。

“機器竟然能夠把人類數學家的工作轉化為一份長達1300萬行、堅不可摧的証明，這完全讓我震撼。”美國羅格斯大學數論學家亞歷克斯·孔托羅維奇說。

英國《自然》網站在7日發表的文章中稱，這一成果表明，AI將在數學家的工作中發揮越來越重要的作用，不僅可幫助檢驗數學証明，也可能參與產生新的數學推理。按照目前的發展速度，AI審查整個人類數學知識庫，已不再是遙不可及的事，甚至可能發現一些廣為人知的數學結論中是否藏著錯誤。而在兩年前，這還只是幻想。

AI打破人工核驗局限

數學証明是一連串嚴密的邏輯步驟，只要其中一環出錯，整個証明就可能坍塌。面對動輒數百頁、涉及大量復雜理論的証明，單靠人工逐一核驗每個環節，幾乎是不可能完成的任務。

費馬大定理就是一個典型。1637年，法國數學家皮埃爾·德·費馬提出了這個命題：當整數n大於2時，不存在滿足xn+yn=zn的正整數x、y、z。

1908年，德國曾懸賞一筆獎金（今天約合100萬至200萬美元），向數學家征集費馬大定理的証明。僅第一年，就收到了621份証明，但沒有一份站得住腳。直到上世紀90年代，英國數學家安德魯·懷爾斯才真正攻克了這一難題。他在1995年5月發表了長達129頁的証明，橫跨數論多個分支，匯集了大量現代數學成果。該証明通過了數學界審查並得到認可，費馬大定理就此塵埃落定。

所謂“形式化”証明，就是把數學証明翻譯成一種極其嚴格、精確的語言，讓計算機能夠自行驗証其中的每一步，而不需要依賴人的主觀判斷。

近年來，AI進行數學形式化的能力進步很快。今年2月，AI輔助數學形式化取得一項裡程碑式進展，成功對菲爾茲獎得主瑪麗娜·維亞佐夫斯卡關於8維和24維空間中最有效球體堆積方式的研究成果完成了計算機驗証。不過，英國倫敦帝國理工學院數學家凱文·巴扎德說，費馬大定理的形式化工作“可能更困難一個數量級”。

預估十年工作量被AI壓縮到11天

2024年，巴扎德啟動了一個項目，目標是把懷爾斯的証明翻譯成Lean語言，以便計算機驗証。他原本估計這項工作需要10年。項目自身的規劃文件就長達86頁，資金支持目前已經確定到2029年。

一年多后，AI大大推進了工作進度。Anthropic讓Claude承擔了費馬大定理的形式化任務。據Anthropic介紹，哥倫比亞大學研究人員彭天翼及其團隊讓數十個Claude智能體並行工作，不同智能體分別負責定義數學概念、証明較小的輔助定理，再將這些結果逐步組合起來。

Claude此次使用的Lean是一種專門用於形式化數學的証明輔助工具。數學家通過Lean把數學定義、定理和推理寫成計算機能夠處理的形式，再由計算機檢查証明過程。

與Lean配套的Mathlib是一個由數學家持續維護的數學代碼庫，其中已經收錄了大量經過形式化處理的數學知識。新的數學証明可以調用其中已有的定義和定理，從而避免重復勞動。

不過，這項工作最初並不順利。智能體會忘記其他智能體已經完成的工作，產生重復工作，有時甚至停止協作。研究團隊隨后使用Prove2Me工具，為智能體提供實時任務清單，記錄已完成和待辦事項，幫助各智能體調用已有成果。

經過11天運轉，Claude完成了整個形式化過程，証明了約3萬個輔助定理，生成了約1300萬行代碼，規模相當於160部長篇小說。

正確判定率從99.9%到100%

經過形式化之后，懷爾斯的証明獲得了一份計算機可逐行核驗的“認証”。巴扎德說，過去自己有“99.9%的把握”認為這份証明正確，如今則是“100%”。

這種確定性對於數學同行評審尤為關鍵。數學論文數量不斷增加，篇幅越來越長，涉及的數學知識也愈加復雜，人工檢查一份完整証明往往需要耗費大量時間。即使如此，仍可能漏掉一些錯誤。

數學家對這種情況並不陌生。開普勒猜想的一項計算機輔助証明花了4年時間，之后審查小組仍只能給出“99%確定”的評價。格裡戈裡·佩雷爾曼關於龐加萊猜想的証明，也花費了大約4年時間才得到數學界充分理解和認可。

美國加州大學聖迭戈分校數學家弗雷德裡克·曼納斯設想，如果有一種“魔法”，能夠把一篇發表在預印本平台arXiv上的論文交給機器，由機器判定証明是否正確，或者直接指出其中錯誤，那將具有極其重要的價值。

如今，Claude生成的約1300萬行証明已經公開在GitHub上，任何數學家都可以免費獲取並逐行核查。隨著AI參與數學形式化的能力不斷提升，曼納斯設想的“魔法”正從想象一步步走向現實。（記者 張佳欣）