7 月 19 日，Levent Alpöge 在 X 上貼出一行話：Anthropic 的 Fable 模型找到了 Jacobian 猜想在三維的反例——一個懸置了將近一百年的著名問題。隔天，Kevin Buzzard 在部落格寫下：「What a time to be alive」。
LLM 找到 Jacobian 猜想的反例，人類數學家負責驗證
Jacobian 猜想問的是一個看起來很直觀的問題：如果一個多項式映射 F: ℂⁿ→ℂⁿ 的雅可比行列式恆為非零常數，這個映射是不是必然整體可逆？一維時答案顯然是真的，二維至今無人證明或推翻，三維以上則長期沒有已知反例——Kevin Buzzard 在部落格裡形容這是「開放了 100 年」的著名問題。7 月 19 日之後，這句話要改成「三維已經有反例了」，但代價是一連串需要說清楚的分工：誰生成了它、誰驗證了它、誰真正理解了它。
一百年的猜想，一行 X 貼文
7 月 19 日，Levent Alpöge 在 X 上宣布：在與 Akhil Mathew 討論「找更多代數幾何反例」的方向之後，他用 Anthropic 的 Fable 模型找到了 Jacobian 猜想的一個反例，用在了三維（n=3）——一個此前沒有已知反例的維度。Buzzard 隔天在部落格報告這個消息，用的形容是「a big deal」，並補了一句形容：這是代數幾何裡一個懸置了 100 年的著名問題。這句「100 年」不是修辭：Jacobian 猜想的討論可以追溯到很早，中間幾十年裡數學家試過各種構造反例的路數，二維始終原地踏步，三維以上也長期沒有已知反例。
Fable 具體怎麼搜出這個候選，材料裡沒有給出——Buzzard 的部落格只報告了「發現了」這件事本身，沒有描述模型內部的搜尋過程。這一點值得先標記清楚：後面整篇文章要講的驗證鏈，起點是「一個候選出現了」，不是「一個候選被理解了」，這兩者之間隔著整整幾天的人類工作。
「找反例」這種任務，傳統上極度仰賴數學家的直覺與嘗試——次數 7、三個變數的多項式映射，係數的搜尋空間大到沒有窮舉的可能，過去人類找不到候選，不代表反例不存在，只代表沒有人剛好猜對方向。Fable 找到候選這件事值得記錄的，不是「AI 比人聰明」這種空泛的結論，而是它把原本需要人類直覺去猜的搜尋，換成了一次模型推理；至於這次推理背後用了什麼策略、跟人類數學家過去的嘗試有什麼不同，材料完全沒有描述，本文也不替它編。
消息傳開的速度本身也值得留一筆。Buzzard 部落格的發文時間是 7 月 20 日，距離 Alpöge 在 X 上貼出那則消息，中間只隔了 12 個小時。一個懸置將近一百年的猜想被找到反例，從一則社群媒體貼文到一位數學家寫成完整的部落格文章、把驗證鏈的分工講清楚，中間的間隔用「小時」計算而不是「天」或「週」——這個速度差本身，就是這則消息在數學社群裡引起多大反應的側面證據。
下面這張圖把 Terence Tao 後來貼出的三個具體點攤開——三個不同的起點，套進同一個次數 7、雅可比行列式恆為 -2 的映射之後，全部落到同一個終點。點選任一個起點，看它精確的座標與被送到哪裡。
點選任一個起點，看它的座標與映射結果 · 3 個起點
P1 · 起點座標 (0, 0, -1/4)
Tao 部落格貼出的三個點之一。套進這個次數 7、雅可比行列式恆為 -2 的映射後，落在輸出點 (-1/4, 0, 0)——跟 P2、P3 落在同一個點。
P2 · 起點座標 (1, -3/2, 13/2)
跟 P1 相差不只一個座標分量，是貨真價實不同的三維複數點。同一個映射把它送到 (-1/4, 0, 0)，跟 P1、P3 撞在一起。
P3 · 起點座標 (-1, 3/2, 13/2)
第三個相異點，同樣映到 (-1/4, 0, 0)。三個點、一個輸出，就是「雅可比行列式恆為非零常數」不足以推出「整體單射」的直接證據。
這正是「整體單射」失效的教科書樣子——不是某個座標算錯了，而是三個貨真價實、彼此不同的三維複數點，在同一個多項式映射下坍縮成了一個輸出。雅可比行列式恆為非零常數這件事，長期以來被許多人直覺地當成「局部處處可逆」理應疊加成「整體可逆」的證據；三維這個反例證明這個直覺在 n=3 不成立。次數只有 7、係數也不算特別龐大，卻在懸置了將近一百年之後才被找到——這正是這則新聞讓數學家吃驚的地方。
AI 生成候選，人類負責形式化與驗證
Buzzard 部落格最有價值的一段，不是報告「反例存在」，而是解釋這條消息為什麼可信、以及可信的邊界在哪裡。他寫道：Mathlib（Lean 的標準數學庫）並不收錄大量的數學猜想，但 DeepMind 維護的 Formal Conjectures repo 收錄；形式化猜想這件事的重要性在於——如果人類同意某條 Lean 陳述忠實捕捉了猜想背後的想法，那麼檢查「（可能是 AI 生成的）Lean 程式碼是否構成一個證明或反證」就變成一件 trivial 的事。這句話把整條鏈的分工劃得很清楚：陳述本身是否對題，是人類的判斷；陳述一旦確定，程式碼是否邏輯自洽，是機器可以窮舉檢查的事，兩件事不能混為一談。
負責把 Fable 的候選手動形式化進這個 repo 的人是 Paul Lezeau。這一步是人類做的，不是 AI 自動完成的——候選以多項式係數的形式從 Fable 手上交出來，Lezeau 得先把它翻譯成 Lean 能理解的陳述，這個翻譯本身需要判斷「這串符號是不是真的在講 Jacobian 猜想」。翻譯完成之後，Lean 的型別檢查器才接手，確認這串程式碼邏輯自洽，這一段才是 Buzzard 說的那個「trivial」的機器檢查。
這一步為什麼不能跳過，值得想清楚。假設 Lezeau 翻譯陳述時出了差錯——多寫一個條件、少寫一個限制，讓 Lean 陳述其實描述的是另一個比較容易的問題，而不是真正的 Jacobian 猜想。機械檢查依然會通過，因為程式碼邏輯本身完全自洽；但通過的是一個「陳述錯誤的問題」，跟猜想本身無關。這正是 Buzzard 反覆強調「人類需要先同意陳述忠實捕捉猜想」的原因：機械檢查只保證「陳述與證明之間邏輯一致」，保證不了「陳述與猜想之間語意一致」，後者永遠是人類的責任，也是整條鏈裡唯一沒有辦法自動化的環節。
這個分工模式，對每天在寫程式的讀者來說其實不陌生：像極了 code review 加 CI。人類先看一段 diff 到底想解決什麼問題、陳述是否對題——這一步機器做不了，因為機器不知道「對題」的標準在哪裡；陳述確定之後，測試套件才接手，逐項跑過去，這一段才是可以自動化、可以窮舉的部分。差別只在於這裡的「測試套件」是 Lean 的型別檢查器，「diff 的意圖」是一句數學猜想。用 LLM 生成候選解法、再交給型別系統或測試套件驗證，本來就是不少團隊已經在做的事；這次的新聞，只是把同一個模式套進了一個懸置百年的數學猜想。
Buzzard 自己的反應是驚嘆——「What a time to be alive」——但他緊接著把敘事拉回到人類身上：下一步的工作，是讓人類搞清楚這個例子究竟在發生什麼，因為這類工作真正的價值，是讓人類對數學有更好的理解。這句話幾乎是本文整個框架的來源：候選由 AI 生成、程式碼由機械檢查驗證，但「這個反例為什麼成立」這件事，價值仍然歸屬於花時間理解它的人。下面把這條鏈的四段攤開，每一段各自負責什麼、由誰完成。
從一個候選到一個被理解的反例——四段驗證鏈
click a stage above
① AI 生成候選 · 職責邊界
Fable 交出的是一組多項式係數，是「候選」而非「已驗證的反例」。模型內部怎麼搜到這個候選，材料沒有描述。
② 人類形式化 · 職責邊界
把候選翻譯成 Lean 陳述，這一步需要判斷語意是否忠實。Buzzard 強調：人類先同意陳述本身對題，後面的檢查才有意義。
③ 機器檢查 · 職責邊界
只檢查程式碼邏輯是否自洽，不判斷陳述是否忠實捕捉猜想——那是第②段已經做完的事。Buzzard 稱這一步是 trivial 的。
④ 人類重新推導 · 職責邊界
Tao 沒有逐行核對 Fable 或 Lezeau 的具體程式碼，而是自己重新推導一遍；他自己揭露也用 AI chatbot 確認了幾個計算細節，但主體推導是他的工作。
Tao 的「消化」——不是逐行核對，是重新推導
7 月 21 日，Terence Tao 在自己的部落格發文，標題直接叫「A digestion of the Jacobian conjecture counterexample」。他在文章開頭確認了這件事：這個猜想最近被證明在三維是假的（用了 Fable AI）。緊接著他給出了反例的具體樣子——一個 F: ℂ³ → ℂ³ 的多項式映射，次數 7，雅可比行列式恆等於 -2，卻不是整體單射：三個相異的輸入點，(0, 0, -1/4)、(1, -3/2, 13/2)、(-1, 3/2, 13/2)，經過同一個映射，全部送到了同一個輸出點 (-1/4, 0, 0)——正是上面那張圖攤開的三個點。
Tao 沒有選擇逐行核對 Fable 或 Lezeau 給出的具體程式碼，而是把自己的貢獻定位為「消化」（digestion）：他用自己熟悉的工具——對稱冪、判別式——重新推導出一個等價的版本，目標是把整個構造裡「需要奇蹟才成立的地方」降到最少。他自己的原話留了餘地：重寫之後仍然有幾處保留了「remarkable phenomena」，不是每一步都能被拆解成平凡的代數操作。這個誠實的保留，比宣稱「完全理解了」更值得記下。
這個選擇背後有一層數學社群長期以來的習慣可以參照：一個結果如果能被另一位數學家用完全不同的方法獨立推導出來，通常比逐行核對同一份證明更讓人信任這個結果——前者測試的是「這個結論在不同的工具下站不站得住」，後者測試的只是「這一份具體的推導有沒有邏輯漏洞」。Tao 選擇消化而不是逐行核對，等於是把 Fable 生成的候選當成一個未經證實的猜測，用自己的方法重新走一遍，而不是預設它已經正確、只需要挑錯。這個態度差異，決定了整篇「消化」文章讀起來更像一次獨立驗證，而不是一次程式碼審查。
這篇文章結尾附了一句 AI 揭露，原文是「I used an AI chatbot to discuss various aspects of this problem and to confirm several of the calculations」——翻成中文：他用一個 AI chatbot 討論了這個問題的各個面向，並確認了其中幾個計算。這句話值得停下來讀兩遍——它說的不是「AI 幫我做了核心推導」，而是「AI 幫我確認了幾個計算細節」。即便是站在驗證鏈最上游、被視為「人類重新理解」代表的 Tao，在消化一個 AI 生成的結果時，也局部借助了 AI；但主體的重新推導——選擇用哪個代數工具、怎麼把奇蹟數量壓到最少——仍然是他自己坐下來做的工作。這條界線，是整條驗證鏈裡最容易被讀者忽略、也最值得記住的一條。
Tao 在文章裡也順手把猜想目前的狀態釘死，原文是「The conjecture remains open in two dimensions, and is easy to establish in one dimension」：二維仍然開放，一維則容易確立。而他文章開頭那句「false in three dimensions (and thus in higher dimensions as well)」又補上另一個邊界——三維的反例會平凡地抬升，讓四維以上也一併為假；真正還懸著的，只剩二維。至於為什麼三維可以找到反例、二維卻依然卡住，這兩篇部落格都沒有給出解釋——這已經超出 Buzzard 與 Tao 涵蓋的範圍，本文不做超出來源的臆測。
| 維度 n | 狀態 | 依據 |
|---|---|---|
| 1 | 平凡為真 | Tao：「easy to establish in one dimension」——多項式恆導數非零即嚴格單調，直接可逆。 |
| 2 | 仍然開放 | Tao：「remains open in two dimensions」——本次反例完全沒有觸及。 |
| 3 | 現在確定為假 | Tao 確認用 Fable 找到反例；Lezeau 形式化進 Lean、機械檢查通過；Tao 獨立重新推導。 |
| ≥4 | 同時為假 | Tao：三維反例「and thus in higher dimensions as well」——四維以上一併被推翻。 |
兩個維度還沒回答，以及第二個獨立來源
7 月 22 日，中文部落格 gslin 補上這則新聞的第二條佐證。文章劈頭第一句就點出讀者的第一反應：「Jacobian conjecture 居然被 LLM 找出反例了」。gslin 轉述的訊息裡，最重要的一條是：OpenAI 的 Aaron Lou，用另一個關掉網路搜尋功能的內部模型，獨立產生了同一個反例。「關掉網路搜尋」這個細節很關鍵——它排除了「模型只是查到別人已經貼出來的答案」這種最無聊也最需要排除的可能性：兩家不同實驗室、兩個不同模型，在互不知情的情況下收斂到同一個具體的多項式映射。
但這裡要小心一個容易混淆的界線：Aaron Lou 的獨立重現，是「獨立生成」，不是「獨立驗證」。兩個 AI 都吐出了同一個候選答案，增加的是「這個候選不是隨機噪音或記憶污染」的信心；它沒有增加「這個候選在數學上成立」的信心——後者仍然要靠 Lezeau 的 Lean 形式化、以及 Tao 的獨立重新推導去扛，這兩個環節跟 Aaron Lou 的獨立生成，各自站在驗證鏈不同的位置。gslin 自己在文章裡也做了一層獨立核對，但核對的對象也是計算層級：他用 WolframAlpha 驗算了雅可比行列式的數值（-2）、以及其中兩個點映到同一輸出（-0.25, 0, 0）——跟 Tao 貼出的三點版本在數值上吻合。他形容這一步「容易看懂的」，但這個「容易」限定在「核對一條代數等式」這個範圍內，不能推廣成「整個猜想的證明容易理解」。
值得留意的是，這三份材料本身彼此也不是同一種東西：Buzzard 的部落格是最早的現場報告，寫在事件發生後不到一天，帶著第一手的驚訝與尚未沉澱的細節；Tao 的部落格是事後兩天的技術消化，重點放在重新推導而不是複述事件經過；gslin 的部落格則是隔了一天之後、面向中文讀者的整理與二次核對，補上了 Buzzard 與 Tao 都沒有提到的 Aaron Lou 這條線索。三份材料的角色不同，本文引用時也按各自的角色取用——事件經過取自 Buzzard、數學細節取自 Tao、獨立佐證取自 gslin，而不是把三者當成可以互相替代的同一種來源。
把三份材料疊在一起看，能確定的和不能確定的邊界很清楚。能確定的：Jacobian 猜想在三維為假，這件事現在有一條完整的驗證鏈撐著——AI 生成候選、人類形式化陳述、機器檢查程式碼邏輯、人類獨立重新推導。不能確定的：二維依然開放（四維以上則已隨三維反例一併為假）；而且即便是三維這個已解的案例，「AI 找到了什麼」與「人類理解了什麼」也不是同一件事——後者目前仍然停留在 Tao 那篇「消化」文章描述的、還留有幾處「remarkable phenomena」的狀態。Buzzard 那句「下一步是讓人類搞懂這是怎麼回事」，到目前為止還沒有被完全回答完。這幾天反覆出現的幾個詞，精確定義值得放在手邊。
術語小抄——這幾天反覆出現的五個詞
桌面：游標停在術語上看定義 手機：定義直接列在下方
- 雅可比行列式多項式映射 F 在每個點上，各分量對各變數偏導數排成的矩陣（Jacobian 矩陣）之行列式。猜想的前提是這個行列式恆為非零常數。
- 整體單射映射把「不同的輸入」永遠送到「不同的輸出」，沒有任何兩個相異點撞在同一個輸出上。這次反例的三個點，正好證明 F 不滿足這個性質。
- 形式化把一句數學陳述翻譯成 Lean 這類證明助理能理解、能機械檢查的程式碼。Lezeau 做的就是這一步：把 Fable 的候選翻譯進 DeepMind 的 Formal Conjectures repo。
- 消化（digestion）Tao 自己選的詞：不逐行核對 AI 的具體輸出，而是用自己熟悉的工具重新推導一遍等價的結果，目的是把「需要奇蹟才成立」的地方降到最少。
- 候選 vs. 驗證「候選」是 AI 生成、尚未被人類確認的結果；「驗證」是候選經過形式化、機械檢查，或人類獨立重新推導之後才成立的狀態。本文全程刻意分開這兩個詞。
把四天攤開看，時間順序本身就是這條分工的骨架——候選出現、形式化、消化、第二條獨立佐證，一步接著一步，沒有一步是跳過的。
對寫程式的讀者來說，這條分工鏈值得留一個位置在腦子裡，不只是當數學八卦看。用 LLM 生成一段候選解法、丟給型別系統或測試套件驗證，跟這次的流程本質上是同一件事：AI 縮短的是「從零到有一個候選」的時間，人類仍然要花時間確認「這個候選陳述的問題，是不是我真正想問的問題」——這一步永遠繞不過去，也正是 Lezeau 形式化這一步、以及 Buzzard 反覆強調的重點。機械檢查再怎麼快，也只能回答「這段程式碼邏輯自洽嗎」，回答不了「這段程式碼想解決的問題陳述對不對」。這條界線，在數學猜想上是 Lean 形式化，在日常工程裡則是需求陳述或測試案例本身——兩邊守的是同一道關卡。
能確定的與不能確定的：能確定的是三維反例現在立在一條完整的驗證鏈上——AI 生成候選、人類形式化、機器檢查、人類獨立重新推導；不能確定的，是二維猜想的真假，以及「AI 找到了什麼」是否等於「人類理解了什麼」——後面這件事，連 Tao 自己的消化文章都還留了幾處沒拆開的「remarkable phenomena」。