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

1 Introduction

• A research paper requires many coherent, interdependent Lean declarations, while verifying an entire paper remains largely open beyond isolated goals.Local definition changes can invalidate distant proofs, and formally correct intermediate statements can drift away from the intended theorem.Source: §1 · pp. 1–2
• Machine-checked Lean proofs can establish correctness and support human digestion through explanations at multiple levels of detail.The paper envisions one formal artifact yielding an overview, a structured outline, or a detailed derivation.Source: §1 · p. 2
• Without a trusted fine-grained proof plan, research-level formalization risks goal drift and unproductive subproblems that obscure the target theorem.Unlike textbook settings, the system must discover, maintain, and repair the proof graph itself.Source: §1 · p. 2

1.1 Contributions

• The blueprint is an evolving proof DAG in one Lean file, pairing formal statements with natural-language proofs and dependencies.The system can split oversized nodes or repair misformalized ones rather than freezing its initial decomposition.Source: §1.1 · pp. 2, 4
• Bounded edit scopes and parity checks between prose dependencies and Lean dependencies are designed to contain mistakes and prevent silent drift.Progress relies on deterministic verification and external review rather than an agent's self-assessment.Source: §1.1 · pp. 2–3
• Four contract-scoped agents draft, audit, prove, and repair the blueprint, coordinated by adversarial target review followed by parallel proof of dynamic leaves.Workers handle nodes whose dependencies are proved; deterministic CI gates pull requests before merging.Source: §1.1 · pp. 3–4
• Across two research papers, LeanMarathon formalizes all seven target theorems without sorry, proving 258 lemmas and theorems in total.The cited commercial single-agent baseline fails on both papers after tens of hours.Source: §1.1 · p. 4

1.2 Related Work

• The related work contrasts IMO-level neural proving and research-problem search with paper-level autoformalization, noting commercial systems' harness designs are unavailable.It distinguishes LeanMarathon from AlphaProof Nexus (Tsoukalas et al., 2026) and names AxiomProver, Gauss, and Aristotle as closed-source products (Hariharan et al., 2026; Achim et al., 2025).Source: §1.2 · p. 4

2.1 The Blueprint as the System of Record

• The blueprint is a Lean file serving as formal proof skeleton, natural-language proof graph, and agent task interface, with durable mathematical state stored in it.It records statements, lemmas, definitions, prose explanations, and proof dependencies; agents maintain no hidden shared memory outside it.Source: §2.1 · p. 5

2.2 Contract-Scoped Agents

• Four contract-scoped agents divide blueprint maintenance into narrow interfaces, bounded edit scopes, and distinct failure-detection or containment roles.Every agent produces an externally checkable artifact accepted only through the verifier.Source: §2.2 · pp. 5–6

2.2.1 Blueprinter

• The Blueprinter decomposes the source proof into a faithful, repairable initial blueprint, aiming to minimize declarations changed if one declaration is wrong.It leaves proof bodies as placeholders and isolates mathematical commitments rather than proving the paper.Source: §2.2.1 · p. 6

2.2.2 Target-Reviewer

• The Target-Reviewer checks each target theorem against its canonical statement, blueprint LaTeX, and Lean type for matching mathematical content and hypotheses.It cannot edit the blueprint; a failed review produces a grouped issue for the Refiner.Source: §2.2.2 · p. 6

2.2.3 Per-node Worker

• A Worker audits one proof node, cheaply tests eligible claims for counterexamples, polishes prose, then attempts a proof while its Lean type remains frozen.Its editable region is restricted to the assigned node’s prose and proof body plus local helper lemmas; disjoint worker regions allow patches to commute.Source: §2.2.3 · p. 7
• The Worker may grow a local refinement DAG of fresh helper nodes before its target, which is the unique terminal node.This local growth addresses possible under-decomposition by the Blueprinter or Refiner.Source: §2.2.3 · p. 8

2.2.4 Refiner

