摘要： Anthropic 研究員 Levent Alpöge 表示 Claude Fable 找到雅可比猜想反例，隨後在 Lean 定理證明器通過機器檢驗。該複三維七次多項式映射的 Jacobian 行列式處處為 −2，卻不可逆，否定三維以上的一般版本。文章強調結果仍待同儕審查，但社群已在約 48 小時內完成形式化驗證。
7 月 19 日入夜後，世界盃決賽佔據了全球多數人的目光。就在同一個週末，Anthropic 的研究員 Levent Alpöge 在 X 上發文表示，Claude Fable 已經找到雅可比猜想的一個反例。這則貼文累積超過兩千萬次瀏覽；更值得留意的是數學社群接下來做的事——他們沒有先去爭論，而是連夜投入驗證。帝國理工學院 Xena 計畫的 Kevin Buzzard 隔天早上醒來時，這個反例已經在 Lean 定理證明器中通過機器檢驗。
雅可比猜想的源頭是 Jacobi 對行列式的研究，1939 年由 Keller 給出形式化的版本：若一個多項式映射的 Jacobian 行列式為非零常數，這個映射是否必然可逆？一維的情形顯而易見，二維至今仍未解，而這次的反例直接否定了三維以上的一般版本。陶哲軒另外補充，它處理的是 Smale 問題清單第 16 題所指的廣義形式。
這個反例的具體樣貌
依陶哲軒 7 月 21 日的文章所述，這是在複三維空間上被明確寫下的一個七次多項式映射：它的 Jacobian 行列式處處等於 −2，卻把三個相異的點送到同一個像點，因此不具可逆性。Tao 的幾何式「消化」從一個乘法映射出發——把線性齊次式與二次齊次式相乘得到三次式——這個映射 generically 是三對一；接著以結式把縮放對稱正規化，得到局部單射（étale），再切出一個三維仿射超平面切片。當對應的三階微分算子恰好有兩個重根時，切片上的多項式便同構於仿射空間，反例於焉成形。在 Tao 筆下，這個構造近似一場機率極低的「大規模抵銷」，靠暴力搜尋很難撞上。
48 小時內完成驗證：從社群貼文到 Lean
決定一個反例地位的並不是貼文，而是驗證。Tao 指出，這裡的驗證只是一段簡短計算，具備中學以上的數學能力就能自行檢查；Paul Lezeau 以手動方式把命題形式化，並向 DeepMind 的 Formal Conjectures repo 送出 PR。陶哲軒則發文消化整個構造，同時透露自己也曾借助 AI 聊天機器人反覆核對計算；他與 ChatGPT 針對這個反例的對話紀錄後來被公開分享，並被轉貼到 Hacker News。目前這項結果仍標記為「待同儕審查」，但重點在於它具備機器可驗證性，社群可以一邊審查、一邊使用。
興奮與不安：數學家心中的兩種情緒
Buzzard 在 Xena 部落格寫下〈人類數學家正在被反例超越〉一文，逐一盤點這個夏天發生的事：5 月 20 日 ChatGPT 推翻 Erdős 單位距離猜想，OpenAI 的 Sol 模型把它完整形式化進 Lean；同一個 Sol 又針對 Grothendieck 約六十年前提出、關於 n 階群簇的問題給出反例，而 Claude Fable 在 Akhil Mathew 分享 12 頁 PDF 之後，四小時內就自動完成形式化。他的結論是「大型 AI 生成的數學進展不可避免」，並稱這是「重大的一天」。芝加哥大學的 Mathew 則以「非常快速、令人非常不安的變化」形容這一切，對資淺數學家尤其如此：AI 給得出「怎麼做」，卻給不出「為什麼」。Buzzard 再補上一刀：機器提問的能力「爛透了」，你得先是出色的數學家，才問得出正確的問題。
這一週對 AI 工程的啟示
這一週展示了一條已經能運作的新流程：模型負責生成、形式系統負責驗證、人類負責補上理解。其中有三件事可以直接借用。首先是把「可信」外包給驗證器——Lean 之於數學，如同測試與型別之於程式碼；Buzzard 的做法是在沙箱裡執行 AI 產生的程式碼，只驗證編譯是否通過、陳述是否符合 mathlib 慣例。其次是前沿實驗室已經把真實研究問題當成高風險的評測場域，數學結果成為模型能力的公開戰場。第三，瓶頸轉移到問題選擇上：生成反例的邊際成本趨近於零，判斷「哪個問題值得問」的價值反而上升。