---
id: 20260606-T0-02
title: "LeanMarathon：通过长跨度自动形式化提升AI可靠性"
title_en: "LeanMarathon Enhances AI Reliability Through Long-Horizon Autoformalization"
url: https://ai.daily.yangsir.net/daily/20260606-T0-02
issue_date: 2026-06-06
publish_date: 2026-06-05T04:00:00.000Z
category: research
source_name: "arXiv cs.AI"
source_url: https://arxiv.org/abs/2606.05400
---

# LeanMarathon：通过长跨度自动形式化提升AI可靠性

研究人员提出LeanMarathon框架，解决数学形式化中的长期依赖问题。该框架采用多智能体架构，解决语句漂移、依赖纠缠、上下文衰减和局部修复破坏远程工作等问题。实验表明，LeanMarathon能够显著提高AI数学证明的可靠性，为构建可靠的AI数学助手提供了新思路。

## English Version

**LeanMarathon Enhances AI Reliability Through Long-Horizon Autoformalization**

Researchers introduced LeanMarathon, a multi-agent framework addressing long-horizon challenges in mathematical autoformalization. It solves issues like statement drift, dependency tangling, and context decay. Experiments show LeanMarathon significantly improves the reliability of AI mathematical proofs, offering a new approach for building reliable AI co-mathematicians.

---

**来源**：[arXiv cs.AI](https://arxiv.org/abs/2606.05400)

**详情页**：https://ai.daily.yangsir.net/daily/20260606-T0-02

---

*智语观潮 · Daily — https://ai.daily.yangsir.net/llms.txt*