還是需要人！

 

這個專案先做到這裡。 到目前為止可以確定的是：AI 可以協助數學推論，也可以把推論寫成 Lean、交給機器一步步檢查過去——這一段確實能跑，而且跑得比預期好。但最後一步的確認必須由人來做：確認那段 Lean 寫的，就是原本要證的那個主張。

這篇文章講的是為什麼那一步交不出去——以及我們試過哪些辦法想把它交出去，結果如何。

「Lean 核心接受某個定理，表示其證明在使用的公理與形式化定義下通過檢查，不必然表示原始自然語言的數學主張已被正確證明。」這是 AMPAS 這個專案一開始就設下的分界線。前兩個案例（FermatWeaker 把主張限制在 n ≤ 3；A13 數學命題一字未改卻重新定義了「質數」）說明這條線是真的存在。這篇記兩個新案例，它們把這句話推到更遠的地方：第一個證明沒有任何強度的 kernel 能補這個洞，第二個是我們為了讓這個判斷有跡可循而做的工具，自己在把陳述印出來的時候印錯了——印成了另一句話，而那句話是假的。

先講六個詞

下面每一個詞後面都會用到，而且其中兩個就是整篇的重點。

詞	意思
忠實度落差 （fidelity gap）	本文的主題。「證明被檢查過了」跟「那個主張成立」之間的距離。檢查器能確認前者；後者要有人讀 Lean 寫的那行陳述，判斷它說的是不是原本那句中文主張。本文四個案例全部落在這道落差裡。
kernel（核心）	Lean 裡真正做檢查的那一小塊程式，幾千行。它只回答一件事：這個證明在給定的定義與公理下站不站得住。
宣告 （declaration）	送進檢查器的一條條東西：一個定義，或一個定理連同它的證明。一份提交通常帶著它所依賴的幾萬條。
sorry	Lean 裡的「這裡先跳過」。寫了它，任何陳述都能「證完」。所以一份提交裡只要有一個 sorry，它就什麼都沒證明——檢查的第一件事就是把它找出來。
對抗性測試	不是為了確認東西能動，而是特意寫來騙過檢查器的測試。關鍵在於是誰寫的：自家寫的對抗測試，只測得到自己想得到的騙法。
凍結（freeze）	把一個陳述、連同它依賴的所有定義，算成一個雜湊值記下來。之後只要一個字或一個定義被改掉，雜湊就對不上。

其中 sorry 跟對抗性測試值得多說一句。sorry 是最容易防的一類攻擊：它留下痕跡，機器一找就到。本文四個案例沒有一個用到它。 它們的證明都是真的、完整的、每一步都站得住的——這正是它們難對付的地方。

每一層擋住什麼

［此處插入圖片：驗證管線分層圖］

左邊是 AMPAS 實際跑的每一層，按順序由上到下。上面六層是機器檢查：不需要人判斷，程式自己跑完就能給出是或否。最下面一層是人讀的。前三個案例的共同點是它們不是被哪一層機器檢查擋下來的：每一層都通過了，因為每一層檢查的都是「這個證明成立嗎」，而不是「這個陳述是那個主張嗎」。它們唯一可能死的地方是最下面那層。

而案例四不在這條路上。它不是穿過哪一層，它是最後那一層所讀的材料本身被污染。兩者的差別很實際：前三個要靠「找更多人讀」減輕，案例四則是找再多人讀也沒用——他們讀到的是同一份錯的語句。

新案例一：一個帶一致性證明的檢查器，接受了錯的陳述

一般人會這樣推論：既有的案例之所以漏掉，是因為檢查器不夠強；換一個「被證明過」的檢查器就好了。這個推論可以被實際測掉，而我們測了。

con-leche 是一個用 Lean 寫的檢查器，它特別的地方在於：檢查器本身被證明過。

這句話要拆開講。有人在 Lean 裡證了一條定理，內容是：只要 con-leche 接受了一組宣告，那組宣告就一定不會自相矛盾。 證法是證「它在集合論裡有模型」：所謂模型，就是一個真正的數學世界，裡面那組宣告每一條都成立。一組宣告只要找得到這樣一個世界，就不可能從它推出矛盾來——也就是說，它不可能證出 False。

所以這不是「作者很小心」那種信心，是一條機器檢查過的定理（ConLeche.no_False_declaration、ConLeche.model_exists）。我們把它整套從原始碼建起來，包含證明那條定理的那一部分——沒自己建過的驗證，不構成任何證據。

