中國醫生用 GPT-5.6 破解懸宕 22 年的 Crouzeix 猜想本人親自證實「正確」

編按：本文綜合整理自 IT 之家〈中國醫生用 GPT-5.6 破解 22 年數學難題〉（2026-08-14）、南華早報（SCMP）原始採訪、康奈爾大學 Alex Townsend 與華盛頓大學 Anne Greenbaum 共同撰寫的 SIAM News 專文〈The Neurosurgery Resident Who Proved Crouzeix’s Conjecture〉（2026-08-11）、預印本平台〈The Numerical Range Is a 2-Spectral Set〉（preprints.org 202607.1919）、jinshanmu/CrouzeixConjecture 公開 GitHub 倉庫（含 Lean 4 形式化與提示詞）、OpenAI 官方〈Ten Advances in Mathematics〉、多位 X 平台學者評論（@Dr_Singularity、@polynoamial、@SebastienBubeck），並加入 Siami 編輯部觀點與分析。

事件：22 年猜想在 16 小時內被 GPT-5.6 證明

2026 年 7 月 27 日，北京協和醫院神經外科博士後、住院醫師金山木（Jin Shanmu）將一篇名為〈The Numerical Range Is a 2-Spectral Set〉的預印本掛上預印本平台，宣稱已證明法國數學家 Michel Crouzeix 在 2004 年提出的著名猜想。3 天後（7 月 30 日），康奈爾大學數學家 Alex Townsend 像過去一年那樣向 GPT-5.6 詢問 Crouzeix 猜想是否可解，意外地得到了一個回應：「三天前剛有人掛出預印本，聲稱已解決。」作者正是金山木。

Townsend 與合作者華盛頓大學教授 Anne Greenbaum 旋即聯絡了金山木，並聯手邀請猜想提出者、法國數學家 Michel Crouzeix 本人親自逐行審閱手稿。8 月 11 日，三人聯名在 SIAM News 發表專文〈The Neurosurgery Resident Who Proved Crouzeix’s Conjecture〉，正式對外確認：證明正確無誤。

「震驚」是 Townsend 與 Greenbaum 兩位專家在審閱證明後用來形容自身感受的詞。22 年懸而未決的猜想，由一位幾乎沒有正式數學訓練的神經外科醫師在 16 小時內交給 AI 跑完——這個故事本身已經遠比論文更戲劇化。

這個猜想為什麼這麼難：Crouzeix 的 22 年困局

Crouzeix 猜想由法國數學家 Michel Crouzeix 在 2004 年提出，屬於數值線性代數（numerical linear algebra）與算子理論的核心問題。猜想核心可表述為一句話：

對任意矩陣與任意多項式函數，矩陣經函數作用後的範數，不超過該函數在矩陣數值域（numerical range）上最大值的兩倍。

數學界對它的追逐歷史堪稱「悲劇式」：

2004：Crouzeix 本人提出猜想，常數為 2（猜想上限）。
2007：Crouzeix 與合作者僅能證明常數在 11.08 時成立——離 2 還有 5 倍以上的距離。
2017：全球頂尖專家在美國數學研究所（AIM）專題研討會上苦戰一週，才將常數降至 2.414。
2017 之後 8 年：實質進展歸零。

整個領域陷入一種奇怪的僵局：所有人都相信常數 2 是對的，但沒有人能證明——就像看清了山頂的形狀，卻找不到一條路上去。

金山木是誰：從地質學到神經外科的跨界數學家

理解這次突破的另一條主線，是金山木本人的背景。

本科：北京大學地質學專業（2016 年透過自主招生加分入學，高考 622 分、北大錄取線 660 分）。
2019：參與南阿爾卑斯山地質考察。
2020：透過北京協和醫學院「4+4 試點班」轉入臨床醫學。
2024：成為神經外科博士後、住院醫師。

他闖入矩陣分析的契機相當偶然：在經顱超音波研究中，他需要解決「超音波如何穿透複雜人體顱骨結構」的數值模擬問題；為了建模，他自學了矩陣分析；又在自學過程中偶然接觸到了 Crouzeix 猜想。

他在接受 SIAM News 訪問時說得相當輕描淡寫：

