資料來源#
摘要#
一個證明助手（互動式定理證明器），其中「定義、定理和證明都是經過機械驗證的程式碼。」證明由一系列策略（基本證明步驟）構建而成；Lean 的編譯器逐一「執行」證明策略，追蹤每一步之後仍待解決的目標，而當編譯器達到沒有待解決目標的狀態時，證明即為正確。Lean 是 AI-Driven Formal Proof Search 和 DeepMind 的 AlphaProof Nexus 的驗證基礎——這個元件將 LLM 的數學推理從容易產生幻覺的散文轉化為可驗證的產物。
為何重要：完美的驗證器#
Lean 是形式化證明搜尋作為 AI 範式能夠運作的原因。它是一個健全的、自動的、逐步驗證器——這使其成為 Karpathy 的 Verifiability Thesis 中最大程度可驗證的領域，也是 agentic 迴圈的理想獎勵/錨定信號。每次編輯後的編譯器錯誤訊息引導下一輪操作，使模型的推理始終錨定於真實基礎（「編譯器回饋在錨定 LLM 推理中的力量」——Agentic Loops Overtake Bespoke Systems）。
sorry 策略#
Lean 的 sorry 策略會立即關閉任何待解決的目標，同時仍通過型別檢查器——作為「證明放在這裡」的佔位符。這使得證明草稿介面成為可能：草稿是一個在證明位置放置 sorry 的 Lean 檔案，而證明一個定理就簡化為生成沒有 sorry（且沒有不允許的公理如 sorryAx）的型別安全程式碼。 SafeVerify 正是強制執行這一點。論文中的失敗分析圍繞 sorry 展開：agent 有時會將核心難點隱藏在重述目標的輔助引理中的單一 sorry 裡，或引用「已確立的」引理（留作 sorry）而這些實際上是幻覺——兩者都被端到端驗證所拒絕。
mathlib 與前沿#
Lean 附帶 mathlib，一個大型社群數學函式庫。論文指出成功案例集中在「組合學、凸優化和數論等領域，這些領域的 Lean 數學函式庫已經成熟，且任務通常可分解為可處理的子目標。」因此 mathlib 的成熟度是 AI 形式化證明搜尋目前能觸及範圍的關鍵門檻——函式庫覆蓋薄弱或需要大量新理論的領域仍然無法觸及。實驗使用 Lean v4.27 在 Docker 沙箱中運行（透過 Pantograph 進行機器對機器互動）。
相關連結#
- AI-Driven Formal Proof Search — Lean 是該範式核心的驗證器
- AlphaProof Nexus — 透過 search_replace 工具加編譯器回饋迴圈驅動 Lean
- The Verifiability Thesis — Lean 是典型的最大程度可驗證領域
- Agentic Loops Overtake Bespoke Systems — Lean 的逐步回饋使簡單迴圈成為可行方案
- Evolutionary Proof Search — Lean 的二元通過/失敗迫使採用 LLM 評審適應度的變通方案
- Google DeepMind — 在研究規模上構建 Lean agent 的實驗室
開放問題#
- mathlib 的成熟度限制了可觸及的前沿。AI 形式化證明搜尋能否作為副產品擴展 mathlib（形式化新理論），從而拓展自身的前沿？
- Lean 是數學的完美驗證器。還有哪些其他領域擁有同樣健全的自動驗證器（相對於僅有如測試或 LLM 評審委員會等帶有雜訊的驗證器）？
資料來源#
Cited by 8
- Agentic Loops Overtake Bespoke Systems
DeepMind's *basic* Ralph-loop agent matched its bespoke evolutionary+AlphaProof system as the LLM improved; the bitter…
- AI-Driven Formal Proof Search
LLM generates Lean, compiler verifies every step → eliminates hallucination; DeepMind resolves 9/353 Erdős + 44/492 OEI…
- AlphaProof Nexus
DeepMind framework for LLM-aided Lean proof generation; four agents (basic→full-featured); proof-sketch + EVOLVE-BLOCK…
- Evolutionary Proof Search
The full-featured agent's mechanism: population DB of proof sketches, Elo via Plackett–Luce/Gibbs, P-UCB selection, LLM…
- Google DeepMind
Google's AI lab; built AlphaProof Nexus; Gemini models, AlphaProof, AlphaEvolve; opens the AI-for-mathematics domain in…
- Entities — People, Orgs, Tools & Projects
Map of Content for all 32 entity pages. See Home for concept domains.
- Open Questions Backlog
_96 pages with open questions, as of 2026-06-14._
- When Does Verification Quality Determine Whether AI Automation Works?
Verification-quality ladder from Lean/formal proof search through software CI and vulnerability reproduction; autonomy…
Related articles
- AlphaProof Nexus
DeepMind framework for LLM-aided Lean proof generation; four agents (basic→full-featured); proof-sketch + EVOLVE-BLOCK…
- Agentic Loops Overtake Bespoke Systems
DeepMind's *basic* Ralph-loop agent matched its bespoke evolutionary+AlphaProof system as the LLM improved; the bitter…
- AI-Driven Formal Proof Search
LLM generates Lean, compiler verifies every step → eliminates hallucination; DeepMind resolves 9/353 Erdős + 44/492 OEI…
- Client-Side Agent Optimization
AgentOpt's framing of developer-controlled agent optimization (model-per-role, budget, routing) as distinct from server…
- Evolutionary Proof Search
The full-featured agent's mechanism: population DB of proof sketches, Elo via Plackett–Luce/Gibbs, P-UCB selection, LLM…