こんにちは｜こんばんは。カエル圖示活動中的 @kyamaz です。

前言

2026 年 9 月 8 日，生成式 AI 宣布解決了數學領域著名的千禧年懸賞問題之一——納維耶－史托克斯方程存在性與光滑性問題（的一部分）。據說其結果顯示：「在有外力的情況下，三維流體的解可能在有限時間內產生奇點，也就是說，光滑解不一定能永遠持續下去。」看到這則新聞的人應該不少吧。

我 之所以在這裡特別留意，是因為這項成果不只是以解析證明公開，還同時附上了 Lean 的形式化。Quanta Magazine 的文章也寫到，這種形式化讓數學家「giving mathematicians confidence that it is indeed correct」（對其確實正確更有信心）。即使證明重到人類無法完整讀完，只要機器通過了，就能相信。也因此，Lean 這個程式語言似乎受到了相當大的關注。至於成果歸屬與發表過程所引發的爭議，本文不打算深入。

【納維耶－史托克斯的新聞文章與 Lean 程式】

而且，也別忘了在那之前大約兩個月發生了什麼。2026 年 7 月，有一個「借助 AI 反證了哥德巴赫猜想」的證明被公開。這個證明同樣是用 Lean4 撰寫，也據說通過了機器檢查。然而三天後，真相曝光：那份 Lean4 證明並不是數學上的驗證，而是利用了 Lean4 處理系統本身的 bug。

定理證明助理（proof assistant）會機械地判定你寫的證明是否正確；只要形式化正確且編譯通過，就會給你一個勾勾。它既可以成為相信千禧年懸賞問題被解決的根據，也可能讓錯誤的證明蒙混過關。這件事似乎浮現出一個平常不太會意識到的問題。

【疑問】
「Lean 證明通過了」這句話裡，我們究竟相信的是什麼？那麼 Lean 本身正確無誤，又是誰來保證的？

我 並不是形式方法的專家，也不是每天都在寫 Lean。即便如此，這個問題還是讓我很在意，所以本文想整理一下我查到的內容。看起來，這個問題其實又可分成三個不同的問題：

• Lean 的邏輯體系裡有沒有潛藏矛盾（數學上的問題）
• 作為程式的 Lean 有沒有 bug（實作上的問題）
• 一開始寫下的命題，是不是真的符合原意（描述上的問題）

第一個完全沒問題，第二個卻出錯，那也一樣完蛋；第一和第二都沒問題，第三卻歪掉，那也沒有意義。接下來就依序來看。

先來釐清「有矛盾」是什麼

形式系統所謂「有矛盾」，是指能從中證明出假命題（False）。在矛盾的系統裡，會因為爆炸律（principle of explosion／「在邏輯中，從矛盾（假）可推出任意命題」的原理）而讓所有命題都可被證明。比如說，可以把它想成某個型別系統出現漏洞，導致只要是任何型別的值都能從 undefined 生出來的狀態。若黎曼猜想也能在這種夾雜著「$1 = 2$」之類矛盾的裝置裡被證明，那它就完全沒有價值了。
所以「Lean 是否無矛盾？」其實等同於「在 Lean 裡能不能證明 False？」。

問題 1：作為邏輯體系的無矛盾性 〜 哥德爾之壁

那麼，證明無矛盾性不就好了嗎？問題的第一道牆就在這裡。這正是《哥德爾第二不完全性定理》所說的：一個具有足夠表達力的無矛盾形式系統，無法證明自身的無矛盾性。

也就是說，在 Lean 裡不可能證明「Lean 是無矛盾的」。更糟的是，如果 Lean 真的能證明這件事，那反而代表 Lean 自己是矛盾的。這不是 Lean 的缺陷；ZFC 集合論或皮亞諾算術也一樣逃不掉，這應該被視為數學基礎的限制。

數學改走的路，是證明相對無矛盾性。也就是像「若系統 M 無矛盾，則系統 T 也無矛盾」這樣的主張：把 T 翻譯到 M 裡，並證明若 T 能推出 False，那麼 M 也能推出 False。

但重點在於，這並沒有真正消除原本的問題。它只是把「Lean 可不可靠？」改成了「系統 M 可不可靠？」而已。我 理解到，相對無矛盾性的證明不是用來消除問題的，而是用來轉移問題的。之所以仍然有意義，是因為轉移到的是一個已被使用了數十年（若以數學作為框架來看，甚至可說是數百年、數千年）且沒有出現矛盾跡象的體系。信任不是靠證明，而是靠實績；這和挑選成熟函式庫時的判斷邏輯其實很像。

