開源通用智能體推理系統，用于形式數學證明：Numina-Lean-Agent

Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics

Numina-Lean-Agent：開源通用智能體推理系統，用于形式數學證明

https://www.researchgate.net/publication/399956619_Numina-Lean-Agent_An_Open_and_General_Agentic_Reasoning_System_for_Formal_Mathematics

摘要

智能體系統近期已成為形式化定理證明的主流范式，通過協調多個模型與工具取得了卓越性能。然而，現有方法通常依賴于任務特定的流水線和經過訓練的形式化證明器，限制了其靈活性與可復現性。本文提出一種新范式：直接使用通用代碼智能體作為形式化數學推理器。該范式基于三點動機：(1) 通用代碼智能體為證明以外的多樣化推理任務提供了自然接口；(2) 僅需更換底層基礎模型（無需訓練）即可提升性能；(3) 通過 MCP（Model-Calling Protocol）可靈活擴展并自主調用專用工具，避免復雜設計。基于此范式，我們提出了 Numina-Lean-Agent，它結合 Claude Code 與 Numina-Lean-MCP，實現與 Lean 的自主交互、相關定理檢索，以及非形式化證明和輔助推理工具的調用。以 Claude Opus 4.5 為基礎模型，Numina-Lean-Agent 成功解決了 Putnam 2025 全部 12 道題目，性能媲美當前最優的閉源系統。除基準測試外，我們還展示了其通用性：通過與數學家協作，成功形式化了 Brascamp–Lieb 定理。我們在 https://github.com/project-numina/numina-lean-agent 開源發布 Numina-Lean-Agent 及所有解決方案。

1. 引言

   形式化定理證明旨在在嚴格定義的邏輯系統（如 Lean (2015) 和 Isabelle (Paulson, 1994)）中構建機器可驗證的數學定理證明。與非形式化數學推理不同，形式化驗證系統提供了自動且可靠地驗證證明正確性的工具，從而為構建可靠推理奠定基礎。早期神經定理證明研究聚焦于開發單模型形式化證明器。早期證明器結合策略預測與顯式搜索方法（如蒙特卡洛樹搜索）來探索證明空間（Lample 等, 2022；Hubert 等, 2025）。為緩解基于搜索方法的效率瓶頸，后續工作探索了整篇證明生成，以直接產出完整證明（Xin 等, 2024）。此后，其他研究引入非形式化推理以指導策略生成與證明構造（Wang 等, 2025；Ren 等, 2025）。盡管取得顯著進展，在形式化系統中有效捕捉長程、結構化推理仍是核心挑戰。

近期，若干系統超越了單模型形式化證明器，引入智能體工作流，使證明器能與形式化定理證明環境及其他模型交互。例如，HILBERT（Varambally 等, 2025）提出一個智能體框架，將非形式化推理器與形式化證明器結合以引導證明構造。同時，Seed-Prover 1.5（Chen 等, 2025）通過大規模智能體強化學習訓練形式化證明器，強調與 Lean 編譯器及相關工具的反復交互。此外，Axiom Math 團隊開發的 AxiomProver（Axiom Math Team, 2025）采用自主多智能體集成架構，在 Putnam-2025 上取得滿分成績。這些系統凸顯了智能體證明系統的日益有效性。然而，盡管性能強大，現有智能體證明系統仍存在若干局限：(1) 依賴于顯式設計的任務特定推理流水線，且常與大量訓練的形式化證明器耦合，限制了其向新工具或領域的擴展能力；(2) 大多數系統為閉源，且實現細節有限，使社區難以復現和拓展其工作。

本文提出一種基于通用代碼智能體構建形式化數學推理器的新范式，其動機有三：(1) 代碼智能體為證明之外的多樣化證明工程任務提供了原生接口；(2) 可靈活替換底層基礎模型以增強推理能力，無需任何訓練；(3) 集成 MCP 支持即插即用式擴展專用推理工具，模型可根據具體查詢自主調用它們。遵循此范式，我們提出 Numina-Lean-Agent，由 Claude Code 與 Numina-Lean-MCP 組成，提供多樣化的推理工具。具體而言，Numina-Lean-MCP 集成了多個核心組件：包括 Lean-LSP-MCP（Dressler, 2025）用于與 Lean 定理證明器進行智能體交互；為提供相關背景知識，我們開發了 LeanDex，用于從 mathlib 等 Lean 庫中語義檢索相關定理與定義；采用 Informal Prover（Huang & Yang, 2025）生成詳細的非形式化證明方案；并引入 Discussion Partner 工具，可查詢外部語言模型以輔助推理與規劃。這些組件共同使 Numina-Lean-Agent 成為一個通用而強大的形式化數學推理系統。

