AI 定理證明怎麼驗證？Lean 4 實作與檢查清單

AI 說「數學證明完成」時，最可靠的第一步是把它放進 Lean 4 專案重跑，確認形式化命題、proof term、imports 與版本都能通過檢查。只看到模型輸出的自然語言推理，或看到編輯器出現勾勾，還不足以回答原本那個數學問題是否被忠實表達。

這篇接續AI 用 Lean 證明數學定理的前一篇解釋往下做，重點放在「拿到一份 AI 產生的證明後怎麼驗」。如果你是在評估模型能不能放進研究或工程流程，也可以先對照AI 模型選型的成本與驗收表，把可驗證性列進測試條件。

先判斷你拿到的是哪一種「通過」

AI 產生的數學答案有三層，讀者先把它們分開，後面的檢查才不會混在一起。

• 自然語言答案： 模型用文字寫出推理，仍要由人逐段檢查定義、計算與推論。Google DeepMind 形容自然語言方法可能產生看似合理、實際錯誤的中間步驟，這也是 AlphaProof 改用 Lean 形式化流程的理由。Google DeepMind 的 AlphaProof 說明有交代這個差異。
• 形式化命題： 原本的題目被翻成 Lean 能讀的 statement，例如變數型別、條件與要證明的結論都要明確寫出。Lean 官方文件要求每個推理步驟回溯到定義、定理、規則或公理。Lean 4 介紹說明了這個驗證目標。
• kernel 接受的證明： Lean kernel 接受 proof term，代表目前檔案與匯入的內容足以推出這個形式化命題；官方把編輯器的藍色雙勾定義在這個層次。Lean 官方的 Proof Validation 文件也提醒，還要確認 statement 符合原本想證明的意思。

因此，讀者第一個問題不該是「這個模型數學能力多強」，應該是「它交出的檔案能不能在指定環境重建，題目翻譯有沒有漏掉前提」。這套判斷也能延伸到AI 模型選型怎麼做，因為模型排行榜不會替你驗證實際任務。

AI 定理證明怎麼運作：從題目到 kernel

這條流程可以拆成四步。AlphaProof 的公開說明提供一個完整例子：先把自然語言題目轉成 Lean 的形式化敘述，再由模型搜尋證明步驟，最後交給 Lean 驗證；已驗證的證明還能回到訓練迴路，協助尋找後續解法。Google DeepMind 的流程說明記載，AlphaProof 與 AlphaGeometry 2 在 2024 年國際數學奧林匹亞合計解出六題中的四題，得分 28 分。

1. 把題目寫成可檢查的 statement

人類題目常把條件藏在上下文裡，Lean 要求型別、變數範圍、假設與結論寫清楚。這一步由人或 AI 完成，最容易產生「形式化後其實換了題目」的風險。Lean 官方驗證手冊把「形式化命題是否對應原本意義」列為獨立的信任條件，不能用 kernel 勾勾代替。官方說明可直接對照。

2. 由模型或人尋找 proof term

Lean 的 tactic 可以幫忙展開細節，但每個 tactic 最後都要產生核心型別理論能檢查的 term。官方語言參考指出，tactic 的錯誤不會直接繞過 kernel，因為產物仍要交給 kernel 檢查。Lean Language Reference說明了這個分工。

3. 由 kernel 檢查邏輯鏈

驗證成功代表 proof term 符合目前的定義、定理、imports 與公理，並通過 Lean kernel 的規則。它能攔下缺步驟、tactic 錯誤與尚未完成的 proof，但它不替你判斷題目翻譯是否正確。Lean 的藍色雙勾說明把這個邊界寫得很清楚。

4. 用 Lake 重建整個專案

Lean 官方安裝手冊要求程式放在 Lake 管理的專案中，Mathlib 專案則提供 lake build、lake test 與預編譯快取。對 AI 產物來說，重跑的價值在於把版本、相依函式庫與建置結果一起留下來，降低「在某台電腦曾經通過」的灰色地帶。Lean 安裝手冊與Mathlib 官方 README都有列出這些入口。

看到藍色雙勾，還要再查三件事

命題與原題是否相同

假設漏掉一條、變數範圍縮小，或把「對所有」誤寫成「存在一個」，都可能讓證明難度大幅下降。Lean 會忠實檢查你寫下的命題，沒有替人補回原始題意的功能；官方文件也把 statement 的語意對應列為使用者必須信任的部分。Validating a Lean Proof直接提醒這一點。