就 Lean 而言，Mario Carneiro 在 2019 年的論文中證明了其型別理論具有與 ZFC ＋「存在 $n$ 個不可達基數」（對所有自然數 $n$）相當的無矛盾強度。不可達基數，是指大到無法由下往上以一般構造程序到達的無限大基數。也就是說，Lean 除了需要接受 ZFC 的無矛盾性之外，還得接受與不可達基數相關的假設。

不過這裡要注意：這個結果是針對 Lean3 的。 Lean4 擴充了型別理論（例如巢狀歸納型別、結構體的 $\eta$ 規則等），Carneiro 自己也在後續論文中提到，2019 年的健全性證明已無法直接套用。 查到的資料顯示，和「Lean 相對於 ZFC + 不可達基數無矛盾」的說法相反，截至 2026 年 9 月，Lean4 型別理論的完整無矛盾性證明似乎仍未完成。

不過，這個課題並不是被放著不管。Lean4Lean 這個專案正在同時驗證邏輯體系的性質，以及型別檢查器是否依照規則運作。驗證型別檢查器確實依指定推論規則運作，和無條件地自證那些規則本身的無矛盾性，是兩回事。論文裡仍保留著像「型別唯一性」這類被視為猜想的項目，但它把需要型別檢查器正確性的證明，和以其他途徑推進的健全性證明區分開來。能夠追蹤哪些已證明、哪些尚未證明，本身就可說是一種健全性的表現，但看來目前還不算完整。

【Lean4Lean 的論文】

問題 2：理論正確，但實作可能出錯

接下來這個應該就是工程師會感興趣的部分了。即使假設邏輯體系本身是無矛盾的，若實作它的程式有 bug，仍然可能證明出 False（假）。

證明物件 〜 為何只要信任檢查器就好

要理解 Lean 採用的防護策略，得先掌握「證明物件」這個概念。簡單來說，在 Lean 裡會把「定理視為型別，而證明視為具有該型別的項（資料）」來看。也就是說，證明其實是存在於處理系統中的資料結構，之後可以再拿來檢查，成為證據（certificate）。

產生證明的部分（tactics、elaborator、型別推導）很複雜，但檢查輸出的證明物件時，只需要一個單純機械比對規則的小程式就夠了。也就是說，我們只要信任檢查器（kernel）就行。這種設計原理據說稱為『德布魯因準則（de Bruijn criterion）』。可以把它想成：不是信任整個編譯器本體，而是把輸出的機器碼交給一個小型驗證器去檢查。
把需要信任的程式，也就是 TCB（Trusted Computing Base）維持到最小。到這裡都非常漂亮。

但問題是，核心並不小

然而 Lean 的核心未必真的「小而單純」。為了效能與表達力，像巢狀歸納型別、結構體投影、多倍長整數運算（透過 GMP 進行自然數高速計算）這些功能都進了核心。它也是少數在轉移到 Lean4 時沒有被重寫、而是仍以 C++ 保留的元件之一。換句話說，核心功能一多，攻擊面也就跟著變大。

而到了 2026 年，這件事真的發生了。前面提到的哥德巴赫「反證」所利用的，就是巢狀歸納型別的處理1。在建立輔助型別時，原本不會出現在建構子欄位裡的參數（phantom parameter）被弄丟了，於是繞過了型別檢查。也就是透過那個漏洞，證明了本來不該能證明的 False。而且據說在報告提出後僅一小時就送出了修補程式。
更可怕的是，這份證明同時通過了 Lean 官方核心，以及另一個獨立實作的檢查器——Chris Bailey 的 Rust 實作 nanoda。更何況，根據這個 bug 的事後檢討1，兩邊踩到的是彼此無關的兩個 bug。nanoda 雖然有檢查相關區塊，卻沒有驗證投影節點的型別名稱。於是「有兩道檢查就安全」這個前提，也在現實中被擊破了。

在這之後，從 7 月 30 日到 8 月 20 日，OpenAI 的 Daniel Selsam 使用公司內部模型，集中尋找核心與執行階段的健全性 bug；結果修正了核心健全性 4 件、執行階段健全性 2 件，以及其他 5 件問題。其中一項手法，是對某個物件建立大量參照，讓參照計數繞回一圈，進而破壞物件狀態並製造出 False；另一項則是 Linux 版的 CI 因為 libc 相容性而使用 GMP v6.1.2（多倍長整數運算函式庫）進行建置，於是可以利用其已知 bug。也就是說，證明的健全性，會從記憶體安全性或外部函式庫這些「非數學層」被攻破。這些修正已於 8 月 21 日以 v4.33.1 釋出。
Lean 的作者 Leonardo de Moura 表示：「這種事之後還會一直發生。AI 在找出核心健全性 bug 方面真的非常擅長。」而在這次 bug hunt 的事後檢討2中，也明確寫道：「我們認為 AI 產生的證明，是潛在惡意證明的來源。」證明驗證看來同時也是數學問題與資安工程問題。

