「通過」先被定義好了：OpenAI 的 Lean 證明，是一套被排好位的驗證介面

2026 年 10 月 7 日，APPI News 刊出一篇長文，討論 OpenAI 公開模型產生的數學手稿與部分形式化證明後，讀者該如何理解 Lean 的檢查結果。文章作者的切入點很實際：Lean 通過，究竟驗證了什麼。

這個問題聽起來像數學，實際上更像介面設計。Lean 的核心檢查器只確認一件事：形式化證明符合程式中寫定的命題與環境設定。它不會判斷這段程式是否完整表達了手稿原意，也不會評估結果重不重要。換句話說，檢查器回報的「通過」，是一個被嚴格限定範圍的訊號。介面把它顯示成一個綠燈，但綠燈的管轄範圍，遠比使用者直覺以為的窄。

文章指出一個關鍵的人工判讀環節：形式化版本可能只涵蓋手稿中的核心引理，也可能在更強的前提下證明一個更窄的命題。假設若比手稿原文更強，形式證明可以完全正確，卻沒有證明讀者以為的那件事。這裡的設計問題在於，檢查結果的呈現方式，並不會自動揭露這條翻譯鏈上的落差。命題範圍、量詞定義、前提強度，這些資訊都存在，但存在於 theorem statement 的文字裡，需要人逐句對照才看得到。

Lean 官方文件其實把這條邊界寫得相當坦白：證明檢查只有在「可信的定理敘述正確」時才有意義。來源引用了參考手冊〈Validating a Lean Proof〉的說法。這是一種誠實的介面設計，系統明確宣告自己不負責的部分：機器檢查推導，人來確認命題翻譯與數學脈絡。問題是，這條免責線寫在文件裡，而不是寫在檢查結果的畫面上。

目錄怎麼計數，決定了讀者怎麼誤讀

文章第二段處理的是另一層資訊設計問題：大量公開的研究成果，篇數本身沒有意義。OpenAI 的資料目錄把「手稿」、「結果家族」（family）與「形式化材料」分成不同的統計對象。一個 family 可能包含主要結果、相關論證、推論或替代證明，且各自的驗證狀態不一。

這幾種項目不能相加，也不能當成同一個「已驗證定理」的數量。官方 repository 也明確說明：並非每份手稿都有 Lean 形式化，未形式化的結果仍可能有問題。

「模型產生」、「研究者檢查過」、「有可建置的形式化證明」、「獨立研究者確認數學內容」，這四種狀態在目錄裡是不同的層次，不能互換。但當媒體報導把整批材料壓縮成一個數字時，這些層次就被抹平了。這與我們先前觀察過的七大難題進展被排成搜尋結果頁的驚嘆號是同一種機制：資訊在傳播鏈上每經過一層轉述，驗證狀態的粒度就粗一級。

目錄設計本身倒是提供了逐篇追查的路徑：論文、來源檔、個別建置說明、Lean library 與形式化目錄都在 repository 裡。來源文章提醒，檢視時應記下當下的版本或提交紀錄，因為目錄會持續更新。依賴版本與提交紀錄，是形式化驗證世界裡的時間戳記，少了它，今天的「通過」和下個月的「通過」就無法區分。

驗證的制度化，是被設計出來的

把視野拉遠一點，這類「把驗證流程寫進規則」的做法，近年越來越常見。克雷數學研究所的千禧年大獎曾把期刊發表與兩年等待期寫進規則，成為一套驗證真理的制度介面，我們在克雷研究所大獎規則的介面觀察中討論過。Lean 的檢查機制與之相比，多了一層機器參與：錯誤從「相信某段長篇推理」，轉成「檢查形式證明及其明確依賴」。

但來源文章的結論值得留在心上：即使所有形式化步驟都合規，定理也可能只因為前提設得過強而容易成立。檢查器不會替人選題，不會判定前提是否符合原問題，也不會告訴你這個結果是否新穎。

所以「Lean 通過代表證明成立嗎」這個問題的答案，取決於你對「成立」的定義。推導層次的成立，機器已經給了確認；命題翻譯、前提強度與研究意義，仍是人的工作。這條分工線本身就是一套設計，而一套好的驗證介面，應該把這條線畫在使用者看得到的地方，而不是只寫在參考手冊裡。