邏輯式證明與可理解的證明

資料來源#

• Advancing Mathematics Research with AI-Driven Formal Proof Search
• After Math
• OEIS Open: How many conjectures can language models turn into theorems?
• Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing

摘要#

Silvia De Toffoli（IUSS Pavia）與 Eamon Duede（Princeton/Purdue）在一篇客座文章中提出主張。這篇文章刊於 Terence Tao 的部落格，時間在 [[navier-stokes-ai-claim|OpenAI 的 Navier–Stokes 公告]]四天後（After Math，2026-09-12，約 2,000 字，practitioner-opinion）：證明有兩種概念，而本文集的整套驗證機制只處理其中一種：

• 邏輯概念。「現代邏輯以演繹有效性來界定證明，因此證明可以透過一種機械程序檢查，這種程序本身不需要理解數學論證。」他們直言，「Lean 形式化恰好符合這些標準」，因此 Navier–Stokes 的 Lean 形式化是「真正且重要的貢獻：符合邏輯式證明的要求，因而確保了確定性。」
• 可理解概念。數學家也「想知道命題為何為真。這種知識所運用的是數學思想，而他們能夠掌握、向其他專家溝通、連結既有知識，並用來進一步推進研究。」

他們的主張是合取的：「真正的證明同時是邏輯式與可理解的證明」，而「缺少邏輯或可理解概念中的任何一者，都會形成阻礙；真正的證明則能為數學進展開路。」依此觀點，OpenAI 提供的是「答案，而非解答」——他們借用的比喻是 Deep Thought 的 42——而 Clay Mathematics Institute 自己的 Navier–Stokes 頁面也支持他們的看法：證明之所以重要，是「因為證明帶來的不只是確證，也帶來理解。」

這是一種論證，不是測量。這篇文章收錄於此 wiki，是因為它指出一項本文集中沒有任何驗證機制會檢查的性質，也因為它是 2026-09 形式數學批次中唯一一個作者沒有實驗室隸屬關係、也沒有待辯護成果的來源。

為何過去兩種概念相同，如今卻不再如此#

歷史主張是論證的關鍵支柱。De Toffoli 與 Duede 指出，兩種概念之所以「往往混為一談」，背後有個偶然因素：「沒有數學家能在未先掌握若干可分享的關鍵思想之前，產生極其複雜的邏輯證明，而這些思想正是定理成立的原因。」因此，邏輯概念「主要……用來驗證可理解證明的正確性」（他們引用 Burgess 與 De Toffoli 2022——第一作者自我引用）。人類認知就是兩者的連結機制：可理解性不是另一項獨立要求，而是產生證書的先決條件。

「但有了 AI，這兩種概念如今可能大幅分離。我們可能得到脫離任何可理解證明而獨立存在的形式證明。」

他們小心指出這種分離也會雙向發生，而本文集也應記錄相反方向，因為那正是形式化的價值所在：「可理解的數學論證能傳達宏大的想法，卻未能證明結果確實為真。」他們舉了兩個典型例子——Jaffe 與 Quinn（1993）討論 Thurston 對 Haken 三維流形幾何化定理的研究，其中重大洞見若缺乏充分完整的證明，可能成為「阻礙，而非啟發」；以及 Hales 的 Flyspeck 計畫（Hales 等人，2009），其動機在於查核那份可理解、卻無法完整審查的 Kepler 猜想證明是否確實成立。因此，這項主張並非反對形式化，而是說單靠任何一種概念都會形成障礙，而 AI 是第一個能只提供其中一者的事物。

本文集所反駁的內容：篩選器的框架#

AI-Driven Formal Proof Search 建立在 DeepMind 的主張上：「形式驗證可以作為篩選器，判斷哪些證明值得人工審查。」De Toffoli 與 Duede 的區分直接質疑這個框架是否足夠，且值得精確說明：**核心會篩選邏輯有效性，而可理解性不是它能排序的性質。**一份沒有 sorry、公理乾淨的 Lean 目標證明，和一段五行的 mathlib 改寫，對編譯器而言是同一類物件。以篩選器自己的標準來說，「值得人工審查」的對象就是所有成功編譯的內容，而排序依據為零。