這不是 Lean 特有的問題

這些全部都是實作 bug，不是理論上的漏洞。只要修掉就會消失的缺陷而已。不過從使用者角度來看，最後都是同樣的結果：出現了錯誤的勾選標記。
而且，這似乎也不是 Lean 特有的問題。Rocq（舊稱 Coq）過去也曾發現過健全性 bug，甚至還有一份管理已知重大 bug 的清單。大概幾乎不存在那種「被長期使用卻從未發現任何實作 bug」的證明助理吧。差別可能在於：設計是否盡量讓 bug 不容易出現，以及一旦出現，是否有快速修復的機制。

採用『LCF 架構』的 Isabelle/HOL 設計者 Lawrence Paulson 問過一句話：「為什麼什麼都要放進核心？」在 LCF 系統傳統（HOL Light、HOL4、Isabelle/HOL）裡，遞迴、歸納資料、模式比對都不放進核心，而是由最小原理在核心外推導。雖然麻煩，但信任的部分會大幅縮小。他的結論是：「如果健全性最重要，就該選 HOL Light 或 HOL4。」另一方面，Lean 的設計則是為了實現表達力、效能，以及龐大的數學函式庫（mathlib）而做的選擇。所以重點不是誰對誰錯，而是要在信任面積與生產力之間取哪個平衡。我想這才是問題所在。大家會怎麼選呢？

【Paulson 的部落格文章】

「只要增加檢查器就好了」是答案嗎

對於採用『德布魯因準則』的設計本身，Paulson 還提出了另一個尖銳的問題。把證明物件當成證明書攜帶，再交給另一個檢查器檢查——這套設計本身的價值，這次就被質疑了。因為官方核心與 nanoda 竟然都放行了同一份證明。照他的比喻，這就像「拖著備用車到處跑」；如果會因為同一個理由一起壞掉，那備用品根本不算備用。
這個批評我覺得有一半是對的。獨立實作，不等於獨立故障。 這次的確是兩個不同的 bug 讓同一份證明通過了。不過在獨立檢查器的一般設計裡，也得注意規格或演算法共享造成的共同缺陷。若多個檢查器都讀同一份規格、寫著相同演算法，只要規格本身有洞，它們就會一起放行。冗餘到底有多有效，取決於實作系統有多分散；這和軟體容錯領域長久以來的道理其實是一樣的。

而且這種對策也不只是單純把數量堆上去而已。comparator 會在可信環境中比對命題與提交證明所對應的命題是否一致。它會先在沙盒中建置證明，取出證明項，再交給沙盒外的多個獨立檢查器。lake check --paranoid 是一個會用所有內建核心重新檢查專案的指令，預計會從 v4.35.0 開始提供。另有計畫是把 lean4checker 同時提供 GMP 版與 mpn 版；甚至也有人打算自行實作經驗證的任意精度運算套件，直接切斷對外部運算函式庫的依賴。還有 lean4lean，那是用 Lean 自己寫成的核心，目標是未來能接受形式驗證。最後這項不是單純在旁邊增加更多檢查器，而是想藉由證明去提升單一檢查器本身的可信度。證明物件這種設計的價值，正是在這種時候最能看出來；只要證明是可攜帶的資料，檢查器就可以一直加，而其中一個也可以先透過形式驗證來鞏固。

問題 3：最後的洞，在人類這一側

即使理論與實作都完美，還是會留下洞。而且在實務上最該注意的，恐怕就是這裡。

正確證明的無意義定理

當核心打出勾勾時，它所保證的只不過是：「這裡寫下的形式命題，可以從所宣告的公理推出。」至於這個命題是否真的符合你原本想表達的內容，完全不保證。假設太強，導致定理空洞地成立；符號或型別類把定義藏起來，讓你讀到的意思和真正的意思不一致。這些錯誤就算證明再多次也抓不出來。結果就會變成一個正確證明、卻毫無意義的定理。
這並不是紙上談兵。前面提到的納維耶－史托克斯方程事件裡，Quanta Magazine 的文章就寫道： "The crucial bit of verification that must still be done by humans is to guarantee that the statement being shown to be true in Lean is logically equivalent to what mathematicians set out to prove"（人類仍必須完成的關鍵驗證，是保證在 Lean 中被證明為真的命題，與數學家原本打算證明的內容在邏輯上是等價的）。即使是千禧年懸賞問題，最後也還是得回到這一步。

意圖性的後門，以及公理審計

此外，Lean 還有好幾種刻意設計的後門。

【刻意設計的後門】

