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

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

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

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

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

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

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

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

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

費(fèi)馬大定理 —— 進(jìn)展如何？

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

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

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

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

下面是一些相關(guān)鏈接：

• 藍(lán)圖和進(jìn)展：https://imperialcollegelondon.github.io/FLT/blueprint/
• Lean：https://lean-fro.org/
• mathlib：https://github.com/leanprover-community/mathlib4
• 貢獻(xiàn)指南：https://github.com/ImperialCollegeLondon/FLT/blob/main/CONTRIBUTING.md
• 項(xiàng)目儀表盤：https://github.com/orgs/ImperialCollegeLondon/projects/102
• 問題：https://github.com/ImperialCollegeLondon/FLT/issues

藍(lán)圖頁面截圖

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

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

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

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

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

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

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

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

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

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

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

所以，正如我所言，Antoine 正致力于解決這個(gè)問題，而我只是在向?qū)＜覀儼素蚤e談，而且我犯了一個(gè)錯(cuò)：在伊斯靈頓的一家咖啡店告訴了時(shí)枝正（Tadashi Tokieda）這件事，他回到斯坦福后向 Brian Conrad 提到了這件事，然后 Conrad 就開始在我的收件箱里問我晶體上同調(diào)有問題到底是怎么回事。

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

這差不多就是故事的全部。上個(gè)月我訪問了伯克利，和 Arthur Ogus 共進(jìn)午餐，我 90 年代在那里做博士后的時(shí)候就認(rèn)識他了。我答應(yīng)過 Arthur，給他講一個(gè)他如何拯救費(fèi)馬大定理的故事，吃飯的時(shí)候我告訴他，他的附錄如何把我從困境中救了出來。他的回答是「哦！那個(gè)附錄有幾個(gè)錯(cuò)誤！但沒關(guān)系，我想我知道如何修正它們?！?/span>

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

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

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

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

參考鏈接：

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

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