這是該頁如今在同一篩選器中記錄的第二個盲點。第一個盲點來自 ProofEvolve，涉及陳述來源——核心能完美分流證明，卻完全不會指出定理是否早已存在於訓練資料庫；此問題最後交由五個 LLM 評審判斷，並從評估集合中剔除 25.6%。第二個盲點是可理解性。兩者形狀相同：核心只回答一個問題，而它沒回答的那些問題，不會因為它回答了那一個就變得容易。

跨越核心與評議會軸線的第三項性質#

Many-Agent Proof Harnesses 將 2026-09 的兩條路線描述為核心對評議會：Lean 接受一個 .lean 檔案；或者由一群 LLM 反證者與全域驗證器接受一份 LaTeX 文件。De Toffoli 與 Duede 的軸線與之正交，而兩條路線都無法妥善處理：

	檢查邏輯有效性	檢查可理解性
Lean 核心	是，且可靠	否——這是其設計使然；檢查「本身不需要理解」
LLM 反證評議會	近似——模型對有效性的看法	否——依然只是模型對有效性的看法
人類審稿人	緩慢，且可能出錯	是——這正是設立此制度要檢驗的性質

對表格左上格的一項補充，新增於 2026-08。「Lean 核心——檢查邏輯有效性，是，且可靠」對核心而言為真，但不會自動適用於代表核心發言的 harness。Kernel-Level Proof Auditing 衡量了這個落差：一個會編譯檔案並在原始碼中搜尋 sorry 字詞的評估伺服器——多數 LLM 證明器論文實際執行的檢查——會接受依賴 sorryAx 的宣告；某個已發布的證明器在 PutnamBench 上，接受率達 31–44%。這並未讓邏輯／可理解軸線移動分毫；核心一直都判斷正確，而較嚴格的問題（#print axioms、三公理白名單）能找回正確答案。但這表示該列應寫成「是，且可靠——前提是你問對問題」。這對本頁很重要，因為此處的論證完全承認邏輯欄位的效力，藉此質疑可理解欄位。這項承認是穩妥的；有時候，對它的呈報卻不然。

評議會路線受到的影響最大。它的產物看起來可理解——自然語言 LaTeX、46 頁與 75 頁的證明草稿——但其驗證器所近似的仍是演繹有效性，而非「掌握、溝通、連結、據以推進」這項性質。寫出文字不等於產生理解，而這條流程中的任何部分都不會針對兩者的差異評分。將核心路線一併考量後，這個領域有兩種機械化的邏輯問題答案，對可理解性則完全沒有任何形式的測量工具。

本文集自身已呈現兩種概念分離的證據#

這個論點沒有經過測量，但 wiki 中已有三個案例，恰好展現它所描述的落差，值得據此解讀：

• **FrontierMath Erdős Benchmark——Erdős 問題 90。**同一個結果有一份 18 頁的自然語言證明，以及一份 120 萬行的 Lean 形式化，由不同團隊產生。數學家閱讀的是其中一項產物；核心接受的是另一項。這是目前最鮮明的例子，說明「證明」如今經常是兩種物件；De Toffoli 與 Duede 指出，只有其中一種能完成這門學科所需的工作。
• **Automated Conjecturing——6,522 個陳述，沒有一個獲得證明。**AutoGraphForge 執行的創新性篩選器證明存活下來的結果無法由一張列有 559 個經典關係的表格推得。這是一項邏輯性質，由線性規劃判定。至於其中任何一個是否有趣——該頁自己的 #oq/now——便是可理解性問題在生成階段的形式，而篩選器無從判斷。
• OEIS Open Benchmark——100 個經認證的證明，由模型敘述。OEIS Open: How many conjectures can language models turn into theorems?（Epoch AI，empirical）附錄 A.1 列出 153 個已解決未解猜想中成本最高的 100 個；文中指出，「數列描述、猜想陳述與證明摘要均由 GPT-5.6 Sol agents 撰寫」，依據是已接受的 Lean 證明、OEIS 條目，以及沙箱化的 Mathlib 原始碼樹存取權。文中沒有報告任何人類對摘要進行查核。因此，這 100 項結果的可理解部分都存在、清晰可讀，卻是未經認證的——它們正是由核心原本被引入以取代的機制產生，並疊加在核心認證過的物件之上。這不是基準測試的缺陷（判定結果不受文字影響），而是本文集中這個落差最具體的形式：理解並非缺席，而是有一個生成的替身；它是否忠實於認證過的產物，唯一的保障只是模型曾看過該檔案。這也提醒我們，解決方法可能長什麼樣：讓形式化本文集變得易讀，最便宜的方法就是讓模型讀回內容，而這個迴圈中沒有任何機制會查核敘述是否就是證明。
• **The Navier–Stokes AI Claim——主張本身。**OpenAI 發布 Lean 形式化主張、手稿、代理程式數量與 token 總數，卻未說明定理成立的原因，也沒有提供數學家可用的解釋。De Toffoli 與 Duede 的判斷刻意保留餘地：「或許我們會發現他們提出了[富有成果的解答]，但目前情況仍遠不明朗。」一週後又浮現第三種落差，與兩種證明概念都正交：Scientific American 報導（Did OpenAI solve the wrong Navier-Stokes problem?，practitioner-opinion，依報導所述）該定理符合 Clay 指定的強迫條件「C」，但不是數學家原本所指的無強迫條件問題。這涉及陳述是否忠於問題，而核心與可理解性都無法處理；請見 The Navier–Stokes AI Claim。

