LeanMarathon：经长程Lean自动形式化迈向可靠的AI共同数学家

研究数学的长期自动形式化不仅在硬引理上失败，而且在规模上失败：语句漂移、依赖关系混乱、上下文衰减以及本地修复破坏远程工作。我们推出 LeanMarathon，这是一种用于可靠研究级Lean自动化形式化的多智能体工具。其核心抽象是一个不断发展的蓝图：一个Lean文件，同时充当形式证明框架、自然语言证明图和共享记录系统。四名合同范围内的代理构建、审核、证明和修复此蓝图。这些代理由两阶段协调器协调，该协调器首先通过对抗性审查稳定目标保真度，然后在并行 CI 门控轮中从其动态叶向上释放证明有向无环图 (DAG)。 LeanMarathon 将一小时的脆弱跑步转化为许多本地、可恢复的并行事务。我们根据最近两篇涉及四个 Erdős 问题的研究论文（#1051、#1196、#164、#1217）对 LeanMarathon 进行评估。在 3 次自主运行中，它毫无遗憾地形式化了所有 7 个目标定理，证明了 258 个引理和定理。这些结果表明，可靠的人工智能联合数学不仅需要更强大的证明器，还需要耐用的工具，以在长期数学发展过程中保持目标保真度。代码可以在 https://github.com/YuanheZ/LeanMarathon 找到。