Aaronson–Ambainis 猜想：PSI 的 AI 證明，Lean 究竟驗了什麼？（2026）

2026 年 11 月 6 日，Physical Superintelligence（PSI）在官網發布〈A proof of the Aaronson–Ambainis conjecture〉，宣布其 AI 研究系統找到了 Aaronson–Ambainis 猜想的證明。這則消息值得注意的地方，是它交出了論文、Lean 形式化與檢查紀錄；讀者因此能追問：究竟證明了哪個命題，又是誰檢查了什麼？

以下先讀清楚公告的主張，再對照原始猜想與公開證明材料，最後判斷這件事對量子計算和 AI 研究各意味著什麼。最需要分開的三件事是：數學結果是否成立、機器實際檢查了哪些內容，以及發現過程能否歸因於某個模型。

一、PSI 的宣告：從答案敘述，走向可檢查的證明

The Aaronson-Ambainis conjecture is now a theorem.

中文：Aaronson–Ambainis 猜想現在已是一個定理。

PSI，〈A proof of the Aaronson–Ambainis conjecture〉

這是 PSI 對結果的明確宣告。它同時表示，內部開發的研究系統使用了非公開的 Anthropic 模型，並在一次執行的第三天取得完整證明，之後又改善結果。這些關於模型與發現速度的敘述，應保留「PSI 表示」的主詞；公開證明成立，也不能單靠它反推當時的完整研究過程。

Instances of a non-public Anthropic model were used in the run.

中文：這次執行使用了某個非公開 Anthropic 模型的多個實例。

PSI，〈A proof of the Aaronson–Ambainis conjecture〉

論文第 2 頁與附錄 A進一步交代分工：David Turturean 選定問題、開發研究執行層並啟動系統，模型實例搜尋、提出與組合想法；作者再審閱編輯論文並承擔正確性責任。這讓「AI 做研究」有了較具體的工作描述，仍不宜改寫成一個聊天模型無人介入、三天就能普遍解決任何難題。

同一份附錄記載，最初證明對應的指數為 22，後續改善到 11，再到 7。這裡的 7 是數學下界中的冪次，並非快了七倍。發現後還能改進中間結果，才是這份自述比較有意思的部分：系統交出的不只是單一結論，而是一組可繼續推進的數學工具。

二、Aaronson–Ambainis 猜想問的是什麼？

要讀懂新聞，先把「快」的單位換成讀取輸入的次數。Aaronson 與 Ambainis 的原始論文〈The Need for Structure in Quantum Speedups〉，研究的是黑箱查詢模型：一般演算法每次查一個輸入位元，量子查詢則能對輸入位置作疊加存取。這種模型把取得資訊的成本抽出來分析。

它關心的核心問題是：量子演算法查了 T 次後，傳統演算法能否只多查一個 T 的固定次方，就在大多數輸入上，近似它接受、也就是回答「是」的機率？「大多數」有分布條件；這裡以所有位元字串上的均勻分布計算。誤差容許值與例外比例，也都要一起指定。

低次多項式把這個量子問題接到純數學。量子演算法做 T 次查詢後，接受機率能寫成次數至多 2T、取值在 0 到 1 的多項式。猜想要求：只要這個值仍有明顯變動，至少有一個位元的影響力不會小得太誇張。影響力的定義，是把該位元翻轉後，數值差的平方，再對所有輸入取平均。

想像你面前有許多開關，一個儀表顯示某個數值。你想用少數幾次查看，估計儀表最後會指向哪裡。若仍有某個開關對讀數影響較大，先查它就有用；當剩下的開關已不太改變讀數，再用剩餘情況的平均值作估計。猜想提供的是這種逐步選擇的數學保證，而非實際量子硬體的測速報告。

PSI 的公開命題檔將原始形式寫成：若多項式在所有 0／1 輸入上介於 0 與 1，次數至多 d，且變異數至少為 ε＞0，就存在一個位元，其影響力至少為 （ε／d）⁷。新論文另給出帶明確常數、與變異數的 5／2 次方及 d 的 6 次方有關的較強下界。數學價值在於依賴是固定次方，且不因輸入位元數增加而直接消失。

三、Aaronson–Ambainis 猜想的影響：查詢次數與實際時間

原始論文已建立「影響力猜想 → 大多數輸入上的經典查詢模擬」這條推論。若 PSI 的證明經檢查成立，就補上了其中的重要前提。較早的獨立研究也能對照：Guy Blanc、Jordan Docter、Carmen Strassle 與 Li-Yang Tan 於 2026 年 8 月 19 日提交的〈Quantum Speedups Require Structure or Depth〉，已處理固定平行輪數的情況；那項結果有輪數條件，不能當作對 PSI 完整證明的外部驗收。

這裡有兩條容易被標題抹掉的界線。第一，平均情況的模擬允許少量例外，特定結構的問題仍可能落在不同範圍。第二，查詢模型主要計算讀取次數；決定下一個位置、計算預測值所花的內部運算，也會影響真正的時間。查詢次數是多項式，還要看冪次、常數與實作，才能討論工程上的可用性。

因此，這份研究應拿來修正「量子加速在哪些條件下可能出現」的理解。若要評估一個真實量子應用，仍需列出輸入承諾、任務類型、誤差、資料取得方式與完整運算成本。只拿這項查詢結果去估算某個產品的速度或市場價值，會把定理之外的工作偷偷省略。

