GPT-5.6 一小時證完 50 年數學難題，功勞卻對不上帳

一份 AI 在一小時內交出的數學證明，最關鍵的一步，是 1983 年三個人做的——而論文從頭到尾一個字都沒提他們。

指出這件事的不是酸民，是曼徹斯特大學的數學家 Thomas Bloom。這週 OpenAI 發論文，宣稱 GPT-5.6 的 Sol Ultra 模式產出了 Cycle Double Cover 猜想的證明；這道題從 1970 年代擺到現在，擱了大約 50 年。Bloom 是目前給出最詳細公開評估的人，他認真讀了，也認真挑了：證明骨子裡的想法，來自 1983 年 Bermond、Jackson、Jaeger 的一篇論文，OpenAI 的稿子完全沒引。

同一週還有第二件。OpenAI 研究員 Sébastien Bubeck 拿一個他用了兩年的凸優化問題餵 GPT-5.6，模型補上了一個大約 30 年沒人補上的下界缺口。兩件擺在一起，露出同一條縫：成果是真的交出來了，但「這到底是誰的功勞、驗證了沒有」——都還沒結清。

64 個 subagent、不到一小時，OpenAI 到底交出了什麼

先把事實擺清楚。OpenAI 的說法是：Sol Ultra 開了 64 個 subagent 平行跑，模型被要求至少算 8 小時，結果不到一小時就吐出一份完整證明。這個數字組合本身就是賣點——一道 50 年的難題，一個下午都不用。

但有兩件事要一起記住。第一，這份證明還沒經過同儕審查，數學社群的完整驗證還在進行，所以現在能講的是「OpenAI 宣稱」，不是「已經定案」。第二，各家報導連運算時長都對不齊，有人寫 148 分鐘、有人寫 168 分鐘。當一個「幾分鐘解出」的故事連分鐘數都晃動，你就知道該把重點放在別的地方。

證明裡最關鍵的一步，是 1983 年三個人做的

真正的重點是 Bloom 挑出來的那一刀。他的評估不是「AI 亂寫」——他認為這是認真的成果；問題出在出處。核心的證明策略追得回 1983 年那篇 Bermond、Jackson、Jaeger，但只讀 OpenAI 這份論文的人，會以為這套策略是 AI 自己想出來的。

Bloom 的原話是：「這是 AI 生成證明與論文的常見問題——它們沿用文獻裡的想法與證明策略，卻不做適當引用。」

這句話比「AI 到底會不會證數學」有用得多。因為它點的不是能力，是歸屬。一個把文獻讀進去、再把裡面的策略重新組裝出來的系統，很容易讓人把「重組」誤讀成「原創」。對讀論文、審論文、或拿 AI 幫忙寫技術文件的人來說，這正是最容易踩的坑：模型給你一段漂亮的推理，你不會自動知道那想法是它的、還是它從某篇 2003 年的論文裡搬來沒告訴你。

另一件更誠實：它標了「一年又幾分鐘」

Bubeck 那件凸優化，反而把時間帳算得比較清楚。他這個問題養了兩年，專門拿來測歷代模型；GPT-5.6 這回不只補上約 30 年的下界缺口（結果涉及 Ω(d²) 級的函式評估下界），還順手產出了 Lean 形式化——也就是把證明寫成機器能逐步檢查的形式，這一步讓驗證不只靠人點頭。

Hacker News 首頁那串討論，戳的就是「幾小時」這個數字。有人算了一筆更誠實的帳：模型跑出結果或許只花幾小時，但那幾小時的前面，是研究者一年多的鋪路——最後餵進去的，是一份約 10 頁、塞滿他過往工作和對話脈絡的提示。用一位網友的話說，那不是「148 分鐘」，是「一年又 148 分鐘」。反過來也有人替模型說話：Lean 形式化是它自己生的，它也探索了提示沒寫到的路。

兩邊其實都對，而這正是重點——這不是「AI 獨立解題」，是「人類把問題鋪到門口，模型踹進最後一腳」。承認這件事，不會讓成果變小；假裝不是，才會讓下一個人高估自己手上的模型。

所以你該把這件事放在哪

把兩件擺回你的桌上，用推理模型解硬問題時，能帶走的其實很具體：

1. 先鋪路，別等奇蹟：推理模型加多個 subagent 並行、再加上形式化驗證，現在真的能攻進以前只有專家能碰的硬問題——但成立有前提。你丟一句話進去不會有奇蹟，Bubeck 花的是兩年加一份 10 頁提示。
2. 能形式化就形式化：讓機器逐步檢查，別把驗證外包給氣勢。不能形式化的，就當它是「待審的草稿」而不是「定案的證明」——連 50 年難題的證明都還躺在同儕審查前面。
3. 盯它的出處：模型很會把文獻裡的策略講得像自己剛想到的，該引的前人它不會主動提。Bloom 替所有人先示範了這一刀怎麼下。

還沒有答案的那題，就留給接下來幾週的同儕審查：Sol Ultra 那份證明到底站不站得住。在那之前，它是一則很好的示範——示範的不是 AI 變成了數學家，是我們讀 AI 成果時，得自己補上那份被省略的引用清單。