LeanMarathon: Multi-Agent Framework for Reliable AI Autoformalization

•LeanMarathon 旨在解決長程自動形式化中的「規模」問題，例如陳述漂移、依賴關係纏結和上下文衰減，這些問題常導致單代理系統失敗。它將脆弱的數小時運行轉化為許多局部、可恢復的平行事務。
•該系統在兩篇2026年的研究論文上進行了評估，成功形式化了涵蓋四個Erdős問題（#1051、#1196、#164、#1217）的七個目標定理，且沒有任何「sorry」（未經證明的斷言），總共證明了258個引理和定理。
•其核心抽象是「演進藍圖」，這是一個動態的Lean文件，同時作為形式證明骨架、自然語言證明圖和共享記錄系統，對於協調四個專業代理（建構、審計、證明和修復）至關重要。
•與商業單代理基準（例如Achim et al., 2025）相比，LeanMarathon在類似任務中表現更優，後者在數十小時後失敗。LeanMarathon能夠將故障定位到單個節點，並防止不正確的早期形式化默默地消耗下游證明器的計算資源。
•這項研究得到了新加坡國家研究基金會和數位發展與資訊部的支持，屬於AI訪問教授計畫（獎項編號AIVP-2024-004）。

📊 競品分析▸ Show

產品/框架	方法	開源/閉源	基準測試/成果	主要特點
LeanMarathon	多代理框架	開源 (GitHub)	成功形式化四個Erdős問題中的七個研究級定理，無「sorry」標記，證明258個引理和定理。	演進藍圖、四種專業代理角色（建構、審計、證明、修復）、兩階段協調器、平行CI門控證明回合。
MA-LoT	多代理框架，基於Lean的長鏈思維 (Long CoT)	未明確說明，但論文在arXiv和Hugging Face上發布	在Lean4版MiniF2F-Test數據集上達到61.07%的準確率，優於GPT-4 (22.95%)、單代理樹搜索 (50.70%) 和整體證明生成 (55.33%) 基線。	結合高層次自然語言推理與形式語言驗證、證明代理與修正代理協作、利用Long CoT中的湧現形式推理能力。
LEAP (Google AI Research)	代理框架，通用基礎模型	未明確說明，但為Google AI Research項目	解決2025年普特南數學競賽所有12個問題；在Lean-IMO-Bench上將通用LLM的一次性形式化解決率從10%以下提升至70%。	模仿人類解決問題方式，將複雜定理分解為互動式引理圖，並利用Lean編譯器的即時反饋。
Prover Agent	AI代理，整合LLM與Lean	開源 (GitHub)	在MiniF2F上達到88.1%的成功率，在PutnamBench上解決25個問題。	協調非正式推理LLM、形式證明模型和Lean的反饋，並生成輔助引理。

核心抽象：演進藍圖，一個Lean文件，同時作為形式證明骨架、自然語言證明圖和共享記錄系統。
代理角色：包含四種合約範圍的代理，分別負責藍圖的建構、審計、證明和修復。
協調器：採用兩階段協調器。
- 第一階段：透過對抗性審查穩定目標保真度。
- 第二階段：以平行CI門控回合的方式，從其動態葉節點向上處理證明有向無環圖 (DAG)。
故障處理：將故障定位到單個節點，防止不正確的早期形式化消耗下游證明器的計算資源，將脆弱的數小時運行轉化為許多局部、可恢復的平行事務。
輸入/輸出：輸入為LaTeX原始碼和單獨的規範目標陳述文件；輸出為一個Lean藍圖，其中每個證明節點都已證明。
程式碼可用性：專案程式碼可在GitHub上公開取得。

AI輔助數學將變得更加可靠並加速大規模研究。

LeanMarathon證明，持久的工具（不僅僅是更強大的證明器）對於在長期數學發展中保持目標保真度至關重要，從而使AI發現的證明值得信賴。

形式化工具如LeanMarathon可能催生新型數學教科書。

Lean證明因其細緻性，可以多種解析度（高層次概述、結構化證明大綱、詳細推導）翻譯成自然語言，同時支持機器檢查和人類理解。

機率性AI生成與確定性形式驗證的結合將成為未來AI系統的標準組成部分。

LeanMarathon展示了大型語言模型在生成（搜索、探索、創造力）方面的優勢，而定理證明器在驗證和正確性方面的優勢，為構建可靠AI提供了強大的協同作用。

2026-06

LeanMarathon論文《LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization》在arXiv上發表。

LeanMarathon：用於可靠 AI 自動形式化的多代理框架