以 Claude Opus 4.5（Anthropic, 2025）為基礎模型，Numina-Lean-Agent 成功解決了 Putnam 2025 全部 12 道題目，達到當前最先進水平，結果與閉源系統 AxiomProver 持平，并比 Harmonic 的 Aristotle（Achim 等, 2025）多解決兩題。我們在第 3 節報告了所有解決方案及其計算成本與證明長度。值得注意的是，在某些題目（如 Problem-B1）上，Numina-Lean-Agent 生成的證明顯著比 AxiomProver 和 Seed-Prover 1.5 更簡潔。除標準自動證明外，Numina-Lean-Agent 還可作為通用數學推理系統，支持數學家進行交互式的“直覺式證明”（vibe proving）。我們通過與人類專家合作形式化 Brascamp-Lieb 定理來演示這一范式，交互過程的細節見第 4 節。

1. Numina-Lean-Agent

2.1 概述
如圖1所示，Numina-Lean-Agent 是一個基于 Claude Code 與 Numina-Lean-MCP 構建的智能體形式化定理證明框架。作為自主智能體，它能夠動態選擇并調用 Numina-Lean-MCP 中的適當推理工具，以應對多樣化查詢并完成復雜的形式化推理任務。

2.2 Numina-Lean-MCP

Lean-LSP-MCP：Lean-LSP-MCP（Dressler, 2025）是一個專為 Lean 定理證明器設計的模型上下文協議（MCP）服務器。它通過語言服務器協議（LSP）在大語言模型與 Lean 內核之間架起橋梁，賦予模型深入理解、分析和操作 Lean 項目的能力。其工具集分為三個維度，顯著增強模型的證明能力：

1. 語義感知與交互：此維度提供一系列工具，使智能體能模擬熟練 Lean 用戶的行為。從用于把握全局結構的lean file outline，到用于精確查詢目標的lean goal，再到用于獲取權威驗證結果的lean diagnostic messages，這些工具使模型擺脫對證明狀態的猜測，實現基于真實編譯環境的精準決策。
2. 代碼執行與策略探索：支持通過lean run code即時編譯孤立代碼片段，并利用lean multi attempt在單個證明節點上并行執行和評估多種策略。該機制建立了“嘗試–反饋–優化”的閉環，為自動定理證明提供穩健支持。
3. 定理檢索與知識增強：集成多層級搜索工具，有效緩解幻覺問題。lean local search聚焦于本地 Lean 項目與標準庫（stdlib）內定義的挖掘；lean loogle則支持通過自然語言或結構化查詢在龐大的 Mathlib 倉庫中進行搜索。這種雙重檢索機制確保模型所引用的每一條定理均真實存在且語境恰當。

LeanDex：我們提出一款新的 Lean 定理搜索工具，支持在 Lean v4.26.0 環境下進行定理檢索。與現有工具相比，loogle對搜索查詢格式要求嚴格，而本地搜索主要局限于項目內部。LeanDex 是一款面向智能體的語義搜索工具，可跨多個包（包括 mathlib 和 FLT）檢索數學定理與定義。給定自然語言查詢后，LeanDex 會調用智能體解釋并推理查詢意圖，識別最相關的 Lean 對象。該工具基于 LeanExplore 構建，在底層語義搜索框架基礎上增強了推理與檢索能力，顯著提升了靈活性與覆蓋范圍。

非形式化證明器（Informal Prover）：我們實現了一個輕量級的 Gemini IMO 智能體系統（Huang & Yang, 2025）作為非形式化證明器，用于生成詳細的非形式化解題方案。該系統包含兩個模型：生成器（Generator）與驗證器（Verifier）。生成器負責生成非形式化解法，驗證器則評估其正確性。二者通過迭代精煉循環協作：當驗證器發現生成證明中的錯誤時，會向生成器提供反饋；在下一輪迭代中，生成器結合前一版解法與驗證器反饋進行修正。此過程持續進行，直至驗證器接受解法為正確，或達到預設最大迭代次數（我們設定為20次）。

為提升驗證可靠性，驗證器對每個候選解獨立評估三次。僅當三次驗證均判定正確時，該解才被接受。在我們的實現中，生成器與驗證器均使用 Gemini-3-Pro-Preview。

討論伙伴（Discussion Partner）：在科學研究中，討論被廣泛認為是一種高效的認知工具。通過交換不同觀點與推理路徑，研究者常能突破思維盲點、激發新靈感，從而推動問題解決。受此啟發，我們設計并實現了“討論伙伴”工具，旨在輔助自動化形式化過程。

具體而言，該工具賦予 Claude Code 在 Lean 形式化過程中“尋求協助”的能力：當遇到障礙——如證明瓶頸、策略選擇困境或中間引理模糊性——主模型可主動發起與其他大語言模型的討論。這些協作模型從不同推理視角分析當前狀態，提供候選思路或替代證明路徑，給予富有洞察力的反饋。借助這一多模型協同機制，系統能更有效地探索證明空間，顯著提升形式化過程的魯棒性與成功率。

