用多智能体系统实现长时序数学定理形式化，保证推理一致性。
LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization
- 构建动态蓝图作为形式化骨架，支持自然语言与代码同步演化。
- 在4个埃尔德什问题上成功形式化7个定理，证明258个子命题无失败。
- 适合需要高可靠性的长周期数学自动化研究者使用。
长时序数学研究的形式化不仅在难证命题上失败，更在规模上受困：命题漂移、依赖纠缠、上下文衰减、局部修复破坏远端成果。我们提出LeanMarathon，一种用于可靠研究级Lean形式化的多智能体框架。其核心是持续演化的蓝图：一个同时充当形式化证明骨架、自然语言证明图谱和共享记录系统的Lean文件。四个契约范围的智能体分别负责构建、审计、证明与修复该蓝图。它们由两阶段调度器协调：先通过对抗性评审稳定目标保真度，再并行自底向上逐轮释放证明有向无环图（DAG）的叶子节点。该方法将一次脆弱的多小时运行转化为多个可恢复、并行的本地事务。我们在两篇近期论文涵盖的四个埃尔德什问题（#1051, #1196, #164, #1217）上评估，三次自主运行中全部形式化7个目标定理，未出现失败，共证明258个引理与定理。结果表明，可靠的AI数学合作者不仅需更强的证明器，更需能长期维持目标一致性的稳健框架。代码见https://github.com/YuanheZ/LeanMarathon。
原文摘要 · Abstract (English)
Long-horizon autoformalization of research mathematics fails not only at hard lemmas, but at scale: statements drift, dependencies tangle, context decays, and local repairs corrupt distant work. We present LeanMarathon, a multi-agent harness for reliable research-level Lean autoformalization. Its core abstraction is an evolving blueprint: a Lean file that serves simultaneously as formal proof skeleton, natural-language proof graph, and shared system of record. Four contract-scoped agents construct, audit, prove, and repair this blueprint. These agents are coordinated by a two-stage orchestrator that first stabilizes target fidelity through adversarial review and then discharges the proof directed acyclic graph (DAG) from its dynamic leaves upward in parallel CI-gated rounds. LeanMarathon turns one brittle multi-hour run into many local, recoverable, parallel transactions. We evaluate LeanMarathon on two recent research papers spanning four Erdős problems (#1051, #1196, #164, #1217). Across three autonomous runs, it formalizes all seven target theorems with no sorry, proving 258 lemmas and theorems. These results show that reliable AI co-mathematics requires not only stronger provers, but durable harnesses that preserve target fidelity across long mathematical developments. The code can be found at https://github.com/YuanheZ/LeanMarathon.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。