形式數學與證明搜尋

formal-math 領域的內容地圖——11 個概念。精選入口；所有領域請見 Home。

Agentic Loops Overtake Bespoke Systems — DeepMind 的基本 Ralph-loop 代理程式隨著 LLM 改進，達到其客製化演化式+AlphaProof 系統的水準；這在形式數學領域證實了苦澀教訓／harness 縮減——但 ProofEvolve 提供了修正：在預算嚴格配平的掃描中，結果恰好相反，只有預算不受限制時，迴圈才勝過客製化系統。驗證器雜訊案例（Stellar Colosseum）：客製化架構比單純呼叫高出 23.7 分，比更強模型低 14 分。OEIS Open（2026-08）再次修正：在客製化系統自身 492 個猜想的 50 美元上限下，三工具迴圈以每次求解成本相同的條件解決 147 個，相較之下該系統解決 44 個；同模型 DeepAgent 消融實驗結果則無差異。應拆開看這些架構：搜尋機制在預算上限下有價值——在獎勵預言機 MCTS 中也位於帕累托前緣，成本還低 32.8%，不過比編譯器回饋迴圈只高 0.9 分；代理式功能則沒有
AI-Driven Formal Proof Search — LLM 撰寫 Lean，編譯器逐步檢查 → 不會幻覺；DeepMind：9/353 個 Erdős + 44/492 個 OEIS 未解問題；以驗證作為人工審查的篩選器。五個分母：ProofEvolve（2026-08）在競賽基準上評分，將資料外洩篩查留給人類；AutoGraphForge 在 Lean 中沒有完成 6,522 個「猜想→形式化→證明」陳述中的任何一個；FrontierMath Erdős：68 個精選未解問題中有 2 個，每個花費 300 美元；OEIS Open 以兩個 Lean 檢查器互有 3 個差異的結果，重新估價其餘問題：147/492 = 30%，花費 50 美元；以及獎勵預言機 MCTS（2026-08），在 MiniF2F 上以相同的 256 次嘗試預算達到 87.1%，少用 32.8% 的 token；其中一項公理稽核推翻了某個證明器在 PutnamBench 上三分之一的「成功」。未形式化分支：Stellar Colosseum 在 300 道 FOCS/STOC/SODA 任務上達到 71.0%——這是模型評分器的判定。以篩選器描述此方法仍有爭議：核心只判定有效性，不判斷可理解性
Automated Conjecturing — 機器數學發現中的生成環節——從 Graffiti 延續 40 年的系統脈絡：根據範例表提出不變量不等式，以及五種常見失敗模式（錯誤／已知／瑣碎／怪物／不良不變量）；新穎性問題則重新表述為可判定的線性規劃：AutoGraphForge 的 559 條關係表可證明候選是否由已知定理推得；經稽核的前 100 個候選中，它產生的 6,522 個倖存項目有 49% 是重新發現，1% 則只是裝飾。人類撰寫的比較於 2026-08 隨 OEIS Open 出現：492 個 OEIS 未解猜想，其中 37% 出自一位多產猜想者，47% 位於完全沒有引用的項目上，而 AI 解決的猜想中約有 40% 是透過反證解決
Evolutionary Proof Search — 針對同一個難題的兩種設計——讓演化式搜尋沿著二元證明判定結果攀升。DeepMind 的 AlphaProof Nexus 以 LLM 評論者的 Elo 評估未完成的草稿（Plackett–Luce/Gibbs、在前 64 名候選池上採用 P-UCB）；Meta AI/UVA 的 ProofEvolve 則直接從核心取得分級適應度——AND-OR 證明 DAG 中經驗證的閉合率 ρ——並跨問題繼承已閉合的子 DAG，形成可持續使用、經 Lean 檢查的綱要程式庫；在相同預算下，平均求解率達到 57.8%，高於 LEAP 的 50.5% 和純 ReAct 迴圈的 25.7%。另有兩個對照案例：反證案例中，梯度免費，繁複的搜尋器反而輸給查找表；以及其機制自身的 OEIS 項目集，在每次求解成本相同的條件下，它解決 44/492，三工具迴圈則解決 147/492；兩代模型之差是混淆因素
FrontierMath Erdős Benchmark — Epoch AI 對 68 道重要未解 Erdős 問題所做的基準測試——由 Thomas Bloom 從 erdosproblems.com 上約 652 道未解問題中精選，以 Lean 形式化（50 道來自 Google 的 Formal Conjectures，18 道由 AI 形式化且尚未經專家審查），由 Lean FRO 的 Comparator 檢查，採用固定的 300 美元／72 小時／單次嘗試協定。預發布版 GPT-6 Astra 得分 3%（2/68；方法論論文按實際價格重新計算後，每次求解花費 218 美元及 247 美元，取代公告中的 222 美元及 172 美元）；GPT-5.6 Sol、GPT-5.5、Claude Fable 5.1 與 Fable 5 的得分皆為 0%。協定外的嘗試花費超過 220,000 美元，達到 5/68；計分測試則花費約 20,000 美元——這是該語料庫首次以固定美元預算衡量開放研究數學，也是最鮮明的形式化成本數據（Erdős 問題 90：18 頁散文、120 萬行 Lean）。該作者的另一項 2026 年基準 OEIS Open，在 492 個未經篩選的未解猜想上以每題 50 美元達到 30% 得分——兩項結果顯示，精選可讓求解率提高約 10 倍
Kernel-Level Proof Auditing — 「Lean harness 回報成功」與「核心證明了定理」之間的差距，以及彌合差距的檢查方式：對每個已編譯證明執行 #print axioms，並將接受範圍限制在 propext/Quot.sound/Classical.choice。語料庫中首次實測較弱管線（編譯 + 原始碼層級 sorry 掃描）的錯誤接受率，是 Vamshi & Yang 2026-08 的研究：在 PutnamBench 上，DeepSeek-Prover-V2-7B 的證明可成功編譯且不含 sorry token，卻因 apply? 錯誤而依賴 sorryAx——整體證明成功中有 4/13 和 8/18；MCTS 下則有 11/27 和 19/44，也就是該模型在該基準上 31–44% 的成功案例。Goedel-Prover-V2-8B 和 Kimina-Prover 在四個基準上皆為零。此現象已在 Lean 4.9.0 中記錄，並確認在 Lean 4.15.0 中仍然存在
Logical vs Intelligible Proof — De Toffoli 與 Duede（2026-09，practitioner-opinion）區分了邏輯上的證明概念——可由不必理解內容的機械程序檢查其演繹有效性，而 Lean 證書恰好符合此定義——以及可理解的概念——數學家能掌握、溝通、連結既有知識並以之為基礎繼續推進的論證。歷史上兩者緊密相連，因為沒有人能在缺少後者的情況下產出前者；AI 將兩者分開。此框架將 OpenAI 的 Navier–Stokes 結果視為「一個答案，而非解答」，而第三項性質既不由核心也不由 LLM 委員會檢查。OEIS Open（2026-08）提供了觀察到的最低成本權宜做法：100 個經核心認證的證明中，唯一以人類可讀方式呈現的內容，是對 Lean 檔案所做的未經認證模型敘述，且沒有報告任何人工檢查
Many-Agent Proof Harnesses — 機器證明的未形式化分支：多代理程式管線以自然語言撰寫研究級證明，並透過 LLM 反證委員會檢查，而不是使用核心。Google 的 Stellar Colosseum（2026-09）是代表案例——從策略探索到區段層級相依 DAG，再到全域驗證，共五個階段；在 TCS-Bench 上得分 71.0%，在 Codeforces 上則有 218/222；同一來源也指出此分支難以取信之處：沒有任何內容經 Lean 驗證，評分者本身也是模型，而相較於直接呼叫 GPT-5.6 Pro 高出的 3.0 分，落在評分者本身的誤差範圍內。對此分支前提最精簡的乾淨測試結果恰好相反（OEIS Open，2026-08）：在經核心驗證的領域中，子代理程式委派、持續記憶與待辦清單，在相同模型和相同 200 美元上限下，分數沒有變化。
The Navier–Stokes AI Claim — OpenAI 第一手公告（2026-09-08，vendor-claim，有爭議）聲稱，一個內部模型「能力顯著強於 GPT-6 Astra」，透過約 10,000 個並行代理程式耗時 88 小時，並由 GPT-6 Astra 再花 17 小時形式化，為 Navier–Stokes 千禧年大獎問題——Clay 表述中的 C 與 D 陳述——得出有限時間奇異性解，並完成 Lean 形式化；僅此問題就有 270 萬則代理程式間訊息和約 1,300 億個輸出 token，所有嘗試問題合計則為 490 萬則／約 3,000 億個 token。這是十多個頁面二手引用的數據之權威來源，也記錄了對強迫／非強迫 Euler 優先權讓予 Alpöge 和 Buckmaster 的讓步，以及尚未驗證之處：此語料庫沒有預印本、沒有獨立 Lean 複查、沒有單一代理程式或代理程式數量基線
OEIS Open Benchmark — Epoch AI 對 492 個未解 OEIS 猜想所做的基準測試，這些猜想以 Lean 形式化；模型必須證明或反證，並由 SafeVerify 檢查核心型別及三公理白名單。Claude Opus 4.8 在 50 美元上限下解決 147/492（30%）——由 Comparator 複查後為 144（29%）——DeepMind 客製化 AlphaProof Nexus 在每次求解成本相近的情況下則為 44/492（9%）。在 100 個猜想的 LITE 子集中，預算為 200 美元時，最佳模型達到 44%。約 40% 的解答是反證。476,000 篇 arXiv 論文，以及採用子代理程式／記憶／待辦清單的 DeepAgent 迴圈，都不會改變分數；求解率則隨支出每增加 10 倍而上升約 10 個百分點，沒有平台期。這是 FrontierMath Erdős 的對照：同一評估器、同一月份、同一核心——此處為 30%，彼處為 3%，原因是分母經挑選而排除了知名問題
Statement Drift — 對錯誤陳述的有效證明：Lean 核心認證的是精化後的定理，卻不會確認該陳述是否符合原意，因此陳述漂移可通過每項公理檢查。四種途徑：形式化錯誤（ShadowBench：最佳代理程式可編譯 178 道困難問題中的 61.8%，但僅 11.2% 與原意一致）；在佔位符壓力下採取符合編譯器要求的捷徑（FormalFlow：同義反覆別名、空洞見證、將結論直接寫入；被標記的陳述從 1 個增至 63 個，直到阻擋掃描器將數量降為 0）；對抗式重新定義（代理程式群以 local notation 覆寫）；以及忠於官方措辭、卻不符合原問題用意的陳述（Navier–Stokes、Clay 的強迫選項）。防禦方式：比對陳述與可信副本（Comparator）、使用契約加評審（ProofLoom，沒有它時錯誤修復從 1 個增至 6 個）、蘊涵檢查，以及由人類閱讀陳述

衍生項目#

（無）