是否留下 sorryAx

sorry 是撰寫長證明時暫時填洞的工具，Lean 會發出警告；它也會在依賴中留下 sorryAx。完成驗收時，在 theorem 後加入 #print axioms theoremName，只看到 Lean 的標準公理才算清楚知道依賴範圍；看到 sorryAx 就代表證明仍有未完成部分。Lean 的 Axioms 文件與Tactic Reference都有說明查法。

版本與外部函式庫是否固定

Mathlib 是由社群維護的 Lean 數學函式庫，含數學內容、程式基礎設施與 tactics；官方 README 也提供快取下載、建置與測試指令。Mathlib4 官方倉庫顯示，專案要依照自己的 lean-toolchain 與依賴設定重建。企業保存 AI 證明時，我會把這些檔案、建置日誌與 #print axioms 結果一起封存，未來才知道當時驗的是哪個環境。

台灣現在到哪：入口已經有，產業普及不能亂推

台灣目前能直接查到的進展，集中在教學與研究場景。國家理論科學研究中心在 2025 年於台大舉辦 Lean 學習講座，主題包含互動式定理證明、數學研究與形式化驗證，並開放不同背景者參加。NCTS 活動頁可確認活動時間、地點與內容。

2026 年中研院資訊科學研究所公開的 Lean-QEC 演講，則把 Lean 4 用在量子錯誤更正碼的形式化，產生可由機器檢查的距離證明，並描述在工業規模的量子位元碼族上測試。中研院演講摘要顯示，這已經超出課堂示範，進入研究工具鏈，但單一研究案例不能拿來代表台灣企業普遍導入。

對台灣個人使用者，最可行的路徑是直接採用 Lean 4、VS Code 擴充功能與 Mathlib，從小命題開始重跑。對半導體、韌體或高可靠軟體團隊，則可把形式化驗證視為一種要求產物可重建的工程方法；Lean 官方也把數學推理與複雜系統的推理放在同一個工具定位裡。Lean 4 介紹與語言參考都支持這個使用範圍。

一般人與企業的檢查順序

一般人拿到 AI 證明

先要求對方交付 .lean 原始檔、使用的 Lean 與 Mathlib 版本、專案設定，以及一個能重跑的命令。接著先讀 theorem statement，再執行 lake build；最後用 #print axioms theoremName 檢查是否含 sorryAx。Lean 官方的安裝流程從 Lake 專案開始，這個順序也最接近可重現的基本要求。官方安裝手冊與驗證手冊可作為操作依據。

企業把 AI 放進驗證流程

驗收表至少要有四欄：原始需求與形式化 statement 的對照、toolchain 與套件版本、lake build 的乾淨結果、#print axioms 的依賴清單。若證明要進晶片、韌體或安全關鍵軟體流程，還要保留人工審查紀錄，因為 kernel 能確認邏輯鏈，無法替團隊判斷需求是否寫對。

我的結論很簡單：AI 產生數學證明值得用，但交付格式要從「一段看起來合理的文字」升級成「可重建的形式化專案」。Lean 解決的是推理步驟的機械檢查；題目翻譯、前提選擇、版本管理與結果能否套回現實，仍然是人和團隊的責任。

常見問題

AI 產生的數學證明，看到 Lean 藍色雙勾就能相信嗎？
藍色雙勾代表 Lean kernel 接受目前形式化命題的證明，不能替你確認命題和原始題目意思相同。還要檢查前提、imports、版本，以及是否含有 sorryAx；完整查法見 Lean 官方驗證文件。

一般人要怎麼開始驗證 AI 定理證明？
先安裝 Lean 4 與 VS Code 官方擴充功能，再建立 Lake 專案和 Mathlib 依賴，執行 lake build。拿到既有證明後，先讀 theorem statement，再用 #print axioms theoremName 檢查依賴，步驟可對照 Lean 安裝手冊。

台灣有沒有可以直接學或研究 Lean 的入口？
國家理論科學研究中心曾在台大舉辦 Lean 學習講座，中研院資訊科學研究所也公開 Lean-QEC 的研究演講。這些資料能證明台灣有教學與研究入口，尚不足以推算全台產業採用比例；可先從 NCTS 活動頁與 中研院演講摘要開始。