# LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization

arXiv: https://arxiv.org/abs/2606.05400 · HTML: https://mlsanity.com/paper/2606.05400/

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- Builds on 29 of its 46 references that are in the map.
- First posted on arXiv 3 Jun 2026.

## Builds on (most cited first, 29 of 29)

- [AlphaEvolve: A coding agent for scientific and algorithmic discovery](https://mlsanity.com/paper/2506.13131/) (2025)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI](https://mlsanity.com/paper/2411.04872/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [Early science acceleration experiments with GPT-5](https://mlsanity.com/paper/2511.16072/) (2025)
- [Semi-Autonomous Mathematics Discovery with Gemini: A Case Study on the ErdHos Problems](https://mlsanity.com/paper/2601.22401/) (2026)
- [Advancing Mathematics Research with AI-Driven Formal Proof Search](https://mlsanity.com/paper/2605.22763/) (2026)
- [AI co-mathematician: Accelerating mathematicians with agentic AI](https://mlsanity.com/paper/2605.06651/) (2026)
- [M2F: Automated Formalization of Mathematical Literature at Scale](https://mlsanity.com/paper/2602.17016/) (2026)
- [The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale](https://mlsanity.com/paper/2512.07087/) (2025)
- [Progress in Formalizing Sphere Packing in Dimension 8](https://mlsanity.com/paper/2604.23468/) (2026)
- [Automatic Textbook Formalization](https://mlsanity.com/paper/2604.03071/) (2026)
- [Towards Formalizing Reinforcement Learning Theory: A Robbins-Siegmund Approach](https://mlsanity.com/paper/2511.03618/) (2025)
- [LeanArchitect: Automating Blueprint Generation for Humans and AI](https://mlsanity.com/paper/2601.22554/) (2026)
- [DAG-Math: Graph-of-Thought Guided Mathematical Reasoning in LLMs](https://mlsanity.com/paper/2510.19842/) (2025)
- [Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral](https://mlsanity.com/paper/2503.19605/) (2025)

## Built on by (most cited first, 12 of 12)

- [A Formalization of the Mean-Field Derivation of the Vlasov Equation](https://mlsanity.com/paper/2607.08986/) (2026)
- [BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints](https://mlsanity.com/paper/2607.28110/) (2026)
- [VALG: An Agentic System for ML Theory Research](https://mlsanity.com/paper/2608.13060/) (2026)
- [FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models](https://mlsanity.com/paper/2608.20153/) (2026)
- [Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science](https://mlsanity.com/paper/2609.15983/) (2026)
- [AutoGraphForge: Towards Automated Graph Theory Discovery](https://mlsanity.com/paper/2609.03478/) (2026)
- [Benign Loss Landscapes Can Coexist with Worst-Case Hardness](https://mlsanity.com/paper/2609.13057/) (2026)
- [Choir: An Open Protocol for Distributed Multi-Agent Autoformalization](https://mlsanity.com/paper/2609.31903/) (2026)
- [ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization](https://mlsanity.com/paper/2609.34960/) (2026)
- [TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science](https://mlsanity.com/paper/2609.35606/) (2026)
- [Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization](https://mlsanity.com/paper/2609.39228/) (2026)
- [AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness](https://mlsanity.com/paper/2610.05367/) (2026)

## Abstract (arXiv)

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 ErdHos 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.