編譯打勾之後還有兩層：AI 的 Lean 4 證明，那筆驗證成本記在誰的工時裡

2026 年 10 月 6 日，APPI News 刊出一篇約 13 分鐘閱讀長度的技術文章，作者張饒輝（Lightman Chang）整理了檢驗 AI 產出 Lean 4 證明的三個步驟：lake build、#print axioms、lean4checker。文章的核心主張可以用一句話概括：編輯器上的核取記號，只代表型別檢查通過，不代表數學命題被正確形式化，也不代表證明沒有暗藏未完成的假設。

這個題目本站先前已從驗證帳的角度談過一次，見AI 定理證明的驗證帳，記在誰的工時裡。這篇新文章的增量在於把檢查流程拆成三層，並明確標出每一層能回答與不能回答的問題。以下按成本結構的角度重拆一次。

三層檢查，各自買到不同的把握

第一層是 lake build。Lean 官方文件把 lake 定義為追蹤依賴並呼叫 Lean 的建置工具；在專案根目錄執行建置且沒有錯誤，表示「這個版本的 Lean、這組匯入、這份 theorem」能通過核心檢查。官方驗證指南也把「lake build 後沒有錯誤或警告」列為與編輯器核取記號等級相同的日常檢查。這一層的成本最低，幾分鐘的機器時間，但它留下兩個明確的未答問題：定理敘述是否忠實對應原本的自然語言數學問題，以及證明是否透過 sorry 或自訂公理偷渡了假設。

第二層是 #print axioms theoremName。依 Lean 官方驗證文件，輸出若只含 propext、Classical.choice、Quot.sound 三個內建公理，屬於可接受的基線；出現 sorryAx 代表定理或其依賴仍含未完成內容；出現其他自訂公理，則必須回頭閱讀該公理的宣告與用途。Lean 的 axiom 文件同時提醒，系統不會替使用者證明新加入的公理彼此一致。這一層檢查的產出物是可歸檔的：作者明確建議企業審查紀錄不要只存「編譯成功」的截圖，至少要同時儲存 theorem 敘述、Lean 版本、依賴版本與 #print axioms 輸出。

第三層是 lean4checker --fresh，針對建置產出的 .olean 檔案，把其中的宣告與證明交回核心重播。官方驗證指南將其列為比一般建置多一層的檢查，並提醒它仍信任 .olean 的結構與建置環境；若要處理不可信的外部證明，官方另有 comparator 與外部 checker 的更高強度流程，涉及隔離建置。這一層的使用時機被作者限定在高價值研究、競賽或企業正式流程，也就是說，它是按任務風險定價的檢查，不是每個專案都該付的成本。

影響推演：誰付這筆帳

把三層檢查攤成成本結構，受益與承壓的位置相當清楚。採用 AI 輔助證明的數學研究與工程團隊，拿到的是把「機器說通了」細分為「編譯通過、公理清單乾淨、宣告重播一致」三項可查核的紀錄，審查責任從印象式判讀變成可歸檔的文件。承壓的一方則是流程中必須做最後人工確認的人：形式化敘述是否符合原始數學意思、自訂公理是否合理，這兩項在機器檢查的邊界之外，只能由具備數學背景的審查者以閱讀承擔。

這個「機器查語法、人工查語意」的分工，與醫療場景導入 AI 時的覆核成本結構同構，可參考本站先前的醫療 AI 五個檢查點的覆核成本帳：模型產出越快，驗證與責任歸屬的帳就越集中在下遊的審查環節。

收束判斷

這篇文章可確認的貢獻，是把 Lean 官方文件散落的驗證手段整理成一條按風險遞增的檢查序列，並點出每一層的信任邊界。它沒有提供 AI 證明錯誤率的實測數據，也未對 AI 定理證明的可靠度下定論；在這類數據出現之前，合理的結論是保守的：三層檢查能壓縮機器端的模糊空間，但形式化命題與原始數學問題之間的對應，仍是一項無法外包給工具的人工成本。