1. 評估

   
   3.1 性能

我們在 Putnam 2025 基準上對 Numina-Lean-Agent 進行了評估，并將其性能與其他現有證明器進行了比較。值得注意的是，我們使用了 Seed-Prover 1.5 提供的形式化題目陳述。此外，我們智能體執行的所有操作均為嚴格串行，未采用任何形式的并行化。所有 API 調用均禁用了互聯網搜索功能，以防止智能體通過在線檢索獲取答案。

在此設置下，Numina-Lean-Agent 取得了當前最先進（state-of-the-art）的性能，成功解決了 Putnam 2025 全部 12 道題目。默認情況下，每道題分配約 50 美元的計算預算。由于問題 A5 的難度顯著更高且證明搜索軌跡更長，其被分配了更大的預算，約為 1000 美元；問題 B6 的預算也相應提高至約 300 美元。這些數值旨在反映相對計算開銷，而非精確的財務核算。

我們針對非形式化證明器（informal_prover）工具的兩種設計范式，在 Putnam 2025 B4 題目上進行了對比實驗。第一種方法采用迭代精煉策略：先生成初始解，再進行驗證，根據反饋進行修正，并重復此循環共 n 輪（Huang & Yang, 2025）。第二種方法采用獨立采樣策略：獨立生成 n 個解，并分別對每個解進行驗證。為確保公平比較，兩種方法的總調用次數保持一致。

實驗結果表明，在相同的搜索配置下，迭代精煉策略顯著優于獨立采樣策略。具體而言，獨立采樣在 10 輪內未能完成 B4 的形式化證明，而迭代精煉僅用 5 輪便成功完成了證明，清晰地展示了基于反饋的迭代修正機制在提升證明效率方面的優勢。

此外，我們還提出了一種新的子智能體（subagent-based）方法來解決 A5 問題，其詳細方法將在第 3.2 節中討論。

如表3所示，我們在 Putnam 2025 上對比了 Numina-Lean-Agent 與其他代表性證明器在各題目上的求解時間。盡管 Numina-Lean-Agent 未采用任何并行執行機制，但它在部分題目上展現出顯著的效率優勢，在多個實例上的求解時間短于其他方法。

在表4中，我們進一步比較了不同證明器生成的證明長度。為確保公平比較，我們從最終的 Lean 代碼中移除了所有注釋和空行，并統計剩余的行數。結果表明，與 AxiomProver 和 Seed-Prover 1.5 相比，Numina-Lean-Agent 在大量題目上生成了更短的證明；尤其在 A3、B1 和 B5 題目上，這一優勢尤為顯著。我們注意到，基于步驟（step-based）的證明器在生成極短證明方面具有固有優勢，因此 Numina-Lean-Agent 生成的證明通常比 Aristotle 的更長。然而，在相似設置下與其他智能體證明器相比，Numina-Lean-Agent 在大多數題目上始終能產出更簡潔的形式化證明，展現出其在生成緊湊高效形式化證明方面的有效性。

3.2 Putnam-2025-A5

對于問題 A5，我們采用了一種新穎的子智能體（subagent）機制，將證明分解為若干子目標并獨立求解，有效緩解了上下文過長的問題。我們的經驗觀察表明，當上下文過長時，模型遵循指令的能力顯著下降，難以聚焦于單一證明目標，從而阻礙關鍵子目標的解決。通過引入子智能體并對證明任務進行模塊化，我們能夠大幅緩解這些問題，提升整體證明效率。

A5 的核心在于證明：在所有滿足某特定性質的排列中，交錯排列（alternating permutations）的數量最多。在若干前期實驗中，模型反復卡在這個關鍵引理上。我們推測這一困難源于上下文過長，因此采用了子智能體策略，將該引理從整體證明中隔離出來單獨處理。具體而言，子智能體首先調用 GPT-5.2 生成一個非形式化的提示（hint），然后在該提示的指導下完成相應的形式化工作。此過程可迭代進行，直至該引理被成功形式化。

1. 使用 Numina-Lean-Agent 形式化 Brascamp–Lieb 定理

4.1 藍圖生成

在 Lean 中形式化一個復雜定理是一項具有密集依賴關系的長程任務。當直接要求 Claude Code 證明最終陳述時，它常常采用次優的形式化方案，并陷入局部死胡同。因此，我們引入“藍圖”（blueprint）作為顯式的規劃層，將全局目標分解為一系列可驗證的子目標。

藍圖是一種類似設計文檔的產物，包含：(i) 所需的定義與記號；(ii) 一組經過精心篩選、粒度適中的中間引理；(iii) 最終定理，其證明主要由這些引理組合而成。依賴關系被顯式記錄（例如通過\uses{...}），形成一個有向無環圖（DAG），用于確定證明順序并在搜索過程中減少歧義。

