AI數學證明，需要區分結果核驗與過程重現

2026年11月6日，PSI報告稱，藉助未公開的Anthropic模型獲得了Aaronson–Ambainis猜想的證明。值得討論的不只是AI能否完成數學工作，而是這項聲明中，哪些部分能夠由外部人員實際檢驗。

研究結果與產生結果的過程，需要不同證據

公開倉庫提供Lean形式化證明及核驗紀錄，同時將命題是否對應原猜想留給人工審查。Open Market Notes沒有重新執行證明，也沒有重現發現過程。

我們的判斷是，兩種看似相反的態度可以同時成立。研究者可以認為公開、可檢查的數學成果很有價值，同時暫不判斷生成它的系統具備怎樣的普遍能力。反過來，無法使用同一模型，並不能直接否定一份證明。將兩者混在一起，容易把可以逐項檢驗的研究對象，變成對一家公司的整體表態。

設想一位評估者只收到最終證明檔案，沒有失敗嘗試的紀錄。他或許可以判斷，這份檔案是否證明了指定命題，卻不能由此推算模型解決新問題的機率、人工篩選的程度，或者此前失敗搜尋的成本。這些問題需要不同的觀察材料。一次成功成果，並沒有提供計算成功率所需的分母。

量子計算的含義有明確範圍

原始論文將這一猜想與查詢模型中對大多數輸入的經典模擬聯繫起來。它不是對量子機器進行的效能測試。

對商業讀者而言，這一區分會改變接下來的問題。抽象演算法需要存取輸入多少次，不等於交付日期、用電成本或應用執行時間。要做實際比較，必須指定工作負載、實作方法及資源核算方式。本文沒有提供這些證據，因此不能據此支持硬體採購決定，更不能推斷現有安全系統何時失效。

合理態度既不是因為理論沒有立即變成產品而忽視它，也不是把理論結論直接描述成工程成果。理論可以改變哪些問題值得研究，但工程仍需檢驗相關假設是否適用於目標應用。對一類問題的限制，不應在傳播中悄然變成對量子計算全部用途的判斷。範圍越清楚，研究的真正價值反而越容易被理解。

核驗應是一套工作流程，而不是標籤

Lean文件區分經典推理與計算內容。因此，一項形式化結果不應自動被描述為可直接執行的方法。

我們建議，編輯與研究團隊分別記錄準確命題、審查版本、實際執行的檢查，以及檢查範圍以外的結論。這是評估建議，不代表本刊已經稽核PSI的工作。版本身分很重要：對一個檔案的審查，不應成為對以後所有修改的認可。紀錄也應註明審查者，並區分發布方日誌與外部人員獨立重複執行的結果。

這種做法同樣有助於處理分歧。如果爭論針對定義，應討論形式化對象是否對應原來要研究的對象；如果針對推導，應指出哪一步存在問題；如果針對AI能力，則應檢查任務選擇、人工介入及可重複性。把分歧保留在正確層次，才能在一處需要修正時，不武斷地宣布所有其他結論都隨之失效。

對於考慮採購AI研究工具的機構，問題也不應停留在最令人印象深刻的展示。試用前可以先確定真正關心的問題，記錄全部嘗試，核算專家投入，並事先規定輸出如何檢驗。這是一種評估設計，並非對PSI表現的估計。無論工具最終成功還是失敗，它都能使後續比較更有解釋力，而不是只留下容易傳播的成功案例。

公開成果的重要性，在於允許人們提出具體、可定位的審查問題。下一項有用進展，應當是獨立檢查究竟確立了什麼，而不是標題再增加一個強調突破的形容詞。在此之前，數學有效性、發現過程的可重複性與實際影響，仍應作為三個不同判斷。