在 Day 1、也就是本次鐵人賽開頭，筆者比較了 2022 年剛問世的 ChatGPT 與 2026 年的、當今最前沿的 GPT-Astra 模型放在一起比較，可以看到四年後，聊天視窗裡的回答能力已經很不一樣，模型仍然沿著同一個基本動作生成文字：讀完前文，預測下一個 token。next-token predictor 依然貫串了生成介面，但沒有告訴我們這套系統最終具備多少可驗證的解題能力。

三十天後，這個問題被推到更難的地方：一個足以推翻八十多年猜想的反例、一份補上二十多年缺口的普遍定理，以及黎曼 ζ 函數的新下界。當模型能輸出這些結果，我們究竟憑什麼相信它？

今年夏天，Anthropic 與 OpenAI 各自公布了數項前沿數學、理論科學的成果，有的來自未公開研究系統，有的出現在數學家與前沿模型的協作中；它們都不能直接換算成一般聊天介面面對任意題目的能力。公司公告、可下載手稿、形式化證明、外部數學家的重建與傳統同儕審查，也各自代表不同層級的證據。

第一個案例，只要一個反例，就能讓八十多年的猜想倒下。先從一元函數想起。若一條曲線在某點的導數不為零，它在那個點附近不會突然折平，通常可以局部反解；換成多個輸入與多個輸出，導數便成為一張偏微分組成的 Jacobian 矩陣，而它的行列式用來判斷這個局部變換有沒有把空間壓扁。

Jacobian 猜想問的是更強的事。對一個從複數空間映到自身的多項式映射 F: C^n -> C^n，如果 Jacobian 行列式處處都是同一個非零常數，局部可逆是否足以保證 F 在全域也有多項式反函數？一維時答案是容易且直觀的；但到了多維，局部每一小塊都正常，遠處的兩個點仍可能被送到同一個位置。這有點像每個街口的道路都沒有斷裂，整張路網卻可能繞回同一個終點。

2026 年 7 月，Anthropic 數學家 Levent Alpöge 公布一個由 Claude Fable 產生的三維、七次多項式映射；後續文獻也記錄了這項發現與歸屬。令 s = xy、u = 1 + s，它的三個輸出座標可以完整寫成：

F1 = u^3 z + y^2 u(4 + 3s)
F2 = y + 3xu^2 z + 3xy^2(4 + 3s)
F3 = 2x - 3x^2 y - x^3 z

把這個 F 代入，可以用精確有理數核對下面兩件事：它的 Jacobian 行列式恆為 -2，三個不同輸入卻撞上同一個輸出。

det DF = -2

F(0, 0, -1/4)
= F(1, -3/2, 13/2)
= F(-1, 3/2, 13/2)
= (-1/4, 0, 0)

第二行已經也除去了「也許它仍可逆」的藉口和退路，若反函數存在，同一個輸出不可能同時還原成三個輸入。反例成立後，三維 Jacobian 猜想被否定，後面再添上不受影響的座標，也會把反例帶到所有更高維；不過二維情況沒有因此解決，仍然是開放問題。

短短一組碰撞座標，不代表這個例子很容易找到。七次三變數映射共有數百個係數；Jacobian 行列式原本可能一路長到十八次，最後卻要讓所有非常數項精確消失。Terence Tao 在他的逐步拆解中指出，若粗略把每個應消失的單項式係數都視為一項條件，大約是 1,329 項條件壓在 360 個映射係數上。它們並非彼此獨立，這個數字仍足以說明模型找到的是一個高度結構化的抵消，不是隨手抽到的亂數多項式。

這也是三個案例裡最接近「答案可在短時間內獨立重播」的一個。Tao 把龐大的公式整理成較能看見結構的推導；Peng Gao 隨後給出自足的幾何解釋與推廣，也以精確算術和 Gröbner basis 核對關鍵性質。這些工作沒有替最初的公開貼文做驗證，卻把原本只能相信一大串係數的結果，轉成其他數學家能重新計算和理解的可靠依據。

第二個案例，沒有一組座標可以替普遍定理作證。想像裁判把一對相關問題分別交給 Alice 與 Bob。兩人事前可以商量策略，收到問題後不得通訊，各自回答；裁判再依兩個答案判定是否過關。這叫做雙人單輪遊戲（two-player one-round game）。若允許 Alice 與 Bob 事先共享糾纏態，他們可使用量子測量協調答案，而 ω*(G) 表示在單局遊戲 G 中能達到的最佳勝率。