最有力的反證，以及它與質疑的交會之處（2026-09-29 從 AI-Driven Formal Proof Search 移入）。DeepMind 的形式證明搜尋論文（Advancing Mathematics Research with AI-Driven Formal Proof Search）指出，即使代理程式失敗，合作者的理解仍因證明嘗試而提升，因為形式草稿讓專家能聚焦於尚未解決的子目標。這項觀察討論的是合作過程：人類處理未解草稿，並從嘗試中學習。De Toffoli 與 Duede 的質疑討論的是產物：完成的證書，產生過程中沒有人需要理解，而旁人也無從由此推知定理為何成立。兩者可以同時為真。迴圈中的數學家可能受到啟發，輸出結果對迴圈以外的人仍然難以理解。要化解這項張力，需要一個案例證明是成果本身而非合作關係教會領域新知，而兩個來源都沒有這樣的案例。

第二個論點：「解數學題」不等於解決問題#

這篇文章反駁兩項假設，而可理解性區分只能駁倒第一項。第二項是「數學只關乎解決問題」，作者另外加以批判——因為他們承認，「未來的 AI 系統很可能產生既經形式認證、又完全能被數學家理解的真正證明」，屆時第一項論證便不再適用。

他們認為競賽框架從根本上就站不住腳：「沒有贏家……沒有數學將死」，因此 Deep Blue 對 Kasparov 的比較（文章引用 Tristan Buckmaster 的說法）沒有對應的對象。他們認同 Jeremy Avigad 的說法——「AI 不過是一種科技，是為了服務我們的目的而設計……我們開車時，並不是在比誰開得更快」——並引用 Tao 在 2026 年列出的數學目標，指出數學不只解題：發展新理論與技巧、理解世界、維繫社群、培育下一代、累積知識，以及創造具有美學價值的作品。關鍵在於，這些目標過去與真正的解答正相關，而「AI 打破了這種相關性，原因與它拆開兩種證明概念相同。」他們也預先回應顯而易見的反對意見：「這不是移動球門柱，而是承認任何特定的球門柱都不足以代表全貌。」

基準測試化的警訊#

有一句話直接批評評估實務，比起哲學論述，更應收錄於此 wiki：

「如果數學成功逐漸被過度等同於產出經認證的答案，數學就可能為了精確配合那些最容易被基準測試、並被自動化取代的特徵而改變自身。」

這是將 Goodhart 定律的批判對準整個學科，而非單一指標，也是每個經評分的開放問題分母都面臨的長期風險——請見 FrontierMath Erdős Benchmark，其整體貢獻便是為精選開放問題建立固定預算分母。文章指出這項顧慮屬於制度層面，不只是哲學問題：mathandai.org 上一份由最初 25 位 Fields Medallists 簽署的宣言，警告 AI 公司的目標與數學界的目標之間存在「嚴重錯位」。作者自己的診斷也指向學界內部——「數學家需要更仔細檢視自己的規範」——並援引 David Bessis 關於數學的聲望與功勞分配經濟需要重新思考的論點。

