1637 年，費馬在閱讀丟番圖《算術》拉丁文譯本時，曾在第 11 卷第 8 命題旁寫道：「將一個立方數(shù)分成兩個立方數(shù)之和，或一個四次冪分成兩個四次冪之和，或者一般地將一個高于二次的冪分成兩個同次冪之和，這是不可能的。關于此，我確信我發(fā)現(xiàn)一種美妙的證法，可惜這里的空白處太小，寫不下?！?/span>

這就是著名的費馬大定理（FLT，也叫費馬最后定理）：

當整數(shù) n > 2 時，關于 x, y, z 的不定方程 x? + y? = z? 無正整數(shù)解。

此后，無數(shù)數(shù)學家和數(shù)學愛好者都嘗試過證明這個定理；甚至對該定理的證明一度成為「民間數(shù)學家」最愛挑戰(zhàn)的難題之一，這個現(xiàn)象讓數(shù)學歷史學家霍華德?伊夫斯（Howard Eves）忍不住感慨：「費馬大定理的獨特之處在于它是迄今為止發(fā)表錯誤證明最多的數(shù)學問題?！?/span>

對費馬大定理的首個完整證明直到 358 年之后的 1995 年才真正發(fā)表。為此，英國數(shù)學家安德魯?懷爾斯（Andrew Wiles）使用了一系列復雜的數(shù)學工具和理論。整體而言，懷爾斯的證明建立在模形式和橢圓曲線之間的深刻聯(lián)系（即谷山 - 志村猜想的一部分）之上，整個證明非常復雜，論文《Modular elliptic curves and Fermat’s Last Theorem》就有 109 頁。

近日，倫敦帝國學院數(shù)學教授 Kevin Buzzard 在自己的博客上分享了一個非常有趣的項目：教計算機理解費馬大定理的證明。這項工作可以幫助驗證對費馬大定理的證明，修正其中可能存在疏漏的部分。雖然計算機還沒有完全理解，但也確實取得了一些進展。

這篇博客在 Hacker News 上吸引了大量討論，很多人都分享了自己的見解或經(jīng)歷，尤其是關于數(shù)學形式化的重要性。

以上截圖均來自 Hacker News 和谷歌翻譯，更多討論請訪問：
https://news.ycombinator.com/item?id=42399397

以下是 Buzzard 教授的博客全文（原文段落較長，這里進行了適當拆分和調(diào)整）。

費馬大定理 —— 進展如何？

我已經(jīng)花了兩個月時間來教計算機理解馬大定理（FLT）的一個證明。

大部分的「進展如何」解釋起來都相當繁瑣且技術性：長話短說，懷爾斯證明了「R=T」定理，而到目前為止的大部分工作都是教計算機理解什么是 R 和 T；我們?nèi)匀贿€沒有完成這兩者中任何一個的定義。

但是，我的博士生 Andrew Yang 已經(jīng)證明了我們需要的抽象可交換代數(shù)結果（「如果抽象環(huán)（abstract rings）R 和 T 滿足許多技術條件，則它們相等」），這是令人興奮的第一步。

我們使用的系統(tǒng)是 Lean 及其數(shù)學軟件庫 mathlib，該軟件庫由 Lean 證明器社區(qū)維護。如果你對 Lean 和數(shù)論有所了解，可以考慮閱讀貢獻指南、查看項目儀表板并認領一個問題。

下面是一些相關鏈接：

• 藍圖和進展：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

藍圖頁面截圖

如前所述，我們已經(jīng)進行了兩個月。但是，我們已經(jīng)有一個我認為值得分享的有趣故事了。誰知道這是否預示著某個未來。

我們的目的并不是形式化 1990 年代那個 FLT 證明。自那以后，已經(jīng)有很多人（Diamond/Fujiwara、Kisin、Taylor、Scholze 等人）對該證明進行了泛化和簡化。我的部分動機是要證明這些更通用、更有力的結果。為什么這是因為如果 AI 真的可以變革數(shù)學（有可能），并且 Lean 被證明是一個重要的組成部分（也有可能），那么計算機將能夠更好地幫助人類突破現(xiàn)代數(shù)論的界限。對于這種形式化工作，計算機能夠以它們理解的方式來獲得關鍵的現(xiàn)代定義。

懷爾斯的原始證明中沒有使用的一個概念，在我們正在形式化的證明中使用了，它就是晶體上同調(diào)（crystalline cohomology）。

這是 20 世紀六七十年代在法國巴黎發(fā)展起來的理論，其基礎是由數(shù)學家 Berthelot 根據(jù)另一位數(shù)學家 Grothendieck 的思想搭建的?；舅枷胧墙?jīng)典指數(shù)和對數(shù)函數(shù)在微分幾何（例如 Lie 代數(shù)和 Lie 群）發(fā)揮關鍵作用，特別是在理解德拉姆上同調(diào)（de Rham cohomology,）中，不過它們在更多的算術情況下不起作用（例如在特征 p 中）。

20 世紀六十年代，Roby 在一系列精彩的論文中提出了「除冪結構」（divided power structures），在構建可用于算術情況的類函數(shù)中發(fā)揮了至關重要的作用。注：我們要想教計算機晶體上同調(diào)，首先需要教它除冪理論。

