Aaronson-Ambainis 猜想：AI 用三天證明了一道 18 年未解的量子難題

11 月 6 日，一家名叫 Physical Superintelligence（PSI）的小公司宣布了一件十年前聽起來像是科幻小說的事：一個 AI 研究系統——運行著一個未公開的 Anthropic 模型——證明了 Aaronson-Ambainis 猜想。這是量子複雜性理論的核心開放問題，自 2008 年以來一直懸而未決。系統在運行的第三天就得到了完整證明。Lean——逐一用機器檢驗每一步邏輯的證明助手——接受了它。PSI 隨後讓系統繼續攻關相關問題，兩次改進了結果，並發表了論文和公開的 Lean 形式化證明，任何人都可以重新檢驗這項工作。

要理解它為何重要，先從量子計算機真正擅長什麼說起。1994 年，Peter Shor 找到了一種量子演算法，能以遠快於任何已知經典方法的速度分解大數。但 Shor 的加速依賴於一種罕見的天賦：問題本身隱藏著重複模式，而量子計算機能找出它重複的頻率。已知的大多數驚人的量子加速都是這樣運作的：它們利用結構。

Scott Aaronson 和 Andris Ambainis 提出了一個令人不安的問題：那隨機輸入呢？隨機輸入幾乎從不具備這種結構。量子計算機能否以比普通計算機少得多的讀取次數，回答關於一個隨機字串的是非問題？他們提出了一個關於多項式的猜想——純數學——並證明，如果它成立，答案是否定的：在隨機輸入上，量子計算機至多快上一個多項式倍。這個猜想成了量子複雜性理論的核心開放問題之一；2026 年 8 月，一個史丹福小組證明了它的一個特例：以固定輪數並行讀取輸入的量子演算法。

PSI 的證明遵循 Shachar Lovett 和 Jiapeng Zhang 提出的方案，把他們方案中留作猜想的一個不等式，替換為論文中證明的一個新不等式，用的是基於 David Reimer 的蝴蝶引理（Butterfly Lemma）的配對論證，以及其他幾個小組的結果。參與其中的人類——PSI 的 David Turturean——搭建了這個研究系統、界定了問題、運行了它，並對論文的正確性負責。顧問 Jim Halverson 審核了證明。證明了特例的史丹福小組一直在閱讀完整證明，提出了意見，正在為專家寫一篇更簡短的闡述。他們目前的評價是：「這是一個巨大的成果。」

這才是閱讀這則新聞的正確方式——不是把它當作加冕，而是一項附帶可檢驗成果的宣稱。Lean 的接受是一個很高的門檻：一台機器已經驗證了論證的每一步。Lean 無法檢驗的是，形式化後的命題是否就是數學家真正關心的那個命題，或者形式化過程是否偷偷帶入了一個隱藏假設。這是人類專家的工作，而且尚未完成。同行評審還沒有發生。找到這個證明的模型並不公開，所以沒有人能重新運行發現過程本身——只能檢查它產出的東西。

而這則公告所處的這一週，才是真正的故事。PSI 的證明不是孤立事件。10 月，OpenAI 發布了 722 篇 AI 撰寫的數學手稿，其中包括對擬黎曼猜想、唯一博弈猜想和一類特殊形狀的霍奇猜想的所謂證明。9 月，《數學季刊》上的一篇論文報告，一個 AI 系統找到了關鍵思路，把關於 k-微分的有條件結果變成了無條件定理，關鍵引理在 Lean 中得到了形式化證明。Axiom 則把約 7500 頁的 Stacks Project——約 1600 萬行——形式化了，使一大批代數幾何成果變得機器可檢驗。模式已經再清楚不過：AI 提出證明，Lean 負責裁決。瓶頸已經從發現證明轉移到了驗證證明，而驗證環節仍然由人類決定節奏。

我關注的正是這種轉移。如果史丹福的闡述順利落地、沒有其他小組發現漏洞，Aaronson-Ambainis 證明將成為一個月內第二項經受住專家審查的 AI 宣稱成果——問題將不再是 AI 能否做前沿數學，而是驗證流程能跟上多快。我的預測是：到 2027 年 12 月 31 日，這項證明將獲得獨立數學家的公開確認——通過史丹福小組的闡述、同行評審期刊的發表，或等效的公開專家確認——且證明中未發現實質性漏洞。我給出的機率是 65%：機器層面的門檻已經跨過，合適的專家已經介入，但人類的確認不是走過場，一個定義的偏差仍可能讓一個通過 Lean 檢驗的證明翻車。