AI 產出的 Lean 4 證明，最基本的驗法是放回固定版本的專案執行 lake build；高風險任務再檢查 #print axioms，最後用 lean4checker --fresh 重播建置出的 .olean。lake build 成功代表 Lean 核心接受目前的形式化命題與其匯入依賴，還要人工確認命題真的對應原本的數學意思。Lean 官方驗證文件把這幾層檢查分開說明。

既有的AI 用 Lean 證明數學定理的解釋談的是形式化證明為何能被機器查證，本文聚焦讀者拿到一份 AI 產出的 Lean 程式後，怎麼在自己的環境判讀「通過」到底代表什麼。

Lean 4 在驗證什麼？

Lean 4 同時是程式語言與互動式定理證明器。定理在 Lean 裡有一個形式化敘述，證明則是符合該敘述型別的項；Lean 的型別系統文件說明，只有通過型別規則的項才具有核心語意。

這個流程和聊天機器人回覆「證明完成」是兩件事。模型可以負責提出定義、引理與 tactic，Lean 仍會把結果交給核心型別檢查器；Lean 的編譯與 elaboration 文件列出的順序是剖析、巨集展開、elaboration、核心檢查，再進入編譯。

Lean 4 證明流程從程式碼經過 elaboration 到核心檢查的示意畫面
AI 只負責產生候選證明，Lean 核心會檢查它是否符合形式化命題（示意圖）。

第一步：在固定專案跑 lake build

先取得 AI 產出的完整專案，不要只複製一段 theorem。專案至少要能交代 lean-toolchain、lakefile.lean 或 lakefile.toml，以及匯入函式庫的版本；Lean 官方文件把 lake 定義為追蹤依賴並呼叫 Lean 的建置工具。

在專案根目錄執行：

lake build

建置沒有錯誤，表示這個版本的 Lean、這組匯入與這份 theorem 能完成核心檢查。Lean 的驗證指南也把「使用 lake build 後沒有錯誤或警告」列為與編輯器核取記號相同的日常檢查方式。

但這一步沒有回答兩個問題。第一，定理敘述是否把自然語言問題寫對；第二，證明是否透過 sorry 或自訂公理留下未完成的假設。錯誤訊息要先分成「語法或型別不合」與「命題本身寫錯」兩類處理，重跑一次通常只會得到同一個結果。

第二步：用 #print axioms 查證明依賴

在 theorem 後加入：

#print axioms theoremName

theoremName 要換成實際定理名稱。官方驗證文件指出，輸出若只包含 propext、Classical.choice、Quot.sound 這三個 Lean 內建公理，通常屬於可接受的基線；出現 sorryAx，代表定理或其依賴仍含有 sorry 或其他未完成內容；看到其他自訂公理，則要回頭閱讀它的宣告與用途。Lean 的 axiom 文件也提醒，Lean 不會替使用者證明新加入的公理彼此一致。

這個結果很適合放進 AI 證明的審查紀錄。企業不要只保存「編譯成功」的截圖，至少要同時保存 theorem 敘述、Lean 版本、依賴版本與 #print axioms 輸出。

終端機顯示 Lean theorem 的 print axioms 輸出與公理清單
公理清單能補上單純編譯結果看不到的依賴資訊（示意圖）。

第三步：需要更高把握時跑 lean4checker

一般專案完成 lake build 就能確認目前程式碼通過 Lean 核心檢查；若證明要進入高價值研究、競賽或企業正式流程，可再執行：

lake build
lean4checker --fresh .lake/build/lib/YourProject/YourModule.olean

lean4checker 會讀取建置產生的 .olean，再把其中的宣告與證明交回核心重播。Lean 官方驗證指南把它列為比一般建置多一層的檢查，也提醒它仍信任 .olean 的結構與建置環境。實際 .olean 路徑會依專案名稱與模組而變，先在 .lake/build/lib/ 找到對應檔案，不要直接照抄上面的佔位路徑。

若要處理不可信的外部證明，官方另列出 comparator 與外部 checker 的更高強度流程。這已涉及隔離建置與受信任的 challenge 檔，不適合把一般 AI 程式碼直接丟進個人電腦測試；本文先把日常專案需要的三層檢查講清楚。

版本與依賴怎麼固定？

Lean 專案的可重現性，先從 lean-toolchain 開始。Elan 官方文件建議專案指定明確的 Lean 版本，並把這個檔案跟程式碼一起放進版本控制；這能避免不同開發者用到不同工具鏈。Elan 的工具鏈說明也說明，修改 lean-toolchain 後，新的工具鏈會在下一次開啟或建置 Lean 檔案時安裝並使用。

Mathlib 依賴則要看 lakefile 與 lake-manifest.json。Mathlib 官方的依賴說明要求使用相同的 Lean 4 工具鏈，並建議更新下游專案依賴時執行 lake update mathlib，由 Lake 更新 manifest；Mathlib 官方 GitHub 說明也建議大型專案採用對應 Lean 穩定版的 Mathlib 標籤，減少直接追 master 的變動。

我的判斷是，台灣團隊目前最實用的落地方式，是把 lake build、#print axioms 與必要的 lean4checker 放進 CI，並把 lean-toolchain 和 manifest 一起審查。官方工具鏈沒有台灣專屬的驗證步驟，地區差異會落在企業的 CI 權限、套件下載政策與程式碼審查流程；若還要評估 AI 模型本身，應把編譯通過率、失敗類型與人工修正時間納入AI 模型選型的評估表，不要只比較模型回答看起來是否流暢。

一般人與企業各自該注意什麼？

使用情境最少要做的檢查判讀重點
個人學習或小型實驗lake build、閱讀 theorem 敘述先確認命題和問題相符，再看是否有錯誤或警告
AI 輔助研究加跑 #print axioms保留公理清單，查 sorryAx 與自訂公理來源
企業 CI 或高風險證明固定工具鏈、依賴與 build 紀錄，必要時跑 lean4checker --fresh讓其他人能在相同版本重跑，並保留審查軌跡

這套順序能回答「這段程式在目前環境是否成立」，也能提早抓到版本漂移與未完成證明。它仍不會替團隊判斷 theorem 的自然語言意義，命題、定義與假設需要由熟悉領域的人閱讀。

軟體持續整合流程中顯示 Lean 4 建置、依賴與檢查結果
企業導入 AI 定理證明時，版本與檢查紀錄和證明程式本身同樣重要（示意圖）。

常見問題

Lean 4 編譯成功，就代表 AI 證明完全正確嗎？
它代表目前的 Lean 核心接受這個形式化命題與證明項，還要人工確認 theorem 的敘述符合原本的數學問題。若命題一開始就寫窄、寫錯或用了不適合的假設，編譯仍可能成功。

為什麼還要跑 `#print axioms`？
因為編譯成功不會在畫面上完整呈現定理依賴的公理。`#print axioms` 可追出 `sorryAx`、自訂公理與其他依賴，讓團隊知道這份證明的成立條件；詳細判讀可參考 Lean 官方驗證指南。

一般人需要使用 lean4checker 嗎？
學習與一般小型專案先完成 `lake build` 和公理檢查即可。研究、競賽或企業正式流程需要更高把握時，再依官方文件用 `lean4checker --fresh` 重播 `.olean`，並確認工具鏈與依賴版本已固定。