• The Refiner identifies the smallest connected sub-DAG needing change, classifies defects as blueprint drift or a source gap, and repairs the affected blueprint region.For a complete proof that no longer compiles, it replaces the body wholesale with a placeholder; Lean, not the agent, decides compilation, and complete proof bodies are never partially edited.Source: §2.2.4 · p. 8

3 System Orchestration

• The orchestration has two stages: adversarially stabilize target fidelity before discharging the proof DAG through parallel, CI-gated attempts.The first stage constructs and audits a faithful blueprint; the second proves it.Source: §3 · p. 9

3.1 Stage 1 – Cold Start and Target Review

• Stage 1 creates an initial Lean blueprint, reviews its theorem nodes against canonical targets, and repeats repair and review until the target review is clean.The Blueprinter’s declarations elaborate with placeholder proof bodies; mismatches or other blueprint defects are grouped for the Refiner after review.Source: §3.1 · p. 9

3.2 Stage 2 – DAG-orchestrated Loop

• Each Stage 2 round extracts the proof DAG from the current main branch and assigns unproved nodes with proved dependencies to independent Workers.Workers share a frozen substrate commit; successful proof PRs and repair PRs pass the same CI gate, and rounds continue until no placeholders remain.Source: §3.2 · p. 9

3.3 Sustaining hours-long runs

• The CI verifier gates merges with structural checks including Lean compilation, well-formed blueprint nodes, and two-way parity between prose citations and Lean proof dependencies.It also checks that the Lean keyword matches the LaTeX environment and that sorry_using references precede the citing node and point only to proof nodes.Source: §3.3 · p. 10
• Lemma closeness requires every lemma to feed a later lemma or target theorem, structurally guarding against orphan lemmas that indicate task drift.The check is mechanical and does not read the mathematics; target theorems may be terminal sinks.Source: §3.3 · pp. 10–11
• The harness enforces agent edit contracts and keeps inter-agent communication in the blueprint and PR/issue stream, preventing out-of-scope patches and hidden shared context.The methodological aim is to turn long-running work into small, recoverable, mechanically checked transactions.Source: §3.3 · p. 11

4 Experiments

• All seven target theorems across four Erdős problems were formalized with complete, sorry-free proofs; 258 lemmas and theorems were discharged in total.Aristotle, the only commercial Lean agent the authors could access, failed on both papers after tens of hours.Source: §4 · p. 11

4.1 Two research papers for evaluation

• The evaluation used two recent research-level papers whose AI-assisted proofs make machine-checked formalization a concrete correctness artifact.The authors selected analytic number theory papers with multi-page estimates rather than competition-style targets.Source: §4.1 · p. 11, §4 · p. 11
• For Erdős–Graham, the formalization extends beyond the easy #1051 instance to a general weighted-series irrationality theorem and a rational construction theorem.The first uses a growth threshold, Mahler’s criterion, local-peak selection, and three-regime tail analysis; the second uses a non-constructive nested-interval covering argument.Source: §4.1 · p. 12
• The primitive-sets paper applies von Mangoldt-weighted Markov chains to target #1196, #164, and #1217, including a conjecture not previously formalized.Parts of #1196 and #164 had prior formalizations, while #1217 had none.Source: §4.1 · p. 12

4.2 Setup

• The harness was run three times, with agents using Codex GPT-5.5-xhigh, a 258K context, read-only access, and no web access.Source: §4.2 · p. 12
• One run formalized all four Erdős–Graham targets, while the primitive-sets work used a #1196 run followed by a seeded extension adding #164 and #1217.The second primitive-sets repository reused the completed #1196 blueprint and its infrastructure.Source: §4.2 · p. 12
• A run counted as successful only when every blueprint proof node had a complete proof, no sorry or sorry_using remained, and all seven CI checks passed.Source: §4.2 · p. 12

