讓AI理解費馬大定理的證明，兩個月過去了，進展如何？
1637 年，費馬在閱讀丟番圖《算術》拉丁文譯本時，曾在第 11 卷第 8 命題旁寫道：「將一個立方數分成兩個立方數之和，或一個四次冪分成兩個四次冪之和，或者一般地將一個高于二次的冪分成兩個同次冪之和，這是不可能的。關于此，我確信我發現一種美妙的證法，可惜這里的空白處太小，寫不下。」
這就是著名的費馬大定理（FLT，也叫費馬最后定理）：
當整數 n > 2 時，關于 x, y, z 的不定方程 x? + y? = z? 無正整數解。
此后，無數數學家和數學愛好者都嘗試過證明這個定理；甚至對該定理的證明一度成為「民間數學家」最愛挑戰的難題之一，這個現象讓數學歷史學家霍華德?伊夫斯（Howard Eves）忍不住感慨：「費馬大定理的獨特之處在于它是迄今為止發表錯誤證明最多的數學問題。」
對費馬大定理的首個完整證明直到 358 年之后的 1995 年才真正發表。為此，英國數學家安德魯?懷爾斯（Andrew Wiles）使用了一系列復雜的數學工具和理論。整體而言，懷爾斯的證明建立在模形式和橢圓曲線之間的深刻聯系（即谷山 - 志村猜想的一部分）之上，整個證明非常復雜，論文《Modular elliptic curves and Fermat’s Last Theorem》就有 109 頁。
近日，倫敦帝國學院數學教授 Kevin Buzzard 在自己的博客上分享了一個非常有趣的項目：教計算機理解費馬大定理的證明。這項工作可以幫助驗證對費馬大定理的證明，修正其中可能存在疏漏的部分。雖然計算機還沒有完全理解，但也確實取得了一些進展。
這篇博客在 Hacker News 上吸引了大量討論，很多人都分享了自己的見解或經歷，尤其是關于數學形式化的重要性。
以上截圖均來自 Hacker News 和谷歌翻譯，更多討論請訪問：
https://news.ycombinator.com/item?id=42399397
以下是 Buzzard 教授的博客全文（原文段落較長，這里進行了適當拆分和調整）。
費馬大定理 —— 進展如何？
我已經花了兩個月時間來教計算機理解馬大定理（FLT）的一個證明。
大部分的「進展如何」解釋起來都相當繁瑣且技術性：長話短說，懷爾斯證明了「R=T」定理，而到目前為止的大部分工作都是教計算機理解什么是 R 和 T；我們仍然還沒有完成這兩者中任何一個的定義。
但是，我的博士生 Andrew Yang 已經證明了我們需要的抽象可交換代數結果（「如果抽象環（abstract rings）R 和 T 滿足許多技術條件，則它們相等」），這是令人興奮的第一步。
我們使用的系統是 Lean 及其數學軟件庫 mathlib，該軟件庫由 Lean 證明器社區維護。如果你對 Lean 和數論有所了解，可以考慮閱讀貢獻指南、查看項目儀表板并認領一個問題。
下面是一些相關鏈接：
- 藍圖和進展：https://imperialcollegelondon.github.io/FLT/blueprint/
- Lean：https://lean-fro.org/
- mathlib：https://github.com/leanprover-community/mathlib4
- 貢獻指南：https://github.com/ImperialCollegeLondon/FLT/blob/main/CONTRIBUTING.md
- 項目儀表盤：https://github.com/orgs/ImperialCollegeLondon/projects/102
- 問題：https://github.com/ImperialCollegeLondon/FLT/issues
藍圖頁面截圖
如前所述，我們已經進行了兩個月。但是，我們已經有一個我認為值得分享的有趣故事了。誰知道這是否預示著某個未來。
我們的目的并不是形式化 1990 年代那個 FLT 證明。自那以后，已經有很多人（Diamond/Fujiwara、Kisin、Taylor、Scholze 等人）對該證明進行了泛化和簡化。我的部分動機是要證明這些更通用、更有力的結果。為什么這是因為如果 AI 真的可以變革數學（有可能），并且 Lean 被證明是一個重要的組成部分（也有可能），那么計算機將能夠更好地幫助人類突破現代數論的界限。對于這種形式化工作，計算機能夠以它們理解的方式來獲得關鍵的現代定義。
懷爾斯的原始證明中沒有使用的一個概念，在我們正在形式化的證明中使用了，它就是晶體上同調（crystalline cohomology）。
這是 20 世紀六七十年代在法國巴黎發展起來的理論，其基礎是由數學家 Berthelot 根據另一位數學家 Grothendieck 的思想搭建的。基本思想是經典指數和對數函數在微分幾何（例如 Lie 代數和 Lie 群）發揮關鍵作用，特別是在理解德拉姆上同調（de Rham cohomology,）中，不過它們在更多的算術情況下不起作用（例如在特征 p 中）。
20 世紀六十年代，Roby 在一系列精彩的論文中提出了「除冪結構」（divided power structures），在構建可用于算術情況的類函數中發揮了至關重要的作用。注：我們要想教計算機晶體上同調，首先需要教它除冪理論。
數學領域的研究者 Antoine Chambert-Loir（簡稱 Antoine）和 Maria Ines de Frutos Fernandez（簡稱 Maria Ines）一直在教 Lean 除冪理論，而整個夏天，Lean 都時而出現一種令人惱火的情況：它會抱怨標準文獻中人為提出的論證，并經過仔細檢查發現人為論證有待改進，特別是 Roby 的工作中有一個關鍵引理似乎不正確。當 Antoine 告訴我這件事時，他覺得我會認為這很有趣，而他收到的回復中一長串大笑的表情符號確實證實了這一點。
然而，Antoine 比我更專業，認為我不應該發推討論這個問題（反正我也不發，我已經拋棄了推特并轉向了社交平臺 bluesky），而應該嘗試解決這個問題。
我們以完全不同的方式來處理這個問題，Antoine 把它列入了自己的工作清單，而我卻完全忽略了它，只是偶爾向人們提及這個證明有問題，是弱證明。我之所以說是弱證明，是因為這一觀察必須放在某種背景下。
根據我目前對數學的觀察（作為形式主義者），當 Antoine 發現這個問題時，整個晶體上同調理論就從文獻中消失了，并帶來巨大的附帶損害（例如數學家 Scholze 的大量工作就消失了，整本的書籍和論文都化為烏有）。但這種消失只是暫時的，晶體上同調在實際意義上并沒有錯誤。這些定理毫無疑問仍然是正確的，只是就我而言，證明是不完整的（或者至少 Antoine 和 Maria Ines 遵循的證明不完整）。因此我們的工作就是修正它們。
我想強調的是，我和 Antoine 都很清楚，即使中間引理是錯誤的，主要結果的證明當然可以修正，這是因為從 20 世紀 70 年代以來晶體上同調就得到了廣泛使用。如果它有問題，早就該暴露出來了。我交流過的每個專家都同意這一點，有幾位甚至認為我在小題大做。但也許他們不明白形式化在實踐中到底意味著什么：你不能只是說「我相信它可以修正」，你必須真正地修正它。另外，Roby、Grothendieck 和 Berthelot 都已經去世了，我們無法從這些原來的專家那里直接尋求幫助。
對更多技術細節感興趣的人可以先看這里：Berthelot 的論文并沒有從頭開始發展除冪理論，他使用了 Roby 的「Les algebres a puissances divisees」，1965 年在 Bull Sci Math 上發表。該論文的引理 8 似乎是錯誤的，而且如何修正證明也沒說明白。該引理的證明錯誤引用了 Roby 1963 年 Ann Sci ENS 論文中的另一個引理。其正確的表述是「Gamma_A (M) tensor_A R = Gamma_R (M tensor_A R)」，但其中一個張量積在應用中意外脫離。這就打破了 Roby 關于「模（module）的除冪代數具有除冪］的證明，從而阻止我們定義環 A_{cris}。
所以，正如我所言，Antoine 正致力于解決這個問題，而我只是在向專家們八卦閑談，而且我犯了一個錯：在伊斯靈頓的一家咖啡店告訴了時枝正（Tadashi Tokieda）這件事，他回到斯坦福后向 Brian Conrad 提到了這件事，然后 Conrad 就開始在我的收件箱里問我晶體上同調有問題到底是怎么回事。
我解釋了這個問題的技術細節，Conrad 同意這好像確實是一個問題，然后他開始思考。幾個小時后，他回復了我，并指出，在 Berthelot-Ogus 的關于晶體上同調的著作的附錄中，存在對「模的一般除冪代數具有除冪」這個斷言的另一個不同的證明，而且 Conrad 認為這個方法沒有問題。證明又回來了！
這差不多就是故事的全部。上個月我訪問了伯克利，和 Arthur Ogus 共進午餐，我 90 年代在那里做博士后的時候就認識他了。我答應過 Arthur，給他講一個他如何拯救費馬大定理的故事，吃飯的時候我告訴他，他的附錄如何把我從困境中救了出來。他的回答是「哦！那個附錄有幾個錯誤！但沒關系，我想我知道如何修正它們。」
在我看來，這個故事表明，人們在編寫現代數學文檔方面做得很差。似乎有很多東西是「專家們已知的」，但卻并沒有得到正確的文檔化。
這些專家們一致認為，重要的想法足夠強大，可以經受住這樣的打擊，但實際發生的細節可能并不像人們期望的那樣。對我來說，這只是人類想要正確記錄數學的眾多原因之一，即在形式系統中，錯誤的可能性要小幾個數量級。
然而，大多數數學家都不是形式主義者，對于這些人，我需要以不同的方式說明我的工作的合理性。對于那些數學家而言，我認為教會機器理解我們的論證是讓機器自己做這件事的關鍵一步。在此之前，我們似乎注定要手動修正人為錯誤。
不過，這個故事確實有一個圓滿的結局 —— 兩周前，Maria Ines 在劍橋數學形式化研討會（Cambridge Formalization of Mathematics seminar）上發表了一個關于除冪的形式化的演講。根據這個演講，我的理解是這些問題現在已經得到解決了。所以我們實際上又回到了正軌。直到下一次文獻讓我們失望……
參考鏈接：
https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/。
https://news.ycombinator.com/item?id=42399397。
