2026 年 10 月 2 日，APPI News 刊出一篇以 Lean 4 與 Mathlib 為框架的操作指南，討論「拿到 AI 產生的數學證明後怎麼驗」。這篇文章的價值不在教學本身，而在它把一個常被略過的問題攤開：當模型宣稱「證明完成」，驗證這一步的成本由誰吸收、透過什麼機制吸收。這與我們先前分析的AI 解題能力的時間差是同一條故事的下半場，模型能力先到位，驗收流程的建置成本隨後才浮現。
三層「通過」，三種不同的信任等級
來源文章先把「AI 說它證明了」拆成三層，這個分層本身就是成本結構的起點。
第一層是自然語言答案，模型用文字寫出推理，驗證工作完全落在人身上，逐段檢查定義、計算與推論。Google DeepMind 在 AlphaProof 的說明中直陳，自然語言方法可能產生看似合理、實際錯誤的中間步驟，這正是 AlphaProof 轉向 Lean 形式化流程的理由。
第二層是形式化命題，題目被翻成 Lean 能讀的 statement，型別、變數範圍、假設與結論都必須明確寫出。Lean 官方文件要求每個推理步驟回溯到定義、定理、規則或公理。
第三層才是 kernel 接受的證明。Lean kernel 接受 proof term，代表目前檔案與匯入內容足以推出該形式化命題；編輯器的藍色雙勾被官方定義在這個層次。但官方的 Proof Validation 文件同時提醒，kernel 勾勾不能替代「statement 是否對應原本想證明的意思」這項獨立檢查。
換句話說，最貴的驗證環節不在 kernel，在命題翻譯。形式化過程漏掉一條假設、縮小一個變數範圍，都可能讓「通過的證明」證明的是另一道題。
流程四步與可重跑性
來源文章引用 AlphaProof 的公開流程，將驗證路徑拆為四步：先把自然語言題目轉成 Lean 的形式化敘述，再由模型搜尋證明步驟，交給 Lean 驗證，已驗證的證明還能回到訓練迴路。可對照的量化基準是 DeepMind 公布的成績：AlphaProof 與 AlphaGeometry 2 在 2024 年國際數學奧林匹亞合計解出六題中的四題，得 28 分。
在工具鏈一側，Lean 官方語言參考指出 tactic 的錯誤不會繞過 kernel，因為 tactic 的產物仍要交給 kernel 檢查；安裝手冊則要求程式放在 Lake 管理的專案中，Mathlib 提供 lake build、lake test 與預編譯快取。對 AI 產物而言，用 Lake 重建整個專案的價值，是把版本、相依函式庫與建置結果一起固化，壓縮「在某臺電腦曾經通過」的模糊空間。
這套流程的隱含帳目很清楚：模型把「找證明」的成本壓下來了，但「確認題目被忠實翻譯」與「重跑建置」這兩段工時沒有消失，只是從模型端移回了使用者端。這個結構與醫療 AI 覆核成本掛在誰的報表上的邏輯同構，自動化產出越多，人工覆核的絕對量隨之上升，而非下降。
誰受惠、誰承壓
受惠端是形式化工具鏈的生態系。Lean 4、Mathlib 與 Lake 的使用門檻構成一段學習曲線，當 AI 證明供給增加，能操作這條驗證流程的人員與教學內容需求同步上升；來源文章本身就是這類內容供給的一部分。
承壓端是直接消費 AI 數學答案的使用者與機構。若驗收條件只停在自然語言層，錯誤中間步驟的風險由使用者吸收；若要拉到 kernel 層，就必須付出形式化命題審查與專案重建的固定成本。來源文章給出的檢查方向包括確認命題與原題相同、留意 sorryAx 與公理依賴等，這些都是可執行的程序項目，但每一項對應的都是實際工時。
收束判斷
來源文章的核心主張可以濃縮成一句操作原則：第一個問題不該是「這個模型數學能力多強」，而是「它交出的檔案能不能在指定環境重建，題目翻譯有沒有漏掉前提」。這個原則對應的市場含義是，AI 數學能力的排行榜不會替使用者完成任務驗證，驗證成本始終留在採用方這一側。隨著形式化證明供給增加，能夠把驗證流程標準化、把審查工時壓下來的工具與服務，才是在這條賽道上真正被定價的標的。