• All seven target theorems received complete, machine-checked proofs in every run, with no sorry, axiom, or native_decide.The three runs proved 258 distinct lemmas and theorems: 111 for Erdős–Graham, 44 for #1196, and 103 more for #164 and #1217.Source: §4.3 · pp. 12–13
• The three runs proved 258 distinct lemmas and theorems, including 103 new lemmas and theorems for #164 and #1217 after reusing 59 #1196 blueprint nodes unchanged.The incremental Prim run reached 14,592 lines over 204 nodes rather than restarting.Source: §4.3 · p. 13
• Compiler feedback exposed false statements, vacuous targets caused by totalization, and missing mathematics, prompting corrections to hypotheses and arguments.Examples included adding a summability hypothesis and recasting a density target in ENNReal; a failed route for eta monotonicity led to the paper’s stochastic-domination argument.Source: §4.3 · p. 13
• The three autonomous runs took 17–19 rounds for Erdős–Graham and #1196, while the largest, #164/#1217, cost $624 in GPT-5.5 API-equivalent tokens.The Erdős–Graham run cost $257 and the #1196 run cost $189; 44 of 58 Erdős–Graham Worker pull requests passed checks and merged.Source: §4.3 · p. 13
• Across the three runs, 135 Worker pull requests merged in batches of up to 16, with no merge conflicts.The pull requests were squash-merged directly to a continuously moving main.Source: §4.3 · p. 13
• A fixed 500K Lean budget made runaway tactic searches fail locally and deterministically instead of stalling a whole build.After the change, the agent relied less on unbounded automation and refactored broad searches into direct order arguments and shared sub-proofs.Source: §4.3 · p. 13

4.4 Case study: Erdős–Graham

• Four target theorems were proved in 19 rounds, while all 16 refinement issues concentrated in Proposition 9’s tail bound and the nested-interval covering lemma.Each accounted for eight issues; no other node blocked, and both were results the baseline left unproven.Source: §4.4 · pp. 13–14
• The Refiner split failed nodes into progressively finer sub-nodes for Workers to discharge bottom-up, correcting blueprint drift along the way.Repairs included a false dyadic tail estimate, a Lean index convention mismatch, and downgrading a strengthened statement to a placeholder rather than leaving an unsound proof.Source: §4.4 · p. 14
• A Worker found that Proposition 9’s Case C could choose a peak that was itself a failure, invalidating the paper’s claimed interval bound.The Refiner weakened the selection lemma to allow a failure at the peak, recovering the conclusion.Source: §4.4 · p. 14

4.5 Case study: #1196

• Over five successive rounds, refinement of #1196 moved from a surface estimate to Dirichlet eta monotonicity, then to Gamma-distribution stochastic domination and a Mellin representation.These facts were absent from Mathlib, so the harness built the probabilistic argument compressed into a sentence in the paper.Source: §4.5 · p. 14
• Workers proved the inserted #1196 leaves in dependency order, closing the original defect seven rounds after it first appeared.Five of six Refiner rounds and six of eight issues targeted this analytic spine; the eta-monotonicity step was the blocker the baseline could not discharge.Source: §4.5 · p. 14

4.6 Case study: #164 and #1217

• The Prim run took 40 rounds and 71 hours of active compute, with #164 proved early and #1217 occupying most of the run.It merged 93 pull requests and cost $624 in GPT-5.5-equivalent tokens; the final nine rounds were Refiner-free.Source: §4.6 · p. 15
• The Refiner recorded 32 illness areas: 26 drift and 6 source-gaps, with drift including unconstraining or totalized statements and source-gaps including a routine calculation, an induction, and Mertens’ theorem invoked as a black box.Source: §4.6 · p. 15
• The #1217 cluster required repeated restructuring of a path-data package before its node stabilized and the run closed.A key node was reopened in 10 rounds; the run later corrected real-versus-ENNReal limsup semantics and supplied remaining analytic bridges.Source: §4.6 · p. 15
• About 62 lines of #1217 paper prose with no intermediate lemmas expanded into roughly 84 blueprint nodes, a sixteen-fold increase in lemma count.A “routine calculation” became about 14 lemmas, while “an induction gives” became a 22-node construction; expansion concentrated where the paper deferred to probability and analysis.Source: §4.6 · p. 16

4.7 Ablation: which design choices matter

