Claude 拉 60 個 subagents 攻黎曼猜想：67.2% 進展到底有幾實在
未發布模型用一日半整理舊研究，再由 Lean 核對證明
Claude 冇解開黎曼猜想
先講清楚：Claude 冇證明黎曼猜想，亦冇搵到反例。黎曼猜想主張，黎曼 zeta 函數所有非平凡零點都落喺實部等於 1/2 嗰條「臨界線」上。今次 Claude 處理嘅係一個相關但細好多嘅問題：數學家最少可以保證幾多比例嘅零點落喺條線上。舊紀錄係 41.6%，Anthropic 公開嘅 paper 就將下限推到約 67.25%。
圖片：Anthropic
41.6% 升到 67.2%，實際代表咩
呢個百分比唔係抽樣檢查一批零點，再數有幾多個合格；佢係一個面向無限多零點嘅數學下限。份證明所講嘅 67.2%，即係當觀察範圍一路擴大，至少約三分之二嘅零點都係簡單零點，而且落喺臨界線上。41.6% 嗰個紀錄由 2020 年維持到而家，所以一次跳高約 25.6 個百分點，數學份量相當大。不過餘下約三分一只係證明未涵蓋，唔代表佢哋離開咗臨界線。
60 個 subagents 點樣分工
Anthropic 披露，未發布研究版 Claude 用兩個 Claude Code sessions、合共輸出 3,100 萬個 token。第一次試咗 650 條路線都失敗；第二次就花一日半協調約 60 個 subagents，跑咗 2,400 條 shell 指令、寫咗數百個 Python scripts，又用已知 zeta 零點做數千次數值檢查。搵到結果之後，佢哋下載 54 份 arXiv 論文查重、搵反例，再安排另一批 agent 由頭重證一次。
官方公開嘅分工亦幾有啟示：60 個 agent 入面，得兩個發展出關鍵數學想法，13 個提供線索，30 個嘗試開新路但冇成果，另外 13 個負責驗證，最後兩個協助寫 paper。多 agent 系統嘅價值主要係同時試大量方向，再將失敗路線快速淘汰。不過全部都係同系列模型，互相覆核始終有機會共享盲點，唔可以當成 60 位獨立研究員嘅判斷。
新意來自重新接駁舊研究
Claude 用到 Baluyot、Goldston、Suriajaya、Turnage-Butterbaugh 近年對零點 pair correlation 嘅成果，再接上 Bombieri 2000 年研究，改用二次型、矩陣 rank 同正負特徵值處理離開臨界線嘅零點。模型冇憑空發明成套數論，而係搵到新方法接駁舊研究，令以往受條件限制嘅工具都計到無條件下限。呢類跨幾十份專門文獻搵接口嘅工作，正好啱長時間 agent 發揮。
Lean 過關有幾大保證
Anthropic 公開咗 Lean 4 repo，聲稱 Theorem A 至 E 都有完整、冇 sorry 嘅形式化證明，定理直接用 Mathlib 嘅 riemannZeta 定義，headline results 亦冇額外假設。官方話份 formalization 已通過 comparator。呢點強過淨係跑數值測試，因為 Lean 會逐步核對推理有冇跟規則；但佢唔會判斷研究係咪真係首創、寫法有冇漏講背景，亦代替唔到數論專家檢查形式化陳述有冇準確對應 paper 想講嘅結果。
而家仲欠獨立驗證
Anthropic 兩位內部數學家 Levent Alpöge 同 Ralph Furman 已研究及驗證份 paper；公司亦多謝 Brian Conrey 同 Dan Goldston 喺短時間內睇過。不過截至 8 月 11 日，官方冇公開兩位外部專家嘅詳細評語，亦未見正式同行評審結果。官方亦未公開模型版本、3,100 萬個 token 嘅調度方法同完整執行環境，外界暫時未能照住重現成個流程。下一步要睇數論界能否獨立重跑 Lean artifact、逐頁審核證明，再確認新下限站得穩。
今次較實在嘅進展，係一套 AI agent 可以持續一日半拆工作、搜尋文獻、寫計算工具、互相挑錯，最後交出人類同 proof assistant 都有得核對嘅成果。對科研人員同開發者嚟講，呢種有證據鏈嘅半自主助手已經值得試；至於可唔可靠處理其他開放問題，就要等更多團隊用公開模型同可重現設定驗證。
參考來源
- TechCrunch — An unreleased Anthropic model made progress on one of math’s biggest unsolved problems — original report
- Learning more about Claude's mathematical capabilities — Anthropic 官方披露模型狀態、token 數量、研究時間、subagents 分工同驗證安排。
- More than two thirds of the zeros of the Riemann zeta function lie on the critical line — Claude 署名嘅技術 paper，列出 67.25% 下限、證明方法、歷史紀錄同方法限制。
- Zeta23 Lean 4 formalization — 公開 Lean artifact，交代形式化範圍、依賴版本、定理陳述同 axioms audit。
- An unconditional Montgomery Theorem for Pair Correlation of Zeros of the Riemann Zeta Function — Claude 結果依賴嘅同行評審背景研究，解釋點樣移除 Montgomery 方法原有嘅部分條件。
- Pair Correlation of Zeros of the Riemann Zeta Function I — 相關 primary research，交代 2/3 比例、臨界線零點同 pair-correlation 方法嘅既有進展。
本文根據原文及公開資料整理；資料有出入時，以原文及官方資料為準。