現在把同一種遊戲獨立出題 n 次，要求每一局都答對。直覺會把單局勝率直接乘成 ω*(G)^n，但這一步不能偷渡：Alice 和 Bob 可以對手上的整批問題做聯合測量，把不同局的策略糾纏在一起。題目是獨立抽的，不表示最佳策略必須逐局獨立。量子平行重複問題真正要證明的，是只要原遊戲不可能百分之百獲勝，全部過關的機率仍會隨重複次數快速下降。

OpenAI 公布的 Astra 結果對所有有限的雙人單輪糾纏遊戲給出肯定答案。若 ω*(G) < 1，就存在只依賴原遊戲的正常數 c_G，使得：

ω*(G^⊗n) <= exp(-c_G n)

若用 ε = 1 - ω*(G) 表示單局離百分之百成功還差多少，手稿給出的指數常數包含 ε^13 / (ε + log(|A||B|)) 這個尺度，其中 A、B 是兩人的答案集合。這個十三次方是目前證明付出的價格，作者沒有宣稱它已經最佳；對本文最重要的結論，是固定任何一個 ω*(G) < 1 的遊戲後，成功率一定以指數速度下降。

右邊是指數衰減。重複次數每增加一段，全部作弊成功的機率便再乘上一個固定小於 1 的比例。這類結果是互動式證明（interactive proof）做錯誤放大的數學地基：一次檢查若還留有漏洞，可以平行重複，讓不誠實的證明者全部蒙混過關之機率迅速縮小。古典兩人遊戲早有 Raz 的平行重複定理，允許共享量子糾纏的一般版本則從至少 2004 年起一直缺少同樣的指數界，先前的一般結果只能保證多項式速度的下降。

它和 Jacobian 反例的驗法完全不同，抽查十個遊戲、跑到一千次重複，都不能證明「所有有限遊戲、所有 n」；真正承擔這個全稱量詞的是長證明。完整手稿列出定理的精確常數與假設，OpenAI 表示 Astra 產生論證，研究人員整理手稿，並把各項結果寫入可編譯的 Lean repository。Lean 能逐步檢查形式化敘述是否確實由列出的定義、公理與前述 lemma 推出，比只看 PDF 最後一行多了一道機械防線。

Lean 檢查的是「寫進 Lean 的敘述」，自然語言手稿是否完整對應、定理是否新穎、假設是否涵蓋數學家以為它涵蓋的範圍，仍要另外審查。一份截至 8 月 25 日的外部稽核只檢查了量子平行重複章節的一部分。初版曾報告一處正負方向錯誤（polarity error），後來發現是從 PDF 擷取文字時漏掉上橫線，因而撤回；這意味著 verifier 本身也會讀錯輸入，但至少可確認受檢視的片段沒有留下已確認錯誤。

第三個案例則是解決黎曼猜想失敗的成果，這個數學界最負盛名的未解之謎，突然成為前沿 AI 公司比較誰家的模型比較厲害的戰場。黎曼 ζ 函數最初可在實部大於 1 的區域寫成 ζ(s) = 1 + 1/2^s + 1/3^s + ...，再用解析延拓把它帶到更大的複數平面。它的非平凡零點落在 0 < Re(s) < 1 的臨界帶（critical strip）；黎曼猜想主張它們全部位於中央的 Re(s) = 1/2。這條線因此叫做臨界線（critical line）。

零點是否在臨界線上是一個問題，是否為單根又是另一個問題。單根表示該位置只出現一次，等價地說，在這個零點 ρ 上有 ζ'(ρ) != 0；重根則像多個零點疊在同一位置。數論學家希望知道臨界線上有多少單根，因為「位於正確位置而且沒有重疊」比單純數到一個零點提供更多結構。

在 Claude 嘗試黎曼猜想但沒有成功的研究過程中，Anthropic 報告了一項旁支成果：把已知「位於臨界線上的單根」之無條件比例下界，從 5/12，也就是約 41.67%，推進到 67.25%。論文先給出較整齊的 2/3 與 5/6 結論，再用最佳化過的 Montgomery–Taylor 視窗函數取得更細的數字：

先前的單根下界          5/12 = 0.4167
本文的整齊版            單根 >= 2/3；互異 >= 5/6
最佳化視窗函數          單根 >= 0.6725；互異 >= 0.8362

