摘要
针对研究级数学长程自动形式化中出现的语句漂移、依赖纠缠及上下文衰减问题，本文提出 LeanMarathon，一种可靠的多智能体框架。其核心是“演化蓝图”，兼具形式证明骨架与自然语言证明图功能。四个专用智能体负责构建、审计、证明和修复，由两阶段编排器协调，通过对抗性审查稳定目标保真度，并以并行 CI 门控方式自底向上完成证明有向无环图。实验表明，该系统能可靠地形式化复杂定理，证明了持久性架构对长程数学开发的重要性。
AI 推荐理由
论文核心在于多智能体协同的长程任务规划、依赖管理及并行执行策略。
研究机构
Warwick
AIP
University of Michigan
Princeton University
University of Warwick
论文信息