「我接受的正式數學教育僅限於理工科本科的基礎課程；除此之外的數學知識，都是自學的。」

正是這種沒有學派包袱、敢於讓 AI 自主運行十幾個小時的研究風格，最終讓他做出了 22 年來所有人類專家做不到的事。

GPT-5.6 怎麼跑出來的：16 小時無人值守的解題流程

金山木沒有採用傳統的紙筆推導。他的工作流程相當工程化：

選定平台：在 ChatGPT Work 平台上呼叫 GPT-5.6-Sol 模型。
設計提示詞（prompt）：借鑑 OpenAI 之前攻克 Cycle Double Cover 猜想（懸宕 50 年的圖論難題）時的策略——
- 要求模型在「物理斷網」環境下進行純粹原創思考
- 啟動大量 subagent 沿不同路徑發散探索、防止過早收斂
- 對候選策略進行對抗性審計（adversarial audit）
- 明確指令「在獲得完整證明前不得放棄」
設定完成後離開：金山木把提示詞送進去後即離開，全程未做任何干預。
16 小時後回來：GPT-5.6-Sol 在自主運行中經歷了數萬次假設、推翻與重建，最終給出了完整證明。

Townsend 與 Greenbaum 在 SIAM News 裡把這種提示詞設計總結為：

「這不是請 AI 算數學，而是設計一個讓 AI 自主窮盡所有可能性的環境。」

值得一提的是，這份提示詞完全公開——就放在金山木的 GitHub 倉庫 crouzeix_conjecture_prompt.txt。任何人能夠重現這個實驗，這也是這份研究被學術界迅速接受的原因之一。

8 天後的獨立證明：兩個團隊殊途同歸

預印本掛出僅 8 天後（2026 年 8 月初），兩位歐洲數學家 Emiel Lorist 與 Felix Schwenninger 發布了一份完全獨立、僅 5 頁的證明。Lorist 與 Schwenninger 在 arXiv 公開承認：「在探索證明策略時，我們同樣使用了 ChatGPT 5.6。」

兩份證明的思路完全不同：

比較項	金山木（GPT-5.6-Sol）	Lorist 與 Schwenninger
預印時間	2026-07-27	2026-08-04（晚 8 天）
論文長度	完整 Annals of Mathematics 格式手稿	5 頁精簡證明
核心方法	巧妙採樣策略簡化出正性條件	雙層勢表示法 + 2-擴張擾動引理
是否使用 AI	是（GPT-5.6-Sol 16 小時）	是（ChatGPT 5.6 探索策略）
數學結構	統一處理非厄米特（non-Hermitian）算子	走經典解析路徑

兩份獨立證明在 8 天內相繼完成，互相印證了猜想的正確性——這在猜想證明的歷史上極為罕見。

🚨 為什麼這件事重要（編輯部觀點）

Siami 觀點：這不只是「AI 證了一道數學題」。這是「研究主體性的位移」——AI 從輔助工具升級為能獨立完成跨日科研任務的協作者。

把這件事放進 2026 年的 AI 與數學社群脈絡裡看，有四個訊號值得放大：

1. 數學界對「AI 作為共同作者」的接受度正在結構性鬆動

Lean 4 形式化在這次事件中扮演了關鍵角色：金山木不只給了論文與提示詞，還附上了完整的 Lean 4 形式化證明與公理審計報告。SIAM News 把這件事評為「異常透明的開放程度」。當 Lean 形式化成為可驗證的證書，「作者是誰」這個問題就從單純的人類署名，變成了「人類負責引導與審核，AI 負責搜索與展開」的協作契約。

2. GPT-5.6 在 2 個月內已連破兩個重大猜想

2026-07-10：GPT-5.6 Sol Ultra 用 64 個 subagent 在不到一小時內證明 Cycle Double Cover 猜想（懸宕 50 年的圖論難題）。OpenAI 已公開 prompt 與 Lean 形式化。
2026-07-27：GPT-5.6-Sol 在 16 小時內獨立證明 Crouzeix 猜想（22 年的矩陣分析難題）。

兩個月內兩個不同領域的歷史難題被同一系列模型解決，已不是統計巧合。Noam Brown 在 X 上把這個趨勢命名為「math Singularity」。

