OpenAI 一次宣布三項數學與物理成果
OpenAI 在 10 月 26 日發表一篇公告，說它的模型在三個領域產出了成果：調和分析裡的局部平滑猜想與 Kakeya 猜想、複雜度理論裡的指數時間假說（Exponential Time Hypothesis，簡稱 ETH），以及量子場論裡四維 Yang–Mills 與 QCD 的存在性。最引人注意的是 ETH：OpenAI 說，它的系統證明了這個猜想是錯的。Hacker News 的討論串在我們整理資料時已有 967 points、509 則留言。
如果你是關注 AI 能力的工程師或技術主管，這幾天很可能會被同事或主管問到：「AI 真的推翻了一個數學猜想嗎？」這篇想回答的就是這件事：這三項宣稱現在各自站在什麼狀態，是已確認的定理，還是等人檢查的宣稱；以及接下來出現什麼，才算站穩。
先說結論。三項都是 OpenAI 的宣稱，狀態各不相同：依 OpenAI 的說法，局部平滑、ETH 與 Yang–Mills 的證明都完成了 Lean 形式化，也就是交給電腦逐步檢查過；ETH 的外部專家審查才剛開始，而審查者自己公開表示，他們的參與不代表認證；Yang–Mills 與 QCD 目前沒有公開 AI 產出的材料，外界無從檢查。
先交代我們做了什麼。我們讀了 OpenAI 公告全文，讀了 OpenAI 數學 repo 的 README，也確認了 ETH 預印本資料夾裡有哪些檔案；查了 The Next Web 轉引的審查小組說法；讀了 HN 討論串前 12 則頂層留言。我們沒有讀到論文內文，也沒有自己執行 Lean 檢查。 所以下面不談證明的技術內容，也不判斷證明是對是錯。
ETH 為什麼特別受關注
ETH 是一個關於「判斷一條布林公式能不能被滿足」到底有多難的長期猜想。依 OpenAI 公告的描述，已有數百篇論文把它當成前提，推導出「某些問題在這個條件下不可能算得更快」的結果。如果 ETH 不成立，這些建立在它之上的結論就少了依據。OpenAI 的說法是，這「重新打開」了這些任務究竟能快多少的問題。
不過 OpenAI 同時寫明，從反證走到找出更好的演算法，再變成實際的改進，還需要大量後續研究。換句話說，就算這項宣稱最後成立，也不代表你手上的求解器很快會跑得更快。
HN 上有人問，這會不會進一步推向 P=NP。我們讀到的留言裡沒有可靠的回答；OpenAI 公告和審查小組的公開信也都沒有這樣說。本文不做這個推論。
第一層：Lean 檢查保證的是什麼
Lean 是一種證明輔助工具。把數學命題和證明寫成程式後，由電腦逐步檢查每一步推導是否合法。這比人工讀一份長證明可靠得多，但它保證的是「這段形式化寫出來的命題被證明了」。至於這個命題是否確實等於原本的猜想，例如 Lean 裡寫下的定義是不是學界所說的 ETH，仍要靠熟悉這個領域的人逐項對照。
這是形式驗證的一般限制，不表示這次的形式化有問題。就本案來說，這一步我們沒有能力檢查，也還沒讀到外部專家對此的結論。
依 OpenAI 公告的時間線，三項成果的進度如下：
- Yang–Mills 與 QCD：自然語言證明分別在 9 月 9 日與 9 月 18 日取得；Yang–Mills 部分的 Lean 形式化在 10 月 16 日完成。公告沒有提到 QCD 部分的形式化。
- ETH：10 月 16 日找到自然語言的反證，10 月 17 日完成 Lean 形式化。
- 局部平滑猜想：AI 輸出在 10 月 18 日取得，10 月 19 日完成 Lean 形式化。OpenAI 說，這個結果涵蓋任意維度，因此也解決了 Kakeya 猜想與 Stein 限制猜想。
數學這部分，OpenAI 說自然語言證明與 Lean 證明都已放在 GitHub。我們看了 openai/math 的 README：稿件由一個沒有具名的內部模型產生，我們讀到時收錄了 721 篇稿件、分屬 373 個家族，約 42% 的頂層結果有 Lean 形式化。README 也直接寫了「部分沒有形式化的結果可能有問題」，並表示功勞、優先權與同期研究的認定，完全交給數學界決定。README 會持續更新，這些數字只代表我們讀到當下的內容。
OpenAI 在公告與 README 裡都說，這些稿件最好被看成「原始研究資料」（raw research data）。這個定位值得記住：連發布者自己都沒有把它們當成定論。
數學成果方面，我們沒有讀到任何外部數學家的公開評論。
第二層：ETH 交給原提出者審查，審查者先劃清界線
ETH 的審查小組由三位學者帶領：加州大學聖地牙哥分校的 Impagliazzo、Paturi，以及 MIT 的 Williams。Impagliazzo 和 Paturi 正是與 Zane 一起提出 ETH 的人。OpenAI 公告也提到，Williams 過去曾反駁過 ETH 的一個更強版本。小組向 OpenAI 提了兩個條件：公開全部原始資料，以及出資舉辦一場會議討論這件事的影響。OpenAI 說它同意了。
這三位學者的態度很清楚。依 The Next Web 轉引的公開信，他們寫道，他們的參與「不應被視為對這項宣稱的認證」，這種份量的結果需要仔細、獨立的檢驗。Williams 也在貼文中說，他沒有簽保密協議，也沒有收費，並把這件事稱為「宣稱的反駁」（claimed refutation）。公開信和貼文的原文我們沒有直接讀到，以上都來自 The Next Web 的轉引。
我們在 repo 裡確認，ETH 預印本的資料夾有 README、paper.pdf 和 build 三項內容。論文 PDF 我們下載了，但沒有讀到內文與摘要。
所以 ETH 目前的位置是：OpenAI 說 Lean 檢查通過，論文已放上 GitHub，也同意公開全部原始資料；最有資格判斷的人正在看，而且他們明說還沒有下結論。
第三層：Yang–Mills 與 QCD，外界目前看不到 AI 的產出
物理部分，OpenAI 稱它的模型為四維 Yang–Mills 與 QCD 的存在性產生了嚴格證明，方法建立在 Balaban 的既有工作上。OpenAI 也說，Yang–Mills 部分屬於克雷數學研究所千禧年大獎問題「量子 Yang–Mills 理論」裡的一個子問題。
這組的處理方式和前兩組不同。OpenAI 說，因為篇幅與複雜度，他們等到形式化完成才對外說明。負責的小組由 David Gross 領軍，成員包括 Douglas、Jaffe、Klebanov 和 Nekrasov。小組決定暫時不公開 AI 產出的材料，改由他們自己撰寫。
結果是，三項成果裡唯一連到千禧年大獎問題的這一項，目前反而最難由外界檢查：沒有公開的 AI 產出可供檢查。在小組的文章出來之前，它只能先被當成 OpenAI 的宣稱。
發布方式本身也是這次的重點
這次公告有不少篇幅不是講證明，而是講怎麼把成果交給學界。三組的釋出方式，都是由各自的外部專家建議的：
- 數學：只公開 AI 輸出，讓研究者自己整理。
- 電腦科學：組成審查小組，同時公開 AI 輸出。
- 物理：組成審查小組，由小組決定要不要公開。
OpenAI 說它不知道哪一種最有用，歡迎各方回饋。它把這些外部專家稱為 shepherd，並列了四項原則：透明（不簽保密協議，可以自由討論與發表）、不爭學術功勞、小組因理解與撰寫工作得到認可、獨立（無薪、自願，結論屬於他們自己，不代表 OpenAI）。OpenAI 也自承一個缺點：由誰擔任 shepherd，決定了誰能最先接觸成果，這會造成資訊不對稱。
另外，OpenAI 捐給 Simons Foundation 500 萬美元，用來辦工作坊、會議等活動，協助研究者理解並延伸這些 AI 產出的成果。
HN 前 12 則頂層留言的反應很分歧：有人認為公告標題把最重要的 ETH 埋在後面；有人覺得 500 萬美元太少；也有人認為這會成為新常態。這只是我們讀到的一小段討論，不代表整串留言的看法。
跟同事怎麼說：一則有機器檢查、正在審查的宣稱
回到開頭的問題：AI 真的推翻了一個數學猜想嗎？目前比較準確的說法是：OpenAI 宣稱它的模型做到了，部分結果依 OpenAI 的說法通過了 Lean 檢查，但還沒有獨立專家公開確認，我們也沒有讀到有人公開指出錯誤。
這兩個方向的簡化都不準。說「AI 已經證明 ETH 是錯的」，跳過了審查小組明說還沒認證的事實；說「又是行銷話術」，則忽略了 OpenAI 公開了數學部分的 Lean 證明與 ETH 論文、同意公開原始資料，還把 ETH 的審查交給它的原提出者。比較穩妥的做法，是把三項成果分開看：
- 局部平滑與 Kakeya：AI 輸出與 Lean 證明已公開，等數學界檢查形式化的命題是否與原猜想相符。
- ETH：論文已公開，原提出者正在審查，還沒有結論。
- Yang–Mills 與 QCD：AI 產出沒有公開，外界目前無從判斷。
接下來值得留意的有幾件事：ETH 審查小組的公開結論，以及 OpenAI 承諾出資的那場會議；Gross 小組自己撰寫的 Yang–Mills 與 QCD 文章何時發表；以及數學界對局部平滑證明的公開評論。這些出現之後，再回頭判斷哪些宣稱站穩了。
對工程師來說，這則新聞眼下不會改變手上的工具。OpenAI 自己也說，要把 ETH 的反證變成更好的演算法，還有很長的路。它比較能改變的，是你對「AI 能做到什麼」的參考點：如果審查結果支持這些宣稱，模型產出的證明就不只是練習題，而是有人得認真檢查的研究材料。在那之前，把它當成一份等待檢驗的研究資料，正是 OpenAI 和審查專家目前共同的說法。
