跨越300多年的接力：受陶哲軒啟發，數學家決定用AI形式化費馬大定理的證明

在陶哲軒的啟發下，越來越多的數學家開始嘗試利用人工智慧進行數學探索。這次，他們瞄準的目標是世界十大最頂尖數學難題之一的費馬大定理。費馬大定理是一個非常複雜的數學難題，迄今尚未找到可行的解法。數學家希望藉助人工智慧的強大運算能力和智慧演算法，能夠在數學中探索

費馬大定理又被稱為「費馬最後的定理（Fermat's Last Theorem，FLT）”，由17世紀法國數學家皮耶・德・費馬提出。它背後有一個傳奇的故事。據稱，大約在1637年左右，費馬在閱讀丟番圖《算術》拉丁文譯本時，曾在第11卷第8命題旁寫道：「將一個立方數分成兩個立方數之和，或一個四次冪分成兩個四次冪之和，或一般地將一個高於二次方的冪分成兩個同次方之和，這是不可能的。種美妙的證法，可惜這裡空白的地方太小，寫不下了。 」

這段話前面所表述的就是費馬大定理的內容：當整數n>2 時，關於x^n y^n=z^n 的方程沒有正整數解。 ，後世是有爭議的。孤軍奮戰，終於用130頁長的篇幅完成了證明。還能用AI 做什麼呢？定理和證明，使其能夠在計算機上進行表示、驗證和操作，從而保證數學內容的準確性和一致性。始於20世紀的數理邏輯和計算機科學的發展。 形式化數學的主要目標是建立一套形式系統，其中包括一組符號、一組基本公理和一組推理規則，透過這些規則和公理的運用，可以進行

去年年底，陶哲軒等人曾用Lean（一款互動式定理證明器，也是一門程式語言）形式化了他們的一篇論文。這篇論文是對多項式 Freiman-Ruzsa 猜想的一個版本的證明，於去年 11 月發佈在 arXiv 上。在編寫 Lean 語言程式碼的時候，陶哲軒也藉助了 AI 程式設計助手 Copilot。這事件引起數學界和人工智慧界的廣泛關注。

當時，Lean 技術開源社群最重要的推廣者、倫敦帝國學院的Kevin Buzzard 表示：「從根本上來說，顯而易見的是，當你將某些東西數位化時，你就可以以新的方式使用它。的工具也是Lean。

在一篇部落格中，他介紹了自己做這件事情的背景、動機以及具體的做法。

為什麼要形式化費馬大定理的證明？

費馬大定理的形式非常簡潔、直觀，然而證明它卻異常艱難。這無疑是數學深邃之美的絕佳展示。在過去的幾個世紀中，為了解決這個問題，數學家們發展和創新了大量數學理論，這些理論在密碼學到物理學等多個領域都有所應用。

Andrew Wiles 可能因FLT 而受到啟發，但他的工作實際上為朗蘭茲計劃帶來了突破，該計劃是數學中一系列影響深遠的構想，聯繫數論、代數幾何與約化群表示理論，且在2024 年依然備受關注。

歷史上，代數數論的其他幾個重大突破（例如數域中的因式分解理論和循環域的算術）至少部分是出於對 FLT 更深層理解的渴望。

Wiles 的工作，由他的學生 Richard Taylor 一起補充完整，建立在 20 世紀數學的龐大基礎之上。 Wiles 引入的基本技術 ——「模性提升定理（modularity lifting theorem）」—— 在原始論文發表後的 30 年間，在概念上被極大簡化和廣泛推廣。這一領域至今仍然非常活躍。 Frank Calegari 在 2022 年國際數學家大會上的論文，概述了自 Wiles 突破以來的進展（參見：https://arxiv.org/abs/2109.14145）。 Kevin Buzzard 表示，這一領域的持續活躍，是他將 FLT 證明形式化的動機之一。

數學的形式化，將紙上的數學轉換成能夠理解定理和證明概念的電腦程式語言的藝術。這些程式語言，也稱為互動式定理證明器（ITP），已經存在了數十年。然而，近年來，這一領域似乎吸引了數學界的一部分關注。我們見證了多個研究數學形式化的例子，其中最新的是陶哲軒等人對多項式 Freiman—Ruzsa 猜想證明的形式化。這篇 2023 年的突破性論文在短短三週內就在 Lean 中完成了形式化。這樣的成功案例可能會讓旁觀者認為，像 Lean 這樣的 ITP 現在已經準備好形式化所有現代數學了。