3. 「提示詞工程」正成為一種新的科研能力

金山木的核心競爭力不是數學直覺，而是設計提示詞環境的能力——他知道要禁止 AI 連網、要讓 subagent 並行、要對抗性審計、要禁放棄。這套方法論移植到任何「AI 自主搜索 + 形式化驗證」的科研場景都有效。「寫提示詞」在 2026 年下半年正在變成一種可發表的科研技能。

4. AI for Math 的論文署名困境即將引爆

當兩個獨立團隊都在 8 天內用同一個模型得到正確結果，誰是第一作者？當 Lean 形式化是 AI 跑出來的，版權屬於誰？當 Townsed/Greenbaum/Crouzeix 三人親自審稿確認「正確」但 Lean 證明是 AI 寫的，同行評審該由誰做？這些問題在 2026-2027 年必然會在 SIAM、Annals of Mathematics、JAMS 等頂級期刊引爆。

數據解讀 / 質疑

這次突破有幾個地方值得讀者保留警覺：

「GPT-5.6 自足證明」其實高度依賴提示詞工程。金山木的提示詞明確禁止 AI 連網、明確要求不放棄，這相當於給 AI 製造了一個沒有干擾的純數學環境。離開這個環境，GPT-5.6 的數學表現會明顯下降（見 OpenAI 自己的 Preparedness Framework 評測）。換句話說，這次突破是「模型 × 環境設計」的合奏，不是模型單獨的能力。
Lean 形式化不等於完整驗證。Lean 4 證明的「正確」是相對於它採用的公理集的——如果某個公理本身有瑕疵，形式化無法察覺。SIAM News 的審稿者們審的是論文思路，不是 Lean 程式碼。
22 年猜想之所以艱難，部分原因是缺乏對的切入角度。Crouzeix 本人在 2007、2017 都把常數往下壓，但始終找不到最終證明。這暗示真正缺的不是算力，而是「換個框架」——這正是 LLM 在大量文獻中找隱藏結構的強項。
Townsend 自己承認，過去一年他每週都會向 GPT-5.6 問一次，模型每次都會在某個關鍵 lemma 卡住。換言之，AI 並非一直能解決——它需要正確的提示詞環境 + 正確的數學知識邊界 + 足夠長的計算時間，三者缺一不可。
對 Lean 形式化的未來影響：本次證明使用的 Lean 程式碼約 1,200 行，與 Math Inc. 用 Gauss 模型在 PNT（強素數定理）上跑出的 25,000 行相比規模不大，但驗證流程是完整的。這顯示「AI + Lean」的協作模式已經能覆蓋研究級數學的門檻。

業界反應：X 平台與數學社群怎麼看

Twitter / X 上這則新聞引發的迴響集中在四類觀點：

驚嘆派（@Dr_Singularity 等）：

「math Singularity: 一個幾乎沒有正式高階數學訓練的神經外科住院醫師，靠著 16 小時 GPT-5.6 Sol 自主運行，解決了 Crouzeix 猜想這個懸宕 20+ 年的算子理論與矩陣分析重大難題。」 — 8 月 13 日, 18.2K views

OpenAI 內部背書（@polynoamial, Noam Brown）：

「GPT-5.6 Sol Ultra 昨天剛公開，今天我們就分享它用 64 個 subagent 在不到一小時內證明了 Cycle Double Cover 猜想。期待看到科學家與研究者用這個模型做出什麼。」 — 7 月 10 日, 1M views

哲學派（@SebastienBubeck, Microsoft Research）：

「如果 Erdős 還在世，能用到 GPT-5.6 Sol，他會怎麼用？」 — 7 月 25 日, 59K views

冷靜派（@casinokrisa / Mikhail Drozdov）：

「如果專家確認無誤，這個 16 小時的運行將會改變人們對數學發現的想像。」

在 Hacker News 與 Reddit 的 r/MachineLearning、r/singularity 上，多數留言關注的是「該不該讓 AI 投稿頂級期刊」、「論文寫 AI 還是人類」、「如何評估 AI 證明中的原創性」這些尚未有共識的程序問題。