四、Lean 通過了什麼？把命題、證明與執行分開看

Lean 官方的處理流程說明指出，使用者的證明經 elaboration 轉成核心型別理論中的項，再由 kernel 檢查。這使驗收能從「文字看起來合理」深入到形式規則。關鍵是先問：被送進去的命題，是否正是讀者以為的那個命題？

PSI 的公理稽核文件把界線寫得很清楚：機器檢查針對 Conjecture.lean 的命題；形式化定義與原始猜想是否相符，要逐項對照。論文是另一份文字，論文和 Lean 的對應表是閱讀指南，不是機器替整篇自然語言論文出具的保證。

文件列出的主要定理依賴 propext、Classical.choice、Quot.sound 這三項 Lean 核心公理。這比籠統地說「完全沒有公理」精確得多。它另列一個帶前提的強化版本：更好的常數依賴 FbsDegreeBound。這個外加前提屬於該強化版本，不能混進主定理，也不應反過來說主結果因此是未證明的假設。

驗證紀錄還區分一般建置、從空環境重播、不同型別檢查器與 Comparator 的沙盒流程。其末尾明說，列出的執行由作者工具、租用機器或該程式庫的工作流程完成，尚未由另一方重跑。這是作者對所列紀錄的描述；本文也未執行 Lean 建置，因此不把這些通過結果寫成 AlphaLab 的重現。

特別要小心「獨立」二字：兩套獨立實作的檢查器，能減少共同的型別檢查錯誤；由獨立團隊在乾淨環境重新取得檔案並執行，則增加對執行與材料的信任。兩種獨立性解決不同問題，不能相互替代。

五、這份證明的新意，也有一條人類研究的來路

Lovett 與 Zhang 的〈Fractional Certificates for Bounded Functions〉在 2023 年已研究 fractional certificates，並說明若一個延伸的不等式成立，便能推進 Aaronson–Ambainis 猜想。把它想成：替不同輸入上的開關安排權重，用這些權重控制翻動一組開關可能造成的改變。

依 PSI 論文的證明概覽，新工作沿用層級集合與分數證書的路線，但以新的不等式補上關鍵位置。它先利用行列式建立帶限制的配對，再把配對不等式推到所有點對；接著跨層級積分，最後對部分座標取平均，連到所需的影響力下界。這是作者提出的證明機制概要，並非本文對全部推導完成了數學審稿。

這條來路讓「AI 原創」有了更有用的衡量方式：提出的新連接是否有效、是否補上已知路線的缺口、別人能否理解並重用。引用既有工具與產生新步驟可以同時成立。把所有成果都說成從零出現，反而會遮掉最值得學習的那一段。

六、AlphaLab 的判讀：成果的可信度與模型的神話，分開結帳

我同意：能交出可查的證明，比只交一張成績圖更有份量

數學研究有一個很好的驗收特性：提出方法的人可以很複雜，最後交付的命題與推導仍能被拆開檢查。PSI 把材料公開，讓下一個人有機會從「相信發表者」走向「檢查他交出的東西」。即使發現過程使用閉源模型，公開產物仍可有自身的研究價值。

我存疑：一項成果，能否直接證明整個研究流程的可靠度

單一成功案例回答的是存在性：這套流程至少交出了這份候選成果。要估計普遍的研究能力，還要知道嘗試了哪些問題、花了多少總資源、失敗如何計入，以及人在哪些地方介入。第三天是這次執行的時間敘述，並不是完成同類問題的平均成本。封閉模型也不能由讀者任意換成另一個公開產品名稱，再套上同樣能力。

可讀性會決定成果有多容易被繼續使用

形式化的價值是把邏輯要求變得明確；人類可讀的論證，則有助於找到關鍵想法並把它搬到下一題。PSI 公告轉述那組 Stanford 研究者已閱讀、回饋，並正在撰寫較短的專家說明。這段應視為 PSI 對交流狀態的報告，不能升格成本文已獨立核實的完整外部驗收。值得等待的是可公開對讀的解說與可追溯的重跑結果。

七、接下來看三份交付：定義、重跑、研究帳本

一般讀者可以先做一個很小的練習：在任何「AI 證明了猜想」的標題旁，寫三行問題——形式化的命題是什麼？哪個版本的檔案由誰重跑？發現過程哪些部分有可查看的紀錄？回答能對上，信心就有依據；回答仍停在轉述，就把信心停在轉述的範圍。

研究者可優先比對 PrintedConjecture 的定義與原始猜想，再選固定版本，依公開驗證文件規劃乾淨環境的重跑。要理解模型與研究執行層的分工，可以接著讀 Agent Harness 入門；要判斷一項測量到底保證哪一層，FlashProve 的證明界線提供另一個對照。評估整套研究流程時，則用 AI Evals 的方式先寫出合格條件與失敗分母。

Aaronson–Ambainis 猜想這則消息最有價值的變化，是研究宣告開始附上一份可被追問的交付物。支持它，不必先相信模型的所有能力；審慎看待它，也不必抹去公開證明的價值。下一份最有說服力的進展，是有人把同一命題、同一版本與一次可追溯的檢查結果，清楚接在一起。