跨越300多年的接力：受陶哲軒啟發，數學家決定用AI形式化費馬大定理的證明 https://www.jiqizhixin.com/articles/2024-05-03-4 機器之心 在陶哲軒的啟發下，越來越多的數學家開始嘗試利用 人工智慧 進行數學探索。 這次， 他們瞄準的目標是世界十大最頂尖數學難題之一的費馬大定理。 費馬大定理又稱為「費馬最後的定理（Fermat's Last Theorem，FLT）」，由17 世紀法 國數學家皮耶・德・費馬提出。 它背後有一個傳奇的故事。 據稱，大約在1637 年左右 ，費馬在閱讀丟番圖《 算術 》拉丁文譯本時，曾在第11 卷第8 命題旁寫道：「將一個 立方數分成兩個立方數之和，或一個四次冪分成兩個四次冪之和，或者一般地將一個高於 二次的冪分成兩個同次方之和，這是不可能的。 這段話前面所表述的就是費馬大定理的內容：當整數n>2 時，關於x^n + y^n=z^n 的方程 式沒有正整數解。 費馬表示，自己知道怎麼證明，但因為書的空白部分太小，所以沒寫。 對於該故事的真 實性以及費馬是否真的想出了證明方法，後世是存在爭議的。 在接下來的300 多年裡，數學家一直在努力，接力證明費馬大定理。 直到1995 年，美國 普林斯頓大學的Andrew Wiles 教授經過8 年的孤軍奮戰，終於用130 頁長的篇幅完成了 證明。 Wiles 也成為整個數學界的英雄。 既然費馬大定理已經被證明了，數學家還能用AI 做什麼？ 答案是：形式化它的證明。 數學的形式化通常指的是使用嚴格的形式語言（如 邏輯 和集合論）來表述數學對象、結 構、定理和證明，使其能夠在計算機上進行表示、驗證和操作，從而保證數學內容的準確 性和一致性。 去年年底，陶哲軒等人曾用Lean（一款互動式定理證明器，也是一門程式語言）形式化了 他們的一篇論文。 這篇論文是多項式Freiman-Ruzsa 猜想的一個版本的證明，於去年11 月發佈在arXiv 上。 在寫Lean 語言程式碼的時候，陶哲軒也藉助了AI 程式設計助手 Copilot。 該事件引起數學界和 人工智慧 界的廣泛關注。 當時，Lean 技術開源社群最重要的推廣者、倫敦帝國學院的Kevin Buzzard 表示：「從 根本上來說，顯而易見的是，當你將某些東西數位化時，你就可以以新的方式使用它。我 們將把數學數位化，這會讓數學變得更好。 這位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 將成為數學研究和許多其他領域值得信賴的合 著者。」陶哲軒在之前的部落格中說道。 希望陶哲軒的預言早日成真。 --

※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 114.38.27.129 (臺灣) ※ 文章網址: https://webptt.com/m.aspx?n=bbs/Math/M.1714741883.A.73A.html