LeanMarathon：以进化蓝图实现长程数学自动形式化
研究级数学自动形式化新框架：LeanMarathon解决长程推理中的系统性问题
研究级数学的自动形式化长期面临一个矛盾：单个困难引理可以攻克，但系统在规模上频频失效——语句含义漂移、依赖关系缠绕、上下文逐渐衰减、局部修复反而破坏全局。近日，arXiv上公布了LeanMarathon，一个专为长程数学自动形式化设计的多智能体框架。其核心是一张“进化蓝图”，一张同时承担形式化证明骨架、自然语言证明图谱和系统共享记录表的Lean文件，以此解决规模化的系统性故障。
进化蓝图解决规模化失败的核心痛点
数学自动形式化的目标是把自然语言描述的数学证明转化为机器可验证的形式化代码，但面对长篇研究论文时，现有方法时常在局部细节上正确、却在整体结构上混乱。LeanMarathon的“进化蓝图”充当了全局一致性锚点：它要求每个步骤的改动都反映在这张共享蓝图上，从而避免语句漂移（相同术语在不同段落含义不一）和依赖缠绕（不同部分对同一引理产生冲突解释）。这种设计让系统不只是修补错误，而是持续构建一个自洽的形式化整体。
四类契约范围智能体分工协作
LeanMarathon框架内部部署了四种按契约范围分工的智能体：
- 构建智能体：负责将数学陈述初步转化为Lean代码，填入蓝图的骨架部分。
- 审计智能体：检查已生成代码的逻辑一致性，标记潜在冲突或缺失的依赖。
- 证明智能体：针对审计发现的空缺或薄弱环节，填充具体的证明步骤。
- 修复智能体：当全局校验或运行测试发现错误时，定位并纠正局部问题，同时确保修正不会破坏蓝图其他部分。
这四类智能体共享同一个“进化蓝图”，每步操作都可回溯。当某个引理证明中途出错，修复智能体不会直接覆盖原有代码，而是先更新蓝图上的依赖关系图，再执行针对性修补，降低“补丁打补丁”导致的全局混乱风险。
自动形式化走向可靠协同的新路径
LeanMarathon的提出背景是人工智能辅助数学研究领域的快速演进。随着像Lean这样的证明助手在数学社区中普及，自动形式化成为沟通人类直觉与机器验证的关键桥梁。LeanMarathon通过多智能体协作和进化蓝图，让长程自动形式化从“单个任务的完成度”转向“系统整体的可维护性”。控制住上下文衰减和连锁修复隐患，形式化过程才有可能真正匹配研究级数学的复杂性与严谨性。
