這幾週來反例領域出現了許多有趣的發展。本文主要是我對形式化、AI 工具，特別是反例領域近期發展的看法。

單位距離

就在兩個月前的今天（2026 年 5 月 20 日），ChatGPT 推翻了 Erdős 在離散幾何中的單位距離猜想。這已經是舊聞，但我必須從這裡開始。官方公告附上了多位人類數學家的證言，其中有許多是我認識的，也有幾位是我信任的，他們表示相信這個論證（他們事先獲得存取權限並已驗證過）。證明的核心結構是利用 1960 年代 Golod 與 Shafarevich 提出的數論深刻定理，來建構該猜想的反例。

自從我九年前經歷中年危機、不再信任許多人類數學家在技術細節上的判斷、發現 Lean，並開始主張互動式定理證明器應在數學未來中扮演重要角色以來，我的第一個問題當然是：「這個反例是否已用 Lean 形式化？」答案是「還沒有」。

但不到一週後（2026 年 5 月 26 日），我收到 Fields 獎得主 Mike Freedman 的電子郵件。Mike 現任 Logical Intelligence 的首席科學官，該公司由圖靈獎得主與「AI 教父」Yan LeCun 共同創辦。Mike 告訴我，他們的系統已將 ChatGPT 生成的整篇論文自動形式化至 Lean，並問我是否願意查看。我看了，我的博士後 Thomas Browning 也看了。確實，Logical Intelligence 所做的正是：他們形式化了「數論深刻定理蘊含 Erdős 反例」這一陳述。突破性的 LLM 生成數學成果即時被形式化。這是一個有趣的資料點。

當然，房間裡的大象依然存在：那個需要 100 多頁證明的數論深刻定理（它需要大量全域類域論的內容，而類域論是 20 世紀初發展出來的理論，至今仍無簡短證明；壓縮它相當困難）。2025 年，我曾與 Richard Hill 共同主持 Clay 暑期學校，主題是類域論的形式化；一年後，我們已接近完成局部情形（這是我學生 Edison Xie 目前的博士研究主題）；全域情形仍屬開放，而在 2025 年形式化全域類域論仍像天方夜譚。

一個月後，2026 年 6 月 26 日，我對可能性的認知再次改變。Boris Alexeev 在 Lean Zulip 宣布，他引導 ChatGPT 完成了 Erdős 反例的完整形式化，僅依賴數學公理。Boris 在 OpenAI 工作，並使用他們的新模型 Sol 進行自動形式化。Boris 公開了程式碼，我很快發現，在這些 AI 生成（有時很糟糕，有時還不錯）的程式碼中，確實包含對全域類域論中某些極困難定理的證明。另一個讓我感興趣的地方是，Sol 在三週內生成了 120 萬行 Lean 程式碼。而 Lean 優秀的（利益揭露：我是維護者）數學函式庫 mathlib 目前只有 230 萬行程式碼，且花了九年才完成。或許就在這個時刻，我才真正理解——大規模 AI 生成的數學發展已不可避免。我們無法信任 AI 生成的程式碼，因此我在自己的機器上用沙箱執行它（惡意 Lean 程式碼可以執行電腦上的任意指令——畢竟 Lean 是一種程式語言）。確實，它正在證明關於數域上同調的一些非平凡定理。哇。

階數為 n 的群概形

Boris 發表消息後一週，七月初，我正認真思考如何舉辦我的 形式化費馬研討會。這場研討會由 Logos Research 贊助，該公司與 Logical Intelligence（以及 Harmonic、Axiom AI、Moonshot AI 等）一樣，擁有可將數學從自然語言自動形式化至 Lean 的工具，並建構在 mathlib 之上。Logos 告訴我，研討會期間他們的系統將同時只開放給 5 人使用，而參加者有 25 人，因此我告訴所有參加者，我會為他們購買一個月的 Claude Max 訂閱，以便輪不到 Logos 工具時他們仍有東西可以實驗。研討會於 7 月 6 日至 10 日舉行，而 Claude Max 訂閱將讓參加者至少在 7 日星期二之前能存取 Claude Fable，之後它將被關閉。當 OpenAI 得知我的安排後，也提供所有參加者一個月的免費 ChatGPT Pro 存取權；這是個大事，因為 ChatGPT Sol 將於 9 日推出。因此，基本上所有參加者在研討會的 5 天中有 4 天可以存取 Sol 與 Fable，而 Logos 的工具則可使用整整一週。實際上 Fable 的存取權並未在 7 日被移除，所以我們的情況甚至更好。

我原本不確定 Logos 的工具會有多好，但我需要有限平坦群概形的理論發展來支持我正在進行的費馬最後定理證明，因此我上傳了一些該領域的經典論文給 Fable 與 ChatGPT，請它們合作撰寫該理論的自然語言說明。我在研討會前一天將這份 PDF 文件交給 Logos，研討會第一天他們就說 PDF 中的某個主張是錯誤的，並找到了明確的反例。又是一個反例！我看了，確實 LLM 生成的 PDF 在描述某個標準建構時出了錯；虛驚一場。雖然我在閱讀 PDF 時也漏掉了這點。有趣的是，AI 再次找到了反例。我修正了 PDF。我覺得有趣的是，AI 並沒有只說「我不太理解這個論證」，而是說「這裡有證明這個論證根本是錯的」，這是一個更強有力的陳述。