然後餵給它 A06_wrong_statement。這個攻擊只有一行：

theorem add_comm_nat : ∀ a : Nat, a + a = a + a := fun _ => rfl

它掛在 add_comm_nat 這個名字下，而那個名字的主張是加法交換律（∀ a b, a + b = b + a）。送進去的是 a + a = a + a：一個真定理，一個誠實的證明（rfl：兩邊按定義就是同一個東西），沒有 sorry，沒有偷加公理。最容易找的那幾種毛病，它一個都沒犯。

con-leche 接受了。 而且它檢的不只是那一行：是那一行連同它所依賴的整個 Lean 標準函式庫，一共 58,102 條宣告。跑完花 40 秒、吃掉 0.42 GiB 記憶體。這三個數字在這裡是為了堵住一個很自然的疑問：「是不是它跑不完就放行了？」不是。它完整、快速、輕鬆地跑完了——然後接受。

它沒有理由不接受。那個陳述是合法的（文法跟型別都對），那個證明是對的，整組宣告也確實不自相矛盾。它唯一的問題是不是它掛在那個名字下的那個主張——而那件事不是任何 kernel 判定的對象，無論那個 kernel 自己被證明得多嚴密。

所以這道落差不是「檢查器不夠強」造成的。再強的檢查器也看不到它，因為沒有任何一個檢查器在回答這個問題。它們全部都在回答另一個問題：這個證明站不站得住。

這件事值得特別講，因為它把前兩個案例的意義整個翻轉過來。FermatWeaker 和 A13 讀起來像是「我們的檢查還不夠完整」，可以靠加強工具解決。con-leche 證明了那是誤讀：這兩個案例不是在量工具的強度，是在指出一件工具根本沒在處理的事。

新案例二：稽核證據自己是錯的

前面三個案例都是同一個種類：證明成立，陳述不是那個主張。第四個不是。

既然機器補不了這個洞，剩下的就是人。而 AMPAS 裡人的那一層是六個「是／否」的勾選欄：statement_matches_text、no_unintended_convention、quantifier_order_checked 等。十三份經過簽署的審核紀錄，六項全部 true。問題不在於這些答案錯，而是一個認真讀完陳述的審核者，與一個四秒鐘勾完六個格的審核者，留下的紀錄一模一樣——不是「差不多」，是每一個字元都相同。

所以我們做了一個工具：從凍結的陳述本身推導出每一項勾選「是關於什麼」——這個陳述前面宣告了哪幾個變數、按什麼順序、哪些容易踩到的數學慣例在場、哪些定義必須讀過。機器不會讓判斷變正確，但它能讓草率變得看得見。

第一版跑出來的結果裡，有一條是這樣的：

	內容	讀出來是
凍結的陳述 Challenge.lean:31	∀ n : Nat, ∃ m, n < m	對每一個自然數 n，都存在一個 m 比它大
證據工具呈現的結論	∃ m, m < m	存在一個 m 比它自己小

上面那個是真的，而且是小學就懂的事。下面那個是假的。

機制很單純，而且跟數學沒關係。一個陳述的開頭是一串變數宣告——「對所有的 n」、「存在一個 m」。程式要把這個陳述印出來，得先把這串變數一個個拆開、記住每個叫什麼名字，印完再收起來。我把順序寫反了：收起來之後才去印。那時 n 這個名字已經不在記事本上了，印的時候就拿了手邊還在的那個名字——內層的 m——於是兩個不同的變數被印成同一個。

這個缺陷的形狀跟前面三個都不同：

• 陳述是對的
• 證明是對的
• Lean 核心、第二個 kernel、第三個檢查器、六個審核勾選、雜湊搭配——全部正常
• 錯的是為了證明這些都正常而做的那份證據

假設我沒發現。一個審核者打開證據檔，看到 ∃ m, m < m，然後在 statement_matches_text 勾了 true。那份簽檔會永久對外表示：有人逐條審過，而且審的是哪一版陳述，有雜湊值可以對——那個陳述只要被改掉一個字，雜湊就對不上，簽檔立刻失效。