這些都是當零點高度趨向無限時的漸近下界，分母將非平凡零點連同重數一起計入；它們不是研究者實際觀察到「只有 67.25%」在臨界線上。結果保證至少這麼多，真實比例可以更高；黎曼猜想要求的則是所有非平凡零點都在臨界線上。換句話說，這份論文大幅推高我們能無條件證明的地板，沒有碰到 100% 的天花板，作者也明確表示目前機制不會自行把 2/3 推成全部。

它的核心想法，可以先把無限多個零點暫時投影成一張有限的 Hermitian（厄米）矩陣。矩陣的元素由精心選取的測試函數與 Weil 型二次形式組成；臨界線單根、離開臨界線而成對出現的零點，以及可能的重根，會對矩陣的秩、trace（跡）、平方大小與正負慣性指標施加不同限制。接著用線性代數不等式估計至少必須保留多少個特定符號的 eigenvalues（特徵值），再把這個數量翻譯回零點比例。這不是把 ζ 函數直接丟進數值程式數一遍，而是先設計一個會替零點類型留下「影子」的有限物件，再證明那個影子不可能太小。

發現過程並非一段 one-shot prompt 就能產出一段完整證明，畢竟這可是猜想界的皇冠呢。Anthropic 的紀錄顯示，第一輪約 650 個想法沒有成功；第二輪動用約 60 個子代理，產生 3,100 萬個輸出 token、執行約 2,400 次 shell 指令，寫下數百支 Python 程式、做過數千次數值檢查，並下載 54 篇 arXiv 論文。大量搜尋本身不構成證明，卻能淘汰不成立的 lemma、尋找可用文獻與測試常數，最後留下的下界則近進入紙筆驗證的工作。

Anthropic 的數學家 Levent Alpöge 與 Ralph Furman 檢查成果，並整理成給專家閱讀的短註；Brian Conrey 與 Dan Goldston 則在有限時間內檢視手稿。團隊另公開形式化 repository，相關 Lean 檔案可通過標準 comparator，正式證明不含 sorry。形式化可以抓出推導斷裂，專家重建可以檢查自然語言與既有文獻，之後更廣泛的審閱則可能找到兩者沒有問到的問題。

三個案例真正不同的，是驗證成本。

Jacobian 反例        明確映射 + 常數 Jacobian + 一組全域碰撞
量子平行重複定理    精確假設 + 普遍量化的長證明 + 形式化與外部審讀
黎曼 ζ 函數下界     既有文獻 + 比例定理 + 專家重建 + 形式化

回到 Day 21 那道 4^6 = 8^n。一份 trajectory 第一行先寫 n=3，最後交出 boxed 4，final-answer verifier 仍會給 1 分，因為它只負責最後答案。今天的三個案例當然沒有這個簡單的答案：反例要核對 witness，普遍定理要承受全稱量詞，數論下界還要分清楚「至少多少」與「真實上有多少」。若把它們都壓成公司自己報告的成功標記，RLVR 裡最熟悉的 reward-design 問題就會原封不動地回來。

因此，前沿數學中的 verifier 比程式判定更仰賴證據鏈，電腦代數負責精確展開，proof assistant 負責型別與推導規則，數值實驗負責找反例與測試猜測，領域專家負責判斷形式化之外的含義，公開審閱則讓其他人有機會重新計算。每一層都能抓住不同錯誤，也都可能漏掉自己看不見的部分。

這三項成果再次證明大型語言/推理模型「只是在預測下一個 token」這句話顯得更加可笑和無知，我們更該討論的是推理模型交出的反例能否重算、定理能否重建、形式化能否編譯。Next-token prediction 描述訓練目標，沒有直接決定一個配上搜尋、程式工具、形式化系統與多輪修正的研究流程，最後能產生什麼可供外界核查的數學物件。

所以最後一天的鐵人賽，我並不會用「我們終於打造出會推理的模型」收尾（事實是這樣的模型早已存在，而且已經能做到超出絕大多數人類所能做到的事情），我們手上的 Qwen 3 0.6B 系統依然會算錯、選錯工具，也可能在 verifier 提醒後繼續犯錯，但 prompt、sampling、evaluator、SFT、RLVR、蒸餾、工具調用、checkpoint 選擇、與失敗後如何恢復推理歷程，這些工程工作不論是各自存在或連結起來，都是有意義的；模型的答案也不再因為語氣像證明，就自動被當成證明。

鐵人賽到此完賽。