有限平坦群概形理論的發展回到正軌後，我得以放鬆並投入 FLT 研討會。7 月 7 日星期二，我在午餐時與 Akhil Mathew 面對面坐著；Akhil 是芝加哥大學的數學教授，也是參加者之一，他一直在實驗可用的工具。我們討論了 AI 可能處理的潛在問題，Akhil 提出了 Grothendieck 的老問題：是否每個階數為 n 的有限自由群概形都被 n 所消滅。Deligne 已證明交換情形的結果，Grothendieck 則證明了基底為約化時的情形；Rene Schoof 證明了更多情形，去年甚至有 Emiliano Torti 發表一篇論文，將結果推廣到更一般的設定。我說這是個讓 AI 思考的絕佳問題。

研討會結束後的隔天，7 月 11 日星期六，我收到 Akhil 的私人訊息，告訴我 Sol 找到了一個反例。他傳給我一份 12 頁的 PDF。我立刻回覆說，我不會閱讀 AI 生成的非形式化數學，並請他將整個內容形式化到 Lean。四小時後他再次回覆，說 Fable 已將整個內容自動形式化。我掃描了 1076 行的 Lean 檔案，確認程式碼不會刪除我硬碟上的所有檔案（Lean 是一種程式語言，所以它可以這麼做）。確信它只包含定理後，我在筆電上編譯它，花了不到五分鐘就確認：(a) 所聲稱定理的陳述僅使用了 mathlib 中的概念（因此像 HopfAlgebra 這樣的東西可以被信任為數學家所理解的 Hopf 代數）；(b) 所聲稱定理的陳述是存在一個反例；(c) 證明可以編譯。此時我知道我們找到了一個反例——一個階數為 4 但不被 4 消滅的群概形。我建議 Akhil 將這個反例提交 PR 到 mathlib——他這樣做了。我本來也想建議他起草一份新聞稿，說機器解決了 Grothendieck 在代數幾何中 60 年前提出的問題，但不知怎的，此時我幾乎對這一切都已經免疫了。不清楚媒體是否能區分「機器解決 Erdős 的問題」與「機器解決 Grothendieck 的問題」，即使我個人認為後者更有趣。當然，Grothendieck 的反例遠比 Erdős 的反例容易（一千行，而非一百萬行），我只是說這是我個人更感興趣的數學領域。我向 Akhil 指出，機器似乎越來越擅長找反例，並建議他接下來試試 Hodge 猜想。

模性提升定理

我認為此時值得退一步，審視人類專家對這類事情的態度。7 月 14 日星期二，我去帝國學院工作，Grothendieck 反例成了午餐話題。一位（我不具名）的教職員對我說，這個反例如此容易被找到，只是表示人類對這個問題的思考時間還不夠，暗示 Grothendieck 60 年前提出的問題其實並不是那麼值得研究。我沒有告訴他，我在職業生涯的某個階段曾花了一週時間認真研究這個問題。在我看來，我的同事正在經歷悲傷的五個階段；目前他們似乎處於否認階段。

午餐後，我與博士生 Andrew Yang 會面，他一直在用 Lean 形式化一個模性提升定理，這對我的 FLT 工作至關重要。Andrew 參加了 Logos 的 FLT 研討會，現在可以存取 Sol 和 Fable。他告訴我，使用這些工具，他在大概兩週的時間內寫了 25 萬行 Lean 程式碼，基本上完成了整個專案。

幾天前，我收到帝國學院數學系一位教授的電子郵件，他對我們的一些研究生每月支付 200 美元存取 Sol 和 Fable 這類模型感到驚訝。他說他認為這些人瘋了。我當時沒有立即回覆。但在與 Andrew 會面後，我回信告訴那位教授，在我看來，任何不支付 200 美元存取這些工具的博士生才是瘋了。實際上，在研討會期間，我從哈佛博士生 Bryan Wang 得知，哈佛已經為所有哈佛的博士生、博士後研究員和教職員提供免費的 Fable 存取權。

Jacobian 猜想

但回到 Akhil。我不確定他是否認真考慮了我提出的反駁 Hodge 猜想的想法。但看來他已經深刻理解，透過這些非凡的新 AI 工具，反例目前可能是低垂的果實。他與 Levent Alpöge 討論了在代數幾何中尋找更多反例的想法，而就在 12 小時前，Levent 在 X 上發文表示，Fable 找到了 Jacobian 猜想的反例。這是個大事——這是代數幾何中一個著名的問題，已開放 100 年，許多人都曾思考過。它據說是在 2026 年世界盃決賽期間被解決的。

我今天醒來收到 Akhil 的私人訊息，說「我應該再提交一個 PR 嗎？」但這次他來不及了——Paul Lezeau 已經手動形式化了這個反例，並已向 DeepMind 的 Formal Conjectures 儲存庫 提交了 PR。Mathlib 並不包含數學中大量猜想的清單，但 DeepMind 的儲存庫有。對猜想進行人工形式化的重要性在於，如果人類同意某個 Lean 陳述忠實捕捉了某個猜想背後的想法，那麼檢查（可能是 AI 生成的）Lean 程式碼是否構成對該猜想的證明或反駁就變得非常簡單。恭喜 Levent，感謝 Akhil 向他建議這個問題，也感謝 DeepMind 已經形式化了該陳述，從而讓反例的形式化驗證變得微不足道。

Jacobian 猜想已解決！哇！接下來的工作是讓人類確切理解這個例子到底發生了什麼。這種工作的真正價值在於讓人類對數學有更深入的理解。實際上 Akhil 一直在試圖以遠比「這裡有一個隨機環的隨機表示和一個隨機計算顯示某事不成立」更深入的方式理解 Grothendieck 的反例。我們接下來需要的是從這些非凡例子中能得出的洞見。

這是個活在其中的好時代。