重要的是，藍圖生成是遞歸的，并且緊密耦合于形式化循環，而非一次性預處理步驟。當智能體嘗試在 Lean 中證明引理時，編譯反饋和證明狀態檢查可能揭示某個非形式化步驟存在錯誤、描述不足，或劃分粒度不當。此時，智能體會回溯并精煉藍圖（例如加強假設、重述命題以匹配 Lean 接口，或插入缺失的中間引理），然后基于更新后的計劃繼續形式化。為提升魯棒性，當當前藍圖反復導致瓶頸時，智能體還可調用外部討論模型（如 Gemini）提出替代的分解方案或修復建議。

總體而言，藍圖扮演了高層數學規劃的角色：由更強的數學推理器將困難命題分解為一系列小而可驗證的步驟，而 Claude Code 則專注于將這些步驟轉化為機器可驗證的 Lean 證明。關鍵在于，驗證不僅是終點——Lean 的反饋（如類型類搜索失敗、缺失引理、接口不匹配等）提供了具體信號，用于修正藍圖，從而形成一個閉環的“規劃–形式化–精煉”工作流，穩定地支持長程形式化。

4.2 人機協作

我們為 Numina-Lean-Agent 設計了一種人機協作交互框架，使人類專家能夠通過撰寫提示和修改藍圖與智能體協同工作。本文其中一位作者是數學家，我們基于他于 2025 年 11 月發表的預印本《Effective Brascamp–Lieb Inequalities》（2025）開展了一項協作案例研究。附錄 A.1 展示了該論文主定理的形式化陳述。在此實驗中，一位數學家、一位 Lean 形式化專家與 Numina-Lean-Agent 共同合作，完成了該論文結果的形式化。

在不到兩周的間歇性協作中，兩位人類專家與智能體共同完成了超過 8,000 行 Lean 代碼的形式化。在此過程中，智能體自主引入了約 70 個新定義、引理和定理，展現出其主動擴展形式化庫并參與大規模、持續性形式化工作的能力。目前，人類專家正在對完整 Lean 代碼進行簡化，我們在附錄 A.1 中僅呈現主定理的形式化陳述。

在形式化更復雜的論證時，智能體有時會進一步分解證明，引入比原始藍圖中更細粒度的中間引理。這種行為似乎是一種針對形式化驗證需求的自適應證明分解策略。

此外，與其它專用證明模型相比，我們的智能體不僅限于定理證明，還展現出強大的通用推理能力。對于一個正確性事先未知的形式化命題，傳統方法通常只能并行嘗試證明原命題及其否定。相比之下，在 Brascamp–Lieb 不等式的形式化過程中，我們觀察到智能體能在證明過程中主動推理該命題本身的正確性。當檢測到命題有誤時，它能自主修正該命題。這種在形式化過程中動態檢查并修改問題表述的能力，是以往證明器所不具備的。我們在附錄 A.2 中提供了此類行為的具體示例。

4.3 局限性

有時，我們的系統生成的 Lean 代碼過于冗長或結構欠佳。實踐中，我們主要讓智能體處理兩類不同難度的sorry：

• sorry僅涉及已良好結構化證明中的局部推理時，智能體通常能以高質量代碼填補空缺；
• 但當sorry對應整個引理的完整證明時，盡管智能體通常能達成目標，但生成的代碼往往冗長，不如預期簡潔。

這凸顯了系統的一個局限：雖然能處理復雜證明目標，但在更大或更復雜任務中，生成形式化代碼的可讀性與結構性可能下降。

此外，系統偶爾在類型層面問題上遇到困難，這會顯著拖慢證明進程。例如，有一次智能體完全失敗——并非因為核心數學論證困難，而是由于從Real到NNReal的類型轉換問題。這類類型約束在非形式化數學中很少顯式說明，因此智能體難以自行重建所需結構。在調整證明流程、提前處理類型轉換以使形式化路徑更“類型友好”后，智能體成功完成了剩余證明。此案例突顯了非形式化與形式化證明之間的固有鴻溝，也強調了類型層面要求對自動化推理系統構成的挑戰。

最后，盡管當前智能體在自動定理證明中展現出強大的問題解決能力，但其在功能正確性與形式優雅性之間仍存在明顯差距。雖然智能體生成的證明通常能通過 Lean 編譯器檢查，但經驗豐富的 Mathlib 貢獻者常認為這些證明過于結果導向，依賴冗長且低級的策略腳本。與人類編寫的 Mathlib 代碼相比，這些證明缺乏結構化抽象和對高層模式的慣用表達，在簡潔性、可讀性以及符合 Mathlib 社區規范方面仍有很大提升空間。

原文：https://www.researchgate.net/publication/399956619_Numina-Lean-Agent_An_Open_and_General_Agentic_Reasoning_System_for_Formal_Mathematics