數(shù)學領域的研究者 Antoine Chambert-Loir（簡稱 Antoine）和 Maria Ines de Frutos Fernandez（簡稱 Maria Ines）一直在教 Lean 除冪理論，而整個夏天，Lean 都時而出現(xiàn)一種令人惱火的情況：它會抱怨標準文獻中人為提出的論證，并經(jīng)過仔細檢查發(fā)現(xiàn)人為論證有待改進，特別是 Roby 的工作中有一個關鍵引理似乎不正確。當 Antoine 告訴我這件事時，他覺得我會認為這很有趣，而他收到的回復中一長串大笑的表情符號確實證實了這一點。

然而，Antoine 比我更專業(yè)，認為我不應該發(fā)推討論這個問題（反正我也不發(fā)，我已經(jīng)拋棄了推特并轉向了社交平臺 bluesky），而應該嘗試解決這個問題。

我們以完全不同的方式來處理這個問題，Antoine 把它列入了自己的工作清單，而我卻完全忽略了它，只是偶爾向人們提及這個證明有問題，是弱證明。我之所以說是弱證明，是因為這一觀察必須放在某種背景下。

根據(jù)我目前對數(shù)學的觀察（作為形式主義者），當 Antoine 發(fā)現(xiàn)這個問題時，整個晶體上同調(diào)理論就從文獻中消失了，并帶來巨大的附帶損害（例如數(shù)學家 Scholze 的大量工作就消失了，整本的書籍和論文都化為烏有）。但這種消失只是暫時的，晶體上同調(diào)在實際意義上并沒有錯誤。這些定理毫無疑問仍然是正確的，只是就我而言，證明是不完整的（或者至少 Antoine 和 Maria Ines 遵循的證明不完整）。因此我們的工作就是修正它們。

我想強調(diào)的是，我和 Antoine 都很清楚，即使中間引理是錯誤的，主要結果的證明當然可以修正，這是因為從 20 世紀 70 年代以來晶體上同調(diào)就得到了廣泛使用。如果它有問題，早就該暴露出來了。我交流過的每個專家都同意這一點，有幾位甚至認為我在小題大做。但也許他們不明白形式化在實踐中到底意味著什么：你不能只是說「我相信它可以修正」，你必須真正地修正它。另外，Roby、Grothendieck 和 Berthelot 都已經(jīng)去世了，我們無法從這些原來的專家那里直接尋求幫助。

對更多技術細節(jié)感興趣的人可以先看這里：Berthelot 的論文并沒有從頭開始發(fā)展除冪理論，他使用了 Roby 的「Les algebres a puissances divisees」，1965 年在 Bull Sci Math 上發(fā)表。該論文的引理 8 似乎是錯誤的，而且如何修正證明也沒說明白。該引理的證明錯誤引用了 Roby 1963 年 Ann Sci ENS 論文中的另一個引理。其正確的表述是「Gamma_A (M) tensor_A R = Gamma_R (M tensor_A R)」，但其中一個張量積在應用中意外脫離。這就打破了 Roby 關于「模（module）的除冪代數(shù)具有除冪］的證明，從而阻止我們定義環(huán) A_{cris}。

所以，正如我所言，Antoine 正致力于解決這個問題，而我只是在向專家們八卦閑談，而且我犯了一個錯：在伊斯靈頓的一家咖啡店告訴了時枝正（Tadashi Tokieda）這件事，他回到斯坦福后向 Brian Conrad 提到了這件事，然后 Conrad 就開始在我的收件箱里問我晶體上同調(diào)有問題到底是怎么回事。

我解釋了這個問題的技術細節(jié)，Conrad 同意這好像確實是一個問題，然后他開始思考。幾個小時后，他回復了我，并指出，在 Berthelot-Ogus 的關于晶體上同調(diào)的著作的附錄中，存在對「模的一般除冪代數(shù)具有除冪」這個斷言的另一個不同的證明，而且 Conrad 認為這個方法沒有問題。證明又回來了！

這差不多就是故事的全部。上個月我訪問了伯克利，和 Arthur Ogus 共進午餐，我 90 年代在那里做博士后的時候就認識他了。我答應過 Arthur，給他講一個他如何拯救費馬大定理的故事，吃飯的時候我告訴他，他的附錄如何把我從困境中救了出來。他的回答是「哦！那個附錄有幾個錯誤！但沒關系，我想我知道如何修正它們。」

在我看來，這個故事表明，人們在編寫現(xiàn)代數(shù)學文檔方面做得很差。似乎有很多東西是「專家們已知的」，但卻并沒有得到正確的文檔化。

這些專家們一致認為，重要的想法足夠強大，可以經(jīng)受住這樣的打擊，但實際發(fā)生的細節(jié)可能并不像人們期望的那樣。對我來說，這只是人類想要正確記錄數(shù)學的眾多原因之一，即在形式系統(tǒng)中，錯誤的可能性要小幾個數(shù)量級。

然而，大多數(shù)數(shù)學家都不是形式主義者，對于這些人，我需要以不同的方式說明我的工作的合理性。對于那些數(shù)學家而言，我認為教會機器理解我們的論證是讓機器自己做這件事的關鍵一步。在此之前，我們似乎注定要手動修正人為錯誤。

不過，這個故事確實有一個圓滿的結局 —— 兩周前，Maria Ines 在劍橋數(shù)學形式化研討會（Cambridge Formalization of Mathematics seminar）上發(fā)表了一個關于除冪的形式化的演講。根據(jù)這個演講，我的理解是這些問題現(xiàn)在已經(jīng)得到解決了。所以我們實際上又回到了正軌。直到下一次文獻讓我們失望……

參考鏈接：

https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/。

https://news.ycombinator.com/item?id=42399397。