• The earlier harness left all four Erdős–Graham target theorems unproven after roughly 12 days, with 26 sorry placeholders and a blueprint restarted about eight times.Its final file had 12,910 lines after filing 137 issues.Source: §4.7 · p. 16
• Giving the Refiner access to the source let it classify defects as drift or source gaps; the revised run closed all 16 issues with seven source-aware repairs in one pass.The source-blind Refiner had invented machinery and moved the blueprint farther from the source proof.Source: §4.7 · p. 16
• Removing the Worker’s physical-line budget stopped size alone from justifying a blocked-node issue and required a concrete defect instead.The new run’s 16 issues all named real defects, while a long proof or missing helper had to be handled through local refinement.Source: §4.7 · p. 16
• The paper attributes the earlier run’s failure to two complementary choices: a source-blind Refiner and a budget-based Worker stopping rule.The authors report that removing both turned the same paper into a fully proven formalization.Source: §4.7 · p. 16

4.8 Baseline: Aristotle

• Aristotle failed on both papers: its Erdős–Graham run left two deep results incomplete, and its #1196 theorem remained a sorry.LeanMarathon closed those gaps autonomously and proved every target without sorry.Source: §4.8 · pp. 16–17

• The experiment attempted to formalize OpenAI’s recent disproof of the Erdős unit-distance conjecture.Source: §4.9 · p. 17
• The run never reached the target: later geometric steps required real number-field objects that the dummy record could not provide.The key step was discharged with placeholder values, so the file type-checked and passed CI without proving the result.Source: §4.9 · p. 17
• The disproof depended on deep algebraic number theory, almost none of which was available in Mathlib.Source: §4.9 · p. 17
• The failure marks a scope boundary: LeanMarathon can organize work, but cannot supply prerequisite results missing from the library.Source: §4.9 · p. 17

• Across two 2026 papers spanning four Erdős problems, LeanMarathon formalized all seven target theorems with no sorry.The harness decomposes work into an evolving proof DAG and contains faults behind four contract-scoped agents and a deterministic CI gate.Source: §5 · p. 17
• LeanMarathon frames long-horizon autoformalization as agent durability, using short, recoverable, parallel transactions instead of one brittle multi-day run.Source: §5 · p. 17
• The authors present the system as a step toward AI co-mathematicians whose long-running work stays legible, recoverable, and verifiable.Source: §5 · p. 17

A Agent Knowledge-Store Layouts

• Each agent runs in an isolated git worktree with a fixed knowledge store and reads nothing outside it.Figures 6–9 show the Blueprinter’s store, the Target-Reviewer’s audit-only store, the Worker’s mechanically constrained editable region, and the Refiner’s proof and issue inputs with scope and refine phases.Source: A Agent Knowledge-Store Layouts · p. 23, Figure 6 · p. 24, Figure 7 · p. 24
• Runtime settings fix each agent’s model, sandbox, and tools; stop hooks keep agents running until delivery is recorded and CI failures are handled.The Target-Reviewer is single-shot and has no hook; the Worker’s hook also accepts an issue as terminal.Source: A Agent Knowledge-Store Layouts · p. 23
• Explicit state and ordered recovery rules resume unfinished work without rerunning passed phases or skipping failed ones.The rules use delivery status and phase states to determine whether to exit, resume, deliver an issue or PR, or start the earliest unstarted phase.Source: A Agent Knowledge-Store Layouts · p. 23
• CI-enforced format contracts distinguish placeholder-only Blueprinter files from complete Worker and Refiner proofs, while Worker contracts enforce editable spans and local refinement.Source: A Agent Knowledge-Store Layouts · p. 23
• Ordered execution phases differ by agent, and the Refiner’s scope phase classifies illness areas as drift or source gaps against the proof file.Source: A Agent Knowledge-Store Layouts · p. 23
• Delivery templates and agent-specific permissions determine who files PRs or issues; just-in-time Mathlib retrieval and on-demand references support the workflows.The Target-Reviewer files only issues, the Worker may file either, and the Blueprinter and Refiner only open PRs.Source: A Agent Knowledge-Store Layouts · p. 23