證據說明#

practitioner-opinion，而且分級恰當。這篇文章沒有測量、資料或研究流程，作者也沒有聲稱有。它提供的是一項區分與兩種論證——因此它能讓其他頁面的問題更精準，卻幾乎無法定論。處理事實問題時，證據權重應低於本領域任何 empirical 來源；至於它實際有能力回答的問題——一份證書能證明什麼——其權重則高於它所回應的 vendor-claim。

**作者立場與利益衝突。**De Toffoli 研究數學實踐哲學與證明知識論；Duede 研究科學中的 AI 知識論。兩人都沒有實驗室隸屬關係，也沒有待捍衛的研究成果，這正是這個來源罕見且有用之處——本次彙編的六份文件中，只有這一份的作者不是所討論系統的生產者或評分者。另一方面，歷史主張的兩項佐證引文之一（Burgess 與 De Toffoli 2022）出自第一作者之手；發表平台是部落格，而非經同儕審查的刊物；Tao 的介紹附註則指出，文章「最初以另一種檔案格式撰寫，之後使用 AI 轉換」。作者表示「本文的擴充版本將於其他地方刊出」，因此同儕審查版本將是後續觀察觸發點。

延伸閱讀#

• OEIS Open Benchmark——觀察到的、成本最低的落差應對方式：100 個經核心認證的證明，唯一易讀的說明是未經查核、由 GPT-5.6 Sol 對 Lean 檔案所作的敘述。這是可理解性的生成替身，而非可理解性缺席；也是本文集中第一個在一篇其他方面都處理妥當的論文內部呈現此區分的案例

• AI-Driven Formal Proof Search——其組織框架（「以驗證作為篩選器，判斷哪些證明值得人工審查」）正是本文所質疑的對象：篩選器能替邏輯有效性排序，卻看不見可理解性；這是同一篩選器中第二個被指出的盲點

• The Navier–Stokes AI Claim——本文的起因與貫穿全篇的例子；論點是，即使儲存庫毫無問題，也只能證明邏輯層面

• Many-Agent Proof Harnesses——此區分橫跨核心對評議會的軸線；評議會路線能產生文字，卻不會產生理解，也不會針對理解評分

• Automated Conjecturing——生成端也有相同區分：「無法由 559 項關係的表格推得」是創新性的邏輯證書；它留下的有趣性問題，正是證明出現前的可理解性問題

• FrontierMath Erdős Benchmark——本文集中最明確的案例：同一結果以兩種產物存在（18 頁／120 萬行）；也是「最容易被基準測試」警訊所針對的基準測試

• Transformative Creativity——答案與解答的區分，和 Boden 的第二級／第三級區分平行：經認證的答案是在固定空間內找到的搜尋結果；富有成果的解答則會改變其他人工作的空間

• Outsource Your Thinking, Not Your Understanding——軟體領域也指出相同的剩餘問題：機器可以代勞思考，卻無法代替你理解。本文談的是數學中的案例，差別在於形式證書讓理解落差隱形，而非僅僅沒有處理它

• The Verifiability Thesis——數學加 Lean 是該論點的極致案例；本文指出，即使可驗證性達到極致，仍未產生這門學科的核心價值

• Verification as the New Bottleneck (總覽)——在唯一能保證檢查可靠的領域裡，通過檢查仍有哪些事情無法獲得認證

• Lean——本文既精確肯定、也精確界定這項工具：「恰好符合這些標準」，並確保確定性；但證明的用途不只在於確定性

• Terence Tao——本文的主持人，也是第二個論點所依據的數學目標清單來源

• Kernel-Level Proof Auditing——補充本頁「是，且可靠」格子的說明：核心的判定與 harness 對判定的摘要是不同物件，而本文集首次測得的誤接受率正好區分了兩者

• OpenAI——本文所回應公告的提出者

• Statement Drift——介於有效性與可理解性之間的性質：經認證的陳述是否就是原本要問的問題。Navier–Stokes 強迫條件爭議是它在規格層面的案例

• Autonomous Scientific Discovery——Leiden Declaration 現在收錄於此：一份數學家社群對 AI 可能危害「正確性、嚴謹性與證明標準」的聲明，也是此區分在制度層面的對應案例