而它不是被測試抓到的。 當時跟它一起跑的 25 個測試全部通過——因為那些測試檢查的是「證據檔裡那六個項目是不是都有填到東西、雜湊有沒有算對」，也就是檔案的形狀對不對。沒有一個測試在問「那些字印出來的，是不是那個陳述」，也就是檔案的內容對不對。抓到它的方法是把輸出跟 Challenge.lean 的原文擺在一起讀。

這是整個專案最反覆出現的發現，到現在約十五個實例：沒有任何東西是被它自己的單元測試抓到的。 而且分得出兩類，各要靠不同的東西才抓得到。一類是「說明跟實物對不上」：某個欄位寫的，跟它旁邊的資料不符——案例四就是，證據檔說「這是那個陳述」，其實不是。要抓它，得有同一件事的第二份獨立紀錄拿來對；自己跟自己對，永遠是對的。另一類是「你對世界的假設本身錯了」：案例一就是，以為檢查器夠強就擋得住。要抓它，得有別人出的題目；自己出的題，一定落在自己想得到的範圍裡。

一個插曲：最明顯的假證明，它被接受了

上面四個都是「證明成立，別的地方出錯」。這個插曲是另一個方向的，而且它的愚蠢程度值得記下來。

AMPAS 的第三個檢查器 kernel3 是照著 Lean 的型別規則，用 Python 從頭重寫的一個檢查器。把它丟進 Lean Kernel Arena（198 個第三方對抗性測試）之後，其中一個它接受的測試是：

theorem selfProof : (p : Prop) → p := selfProof

定理的值就是它自己。它證明的是「所有命題都成立」，包含 False。所謂「最明顯」是說：它沒有任何技巧可言。它不是證了一個很像的、或者稍微弱一點的命題，也沒有做任何微妙的語意替換——它就是把「請提出證明」這個要求，用「我已經證過了」回答掉。任何人要騙一個檢查器，第一個會試的就是這招，而它也應該是第一個被擋下來的。

Lean 拒絕它的理由是結構性的：Lean 是檢查完才把宣告加進環境，所以那個自我引用是個未知常數。kernel3 的讀檔程式先加再檢查，那個常數就找得到了。一個先查帳還是先入帳的差別：Lean 是查完才入帳，kernel3 是先入帳才查。就這一個順序，決定了「拒絕最明顯的假證明」跟「接受它」。

更值得記的是我自己寫下來的那句話。docs/ARENA-RESULT.md 裡將這個測試歸類為「outside what kernel3 checks rather than bugs in it」——也就是「這不是 bug，是我們的範圍邊界」。那是對自己範圍邊界的高估。 它就是一個缺掉的檢查，而且讀一下宣告就能判定。

修法是加兩條規則。但新增規則有個風險：它可能把正常的宣告也誤判成有問題，那就會擋到真正的工作。所以先拿 Lean 標準函式庫跟 Mathlib（目前最大的形式化數學庫）裡的 3849 筆真實宣告跑一遍——這些都是 Lean 自己接受過的、正常的東西。結果 0 筆被誤判。要是有哪怕一筆被誤判，那表示我的規則寫錯了，而不是 Lean 錯了。文件裡那句話被就地撤回：原句留著，旁邊註明它被收回了，而不是把它刪掉當沒發生過。讓人看得到一個主張被收回，比讓他某天發現它不見了重要。

這兩輪的進度

兩個方向：把機器能檢的那幾層推到極限，以及把人的那一層從「六個布林值」變成「指向具體物件」。

項目	之前	現在
第三個檢查器的專項檢查 每一個只管一種毛病	3 個	5 個。新增兩項：被標記為 unsafe 或 partial 的宣告（Lean 自己說「這條沒照證明的標準檢」），以及宣告本身合不合法
Lean Kernel Arena 誤接受 72 個該被拒絕的測試	28	7
審核勾選欄有機器證據的項目	0 / 6	5 / 6
測試數	451	510

三件事值得說明。

Arena 的 7 不是好成績。 con-leche 跟 lean4lean 各是 0。這個數字是機器算出來、直接寫進記錄檔的，不是我在正文裡自己打的——這樣它就不會在我改句子的時候，被潤得好看一點。剩下的七個是兩類型別規則（不用細究：一類是取出資料結構的欄位時的型別檢查，一類是歸納型別自己的宣告合不合法）——那些是真正的範圍邊界，跟 selfProof 不同。