然而，真相遠非如此簡單。在數學的某些領域，例如組合學，我們可以看到一些現代突破可以即時形式化。然而，Buzzard 表示，他定期參加倫敦數論研討會，經常注意到 Lean 對現代數學定義的了解還不足以表達研討會上宣布的結果，更不用說驗證它們的證明了。

事實上，數論在這一方面的「滯後」是 Buzzard 啟動 FLT 當代證明形式化的主要動機之一。在專案完成之前，Lean 將能夠理解自守形式（一類特別的複變量函數）和表示、伽羅瓦表示、潛在自守性、模性提升定理、代數簇的算術、類域論、算術對偶定理、志村簇等現代代數數論所使用的概念。在 Buzzard 看來，有了這些做基礎，將他自己專業領域正在發生的事情形式化將不再是科幻小說。

那麼，為什麼要這麼做呢？ Buzzard 解釋說，「如果我們相信一些電腦科學家的話，人工智慧的指數級增長終將使電腦能夠幫助數學家進行研究。這樣的工作可以幫助電腦理解我們在現代數學研究中正在做的事情。」

專案如何進行？ 

費馬大定理的形式化計畫現已啟動。 Buzzard 在一幅圖中展示了當前的進展。

有興趣的研究者可以閱讀詳情：https://imperialcollegelondon.github.io/FLT/blueprint/dep_graph_document.html

該專案由EPSRC 資助，Buzzard 將獲得前五年的資金支持。在此期間，他的第一個目標是將 FLT 簡化為 1980 年代末數學家已知的聲明。

當然，Buzzard 沒有打算獨自完成這件事。他表示，對於有些論證的部分，他理解其基本原則，但從未仔細檢查過細節。而且，朗蘭茲計劃還引入了一些重要的東西，包括 GL_2 的循環基變換以及 Jacquet-Langlands。對於這些深奧的東西，他的理解還不夠深。

不過，這正是形式化專案的優勢所在。 Buzzard 將能夠在 Lean 中明確表達他需要的結果，並將它們傳遞給其他人。這個系統的美妙之處在於：你不必理解 FLT 的整個證明就能做出貢獻。上面的圖將證明分解為許多小引理，因此非常方便進行眾包操作。如果你能形式化證明其中任何一個引理，那麼 Buzzard 會熱切期待你的拉取請求。

想要參與專案的人需要了解一些關於 Lean 的知識。對此，Buzzard 推薦了線上教科書 Mathematics in Lean。

教科書連結：https://leanprover-community.github.io/mathematics_in_lean/

該專案將在Lean Zulip chat 的FLT  stream 上進行，這是一個強大的研究論壇，數學家和電腦科學家可以即時協作，輕鬆地發布程式碼和數學，使用線程和stream 系統，有效地支援多場獨立對話同時進行。

Lean Zulip chat 連結：https://leanprover.zulipchat.com/

Buzzard 表示，他對這個專案將需要多長時間沒有任何預感，但他絕對樂觀。

同時，像 Lean 這類形式化證明工具也在不斷迭代。相較於初代 Lean，現在最新的 Lean 4 版本進行了多項最佳化，包括更快的編譯器、改進的錯誤處理和更好的與外部工具整合的能力等。

去年年底，開放平台LeanDojo 團隊和加州理工學院的研究者也推出了Lean Copilot，這是一款專為大型語言模型與人類互動而設計的協作工具，為數學研究注入了AI大模型的力量。

「我預計，如果使用得當，到 2026 年，AI 將成為數學研究和許多其他領域值得信賴的合著者。」陶哲軒在之前的部落格中說道。

希望陶哲軒的預言早日成真。

相關閱讀：

• 《陶哲軒用 AI 形式化的證明究竟是什麼？一文看懂PFR 猜想的前世今生》

• 《陶哲軒青睞的證明助手Lean，用上了大模型》

• 《大模型幫陶哲軒解題、證明數學定理：數學真要成為首個借助AI實現突破的學科了？ 》

• 《陶哲軒上新專案：Lean中證明素數定理，研究藍圖都建好了》

^{#參考連結：https://leanprover.zulipchat.com/#narrow/stream/416277-FLT}

^{https: //mp.weixin.qq.com/s/d9RSkRhlKH5ZMek3yTqe4Q}

#

以上是跨越300多年的接力：受陶哲軒啟發，數學家決定用AI形式化費馬大定理的證明的詳細內容。更多資訊請關注PHP中文網其他相關文章！