LeanMarathon

A multi-agent harness for carrying long mathematical proofs through Lean formalization.

• Developer / Organization: Yuanhe Zhang, Yuekai Sun, Taiji Suzuki, Jason D. Lee and Fanghui Liu
• Category: Open-source formalization & proving
• Purpose: Carry long research proofs through reliable Lean autoformalization.
• Key features: Long-running, multi-agent Lean formalization organized around a shared proof blueprint.
• Availability: Open-source software; Apache-2.0
• License: Apache-2.0 (source (opens in a new tab))
• Website / Source code: https://github.com/YuanheZ/LeanMarathon (opens in a new tab)
• Version: Source package: 0.1.0 (not a GitHub release)
• Version source: Official release or documentation (opens in a new tab)
• Last checked: 2026-11-01