LeanMarathon Autonomously Proves 258 Math Theorems Where Commercial AI Failed

AI systems can now generate plausible-looking proofs for open mathematical problems. But plausible is not the same as correct. When Gemini's Aletheia agent tackled hundreds of Erdős problems, only 6.5% of its candidate solutions were "meaningfully correct." The gap between a convincing natural-language argument and a machine-verified proof is exactly what formal proof assistants like Lean 4 are built to close. The problem is that nobody has been able to automate that closing step at the scale of a full research paper, until now.

LeanMarathon is a new multi-agent harness that takes a research paper's LaTeX source and a set of target theorems, and produces a fully machine-checked Lean 4 formalization with zero sorry placeholders. Across three autonomous runs on two recent analytic number theory papers covering four Erdős problems, it proved all seven target theorems and discharged 258 lemmas and theorems in total. A commercial single-agent baseline, Aristotle, failed on both papers after tens of hours of compute.

Why formalizing a whole paper is so hard

Autoformalization, the task of converting natural-language mathematics into a formal proof language, is well-studied at the level of individual lemmas. Systems like DeepSeek-Prover and Goedel-Prover can close single Lean goals reliably. But a research paper is not a single goal. It may require hundreds of mutually dependent declarations, all of which must remain coherent while an autonomous system repeatedly edits, checks, and repairs a growing codebase.

The paper identifies three failure modes that kill any long-running single-agent approach:

• Goal drift: the agent's intermediate reasoning gradually deviates from the logical path required to prove the target theorem, producing a formally correct but mathematically irrelevant proof graph.
• Lost-in-the-middle: the agent gets trapped in an exponentially growing space of unproductive subproblems and cannot navigate back to the core target.
• Irreversibility: once the work drifts from the target, the agent cannot recover, and the damage compounds across the rest of the proof.

A monolithic agent asked to read the paper, design the formal skeleton, prove the lemmas, diagnose failures, and repair its own mistakes is fragile. The question LeanMarathon addresses is not how to make an LLM prove a single Lean goal, but how to design a system that makes long-horizon formalization legible, recoverable, and resistant to drift.