尚待解答的問題#

• 可理解性究竟能否操作化，還是終究只是哲學家的區分？可證偽的形式是：有沒有人發表一套流程，在數學家閱讀機器產生的證明後，測試他們能否說明定理成立的原因——而不只是查核定理是否為真——又有沒有任何機器證明通過？若沒有這種測量工具，這項區分可以讓主張更精準，卻永遠無法定論。
• 當 AI 產生的開放問題結果同時有文字論證與形式化版本時，究竟哪一項產物承載了理解？形式化版本是否曾改變數學家運用結果的能力？本文集有一個兩者兼具的案例（Erdős 問題 90，18 頁對 120 萬行），但沒有任何地方回答這個問題。
• De Toffoli 與 Duede 承認，第一項論證有其時效：未來系統「很可能產生既經形式認證、又完全能被理解的真正證明」。(觸發事件：首個由機器產生的開放問題解答，並有實際從事數學研究的數學家公開表示它教會了他們結果為何成立——例如評論、綜述或解說文章，而非僅確認正確性。)

資料來源#

• After Math——Silvia De Toffoli（University School for Advanced Studies IUSS Pavia）與 Eamon Duede（Princeton University and Purdue University），〈"After Math"〉，Terence Tao 部落格客座文章（terrytao.wordpress.com），發布於 2026-09-12，約 2,000 字，practitioner-opinion——一篇沒有測量、資料或研究流程的哲學論證；此處採用的分級符合來源內容，完整閱讀也確認如此。這是網頁文章，並非由 PDF 轉換，因此不適用 docling: 表格規則；來源沒有圖片或表格（原始來源註記顯示文章內容區塊沒有任何 <img> 標籤），整理後的正文是以分享工具為界的完整 post-content 元素。保留了三個小節——「Not All Answers Are Solutions」、「You Need More than Solutions to 'Solve Math'」、「Aftermath」——它們在原文以 <b> 標籤模擬標題。 引文採用文內超連結，不另列參考書目，此處依作者的引用方式使用（Thurston 1994；Jaffe 與 Quinn 1993；Hales 等人，2009；Burgess 與 De Toffoli 2022；C. Thi Nguyen 2019；Avigad 2026，刊於 proofsandprompts.com；Tao 2026，arXiv 2608.16753；Clay Institute 的 Navier–Stokes 頁面；Buckmaster 的聲明 PDF；mathandai.org 宣言；David Bessis 的 Substack）。上述文件均未另外擷取——每一項都是關於本文集未收錄文件的主張，並在本文中歸於作者對該文件的解讀。 編輯框架另行處理：開頭的斜體段落是 Tao 本人對客座作者的介紹（結尾為「— T.」），並包含他對文章「最初以另一種檔案格式撰寫，之後使用 AI 轉換」的說明；這段不屬於客座文章的論證，只作為主持人的框架引用。
• OEIS Open: How many conjectures can language models turn into theorems?——Tom Adamczewski（Epoch AI），arXiv 2608.11941，2026-08-12，27 頁，empirical。此處只引用一個句子，出自附錄 A.1 前言，並根據 pdftotext -layout 輸出的文字核對原文：表 1 的數列描述、猜想陳述與證明摘要「是由 GPT-5.6 Sol agents 根據已接受的 Lean 證明、該數列的 OEIS 條目，以及沙箱化的 Mathlib 原始碼樹存取權撰寫」。論文沒有提出可理解性主張，也未討論此區分——這是本 wiki 的解讀。本文未引用任何單一表格列。完整分析見 OEIS Open Benchmark
• Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing——Vamshi 與 Yang（University of Maryland），arXiv 2608.28639，2026-08-11，empirical。此處只引用一項對上方表格核心欄位的補充——核心判定與「編譯加 sorry 掃描」harness 摘要之間測得的落差。此文沒有討論可理解性，其數據也與本頁主題無關。完整分析見 Kernel-Level Proof Auditing
• Advancing Mathematics Research with AI-Driven Formal Proof Search——Google DeepMind（AlphaProof Nexus，arXiv 2605.22763）。此處僅引用合作者的報告：即使證明嘗試失敗，仍能加深他們的理解。