• sorry …… 先把證明延後處理
• 原生評估（native evaluation）…… 在核心外執行原生碼，並相信其結果
• @[implemented_by] …… 把實作替換成別的東西
• 跳過型別檢查的除錯用選項

這些要嘛會帶入未證明的假設，要嘛會擴大可信實作的範圍。它們都有正當用途，但因為使用方式會改變證明所需的前提，所以必須小心確認。沒學過 Lean 的人，可能甚至不知道 sorry 這東西的存在。sorry 是初學者在卡關時拿來先把證明跑通，或是在逐步撰寫程式時很好用的語法，所以很多人在很早期就會學到這個後門。只要曾經碰過一點 Lean 的人，看到新聞裡的 Lean 程式，第一眼大概都會去找有沒有 sorry；但不知道的人，就算看到 sorry 也可能誤以為那是已經正確證明了。

幸運的是，依賴了哪些公理可以查出來。

#print axioms my_theorem
-- 'my_theorem' depends on axioms: [propext, Classical.choice, Quot.sound]

這三個（命題外延性、選擇公理、商型別健全性）都是 Lean 的標準公理，所以出現它們並不是問題。反過來說，如果出現 sorryAx 或不認識的自定義公理，那就該拉警報了。可是，目前並沒有任何指令能判定「這個命題的意思對不對」。形式命題是否真的和人類意圖一致，光靠證明通過並不能保證，最後還是得靠人工審查。

【官方參考資料〈Validating a Lean Proof〉】

那麼，實際上該怎麼做

與其停留在抽象討論，不如整理成實務上的指引。

【AI 時代處理證明時的指引】

• 閱讀定理主張（statement）…… 單靠形式驗證無法保證和原意一致，因此要審查主張本身，以及它所引用的定義
• 把 #print axioms 納入 CI …… 機械式確認依賴公理落在 {propext, Classical.choice, Quot.sound} 的子集合內
• 把他人的證明，尤其是 AI 生成的證明，視為不可信輸入…… 在沙盒中建置，並用 comparator 或多個檢查器重新驗證
• 直接更新處理系統…… 健全性 bug 會被公開並迅速修補。停留在舊版通常風險更高
• 不要把保證範圍說得太滿…… 「在 Lean 裡證明了」只代表「目前這個處理系統判定：這個形式命題能由這個公理系統推出」，僅此而已

總結

「Lean 是否無矛盾？」這個問題的答案，看起來會依不同層次而不同。

• 邏輯體系…… 原理上不存在絕對保證。能說的只有相對無矛盾性，而移轉目標是 ZFC + 不可達基數。且這個證明是 Lean3 的版本，Lean4 版目前仍在進行中
• 實作…… 理論正確不代表程式不會出錯。可能會從參照計數或外部函式庫這些非數學層面被攻破
• 描述…… 即使理論與實作都沒問題，只要寫下的命題和原意偏掉，一切就都失去意義

這些層次沒有一個是完全可靠的。實務上只能靠沙盒建置、多個獨立檢查器、用 #print axioms 進行公理審計，以及對主張本身做人工審查來補強。
我認為，證明助理並不是「輸出絕對真理的機器」。更接近現實的描述，或許是：它是一種把需要懷疑的對象縮小到人類可審查規模的裝置。信任不是從單一證明而來，而是來自理論、實作、運作流程與人工審查的層層累積。

結語

不知道各位覺得如何？本文把「Lean 是否無矛盾？」這個直觀的問題，拆成邏輯體系、實作、描述三個層次來看。這個結構，其實和我們平常在做軟體品質保證或資安時的思路很像。證明助理比較特別的地方，也許在於多層防護中最內層那一層，竟然是建立在數學體系上的定理。這已經非常厲害，但並不是萬能。

另外，本文是我 根據公開資訊蒐集整理而成。至於 Lean4Lean 尚未解決的猜想後續如何，我沒有完整追蹤；而對於 bug hunt 中找出的各個問題，也只整理到 de Moura 的事後檢討為止。若有錯誤或更新的資訊，還請不吝指教。

感謝您的閱讀。
（●）（●） Happy Hacking!
/"" ＿＿""＼

1. 這是作為 Lean issue #14576 回報的 bug。問題在於核心在移除巢狀出現（nested occurrence）時，所建立的輔助型別會把建構子欄位中未出現的參數（phantom parameter）遺失。攻擊路徑是透過巨集程式設計直接把 inductive 宣告送進核心；一般經由前端的路徑則會被檢查攔下。這個 bug 的事後檢討（↓）
   https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/ ↩ ↩2
2. https://leodemoura.github.io/blog/2026-8-24-postmortem-for-the-kernel-soundness-bug-hunt/ ↩

原文出處：https://qiita.com/kyamaz/items/7b38e5977dc97747d2d9