Summary (Overview)

• LeanMarathon is a multi-agent harness for long-horizon autoformalization of research-level mathematics into Lean 4, addressing the challenge of verifying entire research papers rather than isolated lemmas.
• The core abstraction is an evolving blueprint—a single Lean file that serves simultaneously as a formal proof skeleton, a natural-language proof graph, and the shared system of record.
• Four contract-scoped agents (Blueprinter, Target-Reviewer, Worker, Refiner) construct, audit, prove, and repair the blueprint, coordinated by a two-stage orchestrator that separates adversarial target review from parallel proof discharge.
• The harness formalized all seven target theorems across two research papers spanning four Erdős problems (#1051, #1196, #164, #1217), proving 258 lemmas and theorems with no sorry, while the commercial baseline Aristotle failed on both papers.
• Key design principles include: decomposition via a dynamic proof DAG, external/deterministic verification, restricted tool scope for fault containment, and informalizing-while-formalizing to prevent statement drift.

Introduction and Theoretical Foundation

Background

AI-assisted mathematics operates through three interlocking stages (Tao, 2026): proof generation by LLMs, verification via Lean 4, and human digestion. While generation has advanced rapidly (Aletheia, GPT-5), verification has only kept pace on isolated goals. Verifying an entire research paper—where every definition, lemma, and theorem must type-check with no sorry—remains largely open.

The Core Problem: Agent Durability

The limiting factor is not the model's capability on a single goal but its agent durability: whether an autonomous system stays coherent across a multi-hour run, preserves the intended target, calibrates the failure state, and keeps one wrong decision from corrupting the rest of the proof. This differs fundamentally from textbook formalization, which provides fine-grained blueprints; research-level formalization has no such blueprint available in advance.

Key Failure Modes

The paper identifies three failure modes any long-running agent exhibits:

1. Coherence loss: The task is globally coupled (like Sudoku); a monolithic agent turns myopic and "robs one part of the proof to patch another."
2. Self-evaluation bias: Agents asked to evaluate their own output are overly confident.
3. Irreversibility: Once the work drifts from the target, the agent cannot recover, and damage compounds.

Two Pervasive Failure Modes in Practice

• Goal drift: Intermediate reasoning gradually deviates from the logical path, producing a formally correct but irrelevant reasoning graph.
• Lost-in-the-middle: The agent becomes trapped in an exponentially growing space of unproductive subproblems.

Methodology

The Blueprint

Each mathematical node in the blueprint is a Lean declaration annotated with structured metadata. A typical proof node has the form:

@[blueprint "lem:weighted-tail-bound"
(statement :=/-- LaTeX statement text -/)
(proof :=/-- LaTeX proof prose with \cref{...} citations -/)
(title :=/-- one-line LaTeX title -/)
(latexEnv := "lemma")]
lemma weighted_tail_bound ... : ... := by
sorry_using [aux_lemma_one, aux_lemma_two]

The proof DAG is formed only from lemma and theorem declarations (definitions are global context). The CI verifier enforces two-way parity between prose citations (\cref edges) and the elaborator's actual dependency edges.

Four Contract-Scoped Agents

Two-Stage Orchestration

• Stage 1: A nested Ralph-Wiggum loop—the Blueprinter creates the initial skeleton, the Target-Reviewer audits it adversarially, and the Refiner repairs any mismatches. This repeats until the target statements are certified faithful.
• Stage 2: Repeatedly extracts the proof DAG, identifies dynamic leaves (unproved nodes whose dependencies are proved), and assigns them to Workers in parallel. All PRs pass through the deterministic CI gate before merging.

Seven CI Checks

1. Lean compilation (no errors beyond sorry warnings)
2. Node well-formedness
3. latexEnv consistency (e.g., lemma ↔ lemma)
4. Label-name normalization
5. Unique labels
6. Proof-dependency parity (two-way, between prose and Lean)
7. Lemma closeness: every lemma must be cited by some later lemma or theorem (no orphan lemmas—a structural guard against goal drift)

Editing Scope Enforcement

Worker edit scope is mechanically enforced via an editing MCP server. The Lean file is partitioned around the target node T into frozen and editable spans:

-- previous node ends here
-- BEGIN editable local refinement area for T
@[blueprint "lem:X" ...]
lemma X ... := by ...
-- END editable local refinement area for T
@[blueprint "lem:T" -- frozen
(statement :=/-- editable -/)
(proof :=/-- editable -/)
(title :=/-- editable -/)
(latexEnv := "lemma")] -- frozen
lemma T ... : ... := by -- frozen
-- editable proof body

Empirical Validation / Results

Main Results

Orchestration Statistics

Key Quantitative Findings

• Incremental development works: Seeding Prim with the #1196 blueprint reused all 59 nodes unchanged and added 145 new nodes.
• Parallel PRs never conflict: 135 Worker PRs landed via direct squash-merge, up to 16 in a single round's batch, with zero merge conflicts.
• Ablation: The earlier harness (source-blind Refiner, line-budget Worker) stalled after ~12 days, 137 issues, and 8 blueprint restarts; the current harness completed in ~3 days with 16 issues and 1 restart.

Three Recurring Issue Types from Formalization

1. Compiler refutes false statements: e.g., a tail estimate collapsing to $1 \leq 0$ (issue #431) or $4/3 \leq 2/3$ (issue #465).
2. Mathlib totalization conventions expose vacuous targets: a non-summable real tsum is defined to be 0, hiding missing summability until a Summable hypothesis was added (issue #2); a real limsup of unbounded count returns 0, so the density target was recast in ENNReal (issue #102).
3. Failed tactic probes locate missing mathematics: positivity of the Dirichlet eta derivative led to the need for stochastic domination of Gamma laws (issues #16, #20).

Case Study: Erdős–Graham Gaps

The run caught a genuine gap in the published proof. In Case C of Proposition 9, the paper picks a Borel peak $R$ and the largest exponential failure $P < R$ beneath it, then uses $a_n \geq e^n$ throughout $[P+1, R+1]$. But the peak condition bounds only $a_{R+1}$, not $a_R$, and Case C explicitly permits $a_R < e^{R}$. A Worker flagged the unjustified step (issue #469) and the Refiner repaired it by weakening the selection lemma (PR #473).

Case Study: #1217 – The Hardest Run

The Prim run took 40 rounds, 93 PRs, 46 issues, and 74 hours of active compute. The #1217 proof occupies ~62 lines of paper prose but required ~84 nodes in Lean—a sixteen-fold expansion. The phrase "an induction gives" became a 22-node construction of the probability space and its occupation measure. The single "routine calculation" for the von Mangoldt weight became about 14 explicit lemmas.

Ablation: Design Choices That Matter

Baseline: Aristotle

Failure Case: Unit-Distance Disproof

The harness failed on OpenAI's unit-distance disproof because the required algebraic number theory is largely absent from Mathlib. The Blueprinter resorted to modeling a number field as a dummy record with placeholder values, type-checking but proving nothing real. This reveals a scope boundary: when the hardest part lives in prerequisites the library lacks, the harness can organize but not fill the missing results.

Theoretical and Practical Implications

Theoretical Contributions

• Agent durability as a bottleneck: The paper reframes long-horizon autoformalization as a system-design problem, not just a model-capability problem.
• The dynamic proof DAG: A novel formulation where the decomposition is never frozen but evolves through splitting and repair, discharged bottom-up from dynamic leaves.
• Structural CI checks: The six-point CI contract (including lemma closeness) provides a mechanical, deterministic guard against goal drift without reading mathematics.

Practical Implications

• Fault containment: The four-agent design with bounded edit scopes ensures the worst outcome of any misbehaving agent is a rejected patch, not a poisoned PR.
• Incremental development: The harness supports extending a finished formalization to new targets (as demonstrated by the Prim run), enabling long-term knowledge accumulation.
• Formalization feedback: The Lean compiler provides ground-truth mathematical signal that sharpens the mathematics itself—catching false statements, exposing vacuous targets, and driving the Refiner to the paper's actual argument.
• Human-readable artifacts: Keeping LaTeX prose beside Lean types maintains human readability and guards against drift.

Conclusion

LeanMarathon demonstrates that reliable AI co-mathematics requires not just stronger provers but durable harnesses that preserve target fidelity across long mathematical developments. The system turns one brittle multi-day run into many short, recoverable, parallel transactions, formalizing all seven target theorems across four Erdős problems while a commercial baseline fails.

Future directions implied by the paper include:

• Extending the harness to handle source-gap-heavy papers where the library lacks needed prerequisites.
• Exploring how to supply missing library results automatically.
• Scaling to even larger research papers and more complex proof structures.
• Further improving the orchestration loop with additional CI checks or agent contracts.

The paper's final message is that reliable AI co-mathematics requires not only stronger provers but durable harnesses that preserve target fidelity across long mathematical developments—a lesson that applies broadly to autonomous AI systems working on tasks that span hours or days.