「5 / 6」裡那個 1 是重點，不是遺漏。 statement_matches_text 被標記為 machine_derivable: false，而且會一直是。有一個測試專門盯著這件事：哪天第六項也冒出了機器證據，它就會失敗。因為那表示有人在那個位置放了一個在回答別的問題的東西。

證據不等於有人讀過。 十三份簽檔全部是在這個工具存在之前簽的，所以 verify 的輸出裡有一個欄位叫 attestations_signed_before_the_evidence_existed，把十三份逐一列名。證據能說明那些勾選是針對什麼而勾的，也能在陳述被改掉時讓驗證失敗；但它不是「有人讀過它」的紀錄。

剩下的工作

做到這裡，剩下的東西分得很乾淨，而第二張表才是重點。

程式還能做的

項目	為什麼是下一個
第三個檢查器兩個已記錄的不完備性	都在拒絕方向（安全的那邊），arena 現在是讓往放寬方向修變得可量測的外部護欄
Arena 剩下的七個	其中五個是真正沒實作的型別規則，比這次兩條規則貴很多
Mathlib build cache	清單上最便宜的一個：把 20 分鐘的 build 變成一次下載
資源上限隨主機縮放	這一輪已經因為記憶體被系統砍掉，產生過一個假的「無法判定」

程式不能做的

這一區現在只剩一項，而它承載了整道忠實度落差：statement_matches_text。它的誠實下一步需要的是人，不是更多自動檢查：

• 回譯（back-translation）。把每個凍結的陳述譯回自然語言，交給一個沒看過 Lean 的人跟原文對。協定很便宜；貴的是那個讀的人。
• 開放審查。現在有一份確認，是由寫這套工具的人以外的人給的——那是原本缺的性質；但那跟「由對結果沒有利害關係的人審查」不是同一件事。
• 別人寫的提交。這個專案裡每一個對抗性測試都是自家寫的，例外是 198 個 arena 測試，跟四組歷史題目（像是梅森質數與歐拉的錯誤猜想，對錯在幾百年前就被別人定了）——而那兩個例外比所有自家寫的加起來都有價值。
• 簽章金鑰與身分的綁定。除了紀錄自己說的以外，沒有任何東西把那把金鑰綁到它的持有人身上。這需要的是倉庫外的行動，不是倉庫內的 commit。

給不做形式化驗證的人

這四個案例走的是 Lean，但形狀不是 Lean 特有的。把「證明」換成「控制測試」、「掃描報告」、「模型評測」，每一個都有對應物：

案例	形式化驗證裡	其他領域裡
一	證明成立，但定理被限制在 n ≤ 3	測試全綠，但測的是縮減過的範圍
二	命題一字未改，定義被換掉	指標名稱未改，分母被改掉
三	最強的檢查器也看不到	工具再貴也解決不了「測的是不是該測的那件事」
四	稽核證據本身就印錯了	儀表板跟底層資料不一致，而人是看儀表板簽核的

三個可以帶走的東西。

第一，工具的強度跟「它回答的是不是你的問題」是兩個軸。 con-leche 帶著機器檢查過的一致性定理，這在「證明成立嗎」那個軸上幾乎是極限。它對 A06 毫無幫助。往極限推進一個軸，對另一個軸一點幫助都沒有。

第二，批次核章跟沒核一樣。 六個全 true 的勾選欄，認真審與不認真審留下的是同一份檔。解法不是增加欄位，是讓每一個勾選指向一個具體、可重算、跟標的物綁定的東西。它不會讓判斷變正確，但會讓草率變得看得見——這是兩件很不同的事，而後者是可以做到的。

第三，沒有任何東西是被它自己的單元測試抓到的。 這是整個專案最反覆的發現，到現在約十五個實例。而且這十五個分得出兩類，兩類要靠完全不同的東西才抓得到：

1. 說明跟實物對不上。 某個欄位寫的，跟它旁邊的資料不符——本文案例四就是：證據檔說「這是那個陳述」，實際上不是。要抓到它，要有同一件事的第二份獨立紀錄拿來對。只有一份紀錄時，它永遠跟自己一致。
2. 你對世界的假設本身錯了。 你以為某件事成立，而它不成立——本文案例一就是：以為檢查器夠強就擋得住。要抓到它，要有別人出的題目。自己出的題，一定落在自己想得到的範圍裡。

兩類的共同點：自己寫的測試只會確認自己的假設。

全部程式、記錄與證據在 github.com/lcat2000/ampas-lean。