Latest / Embodied AI 101 / LeanMarathon: Autonomous Formalization of Math Proofs on Erdős Problems
Transcript
- LeanMarathon: Autonomous Formalization of Math Proofs on Erdős Problems. In recent years the vision of AI-augmented mathematics has taken a big step forward. Large language models (LLMs) like Codex and GPT-4 can now generate long natural-language proofs and even tackle open problems in math. For example, systems like Aletheia have had early successes on famous Erdős problems. But a persistent bottleneck remains: verification. It’s one thing to conjecture a proof in English – it’s another to translate it into a computer-checked formal proof. As Tao has noted, AI-assisted mathematics has three stages – proof generation, verification, and human digestion – and the verification stage has lagged far behind. In particular, automatically formalizing entire research papers (turning every definition, lemma, and theorem into a correct Lean proof script) is still largely unsolved. That’s the gap targeted by LeanMarathon, a new system by Yuanhe Zhang et al. (2026), which orchestrates LLMs and proof tools to autoformalize research-level mathematics over many hours. Long-running autoformalization has proved surprisingly fragile. Unlike textbook exercises, research papers present hundreds of interdependent statements but no detailed blueprint to follow. A single wrong step – a mis-formalized lemma, an unnoticed bad hypothesis, or just stale context – can invalidate hours of work elsewhere in the proof. Zhang et al. point out that the failure modes start resembling software bugs: “statement drift, dependency tangles, context decay”, and repairs that propagate silently. For example, a local change to one definition might make unrelated proofs fail to type-check, or an agent might confidently introduce a wrong lemma that derails the whole project. In short, a monolithic agent (or one big “generate-and-check” loop) tends to stumble in exactly these ways. The LeanMarathon team argues that the central challenge is not proving a single hard lemma, but keeping the whole process coherent over many steps. They identify three key failure modes for a lone agent: (1) coherence loss (patching one part at the expense of another), (2) self-evaluation bias (an LLM overconfidently trusting its own output), and (3) irreversibility (drifting irrevocably from the original goal). No matter how smart the LLM is, one error can snowball unless the system is designed to contain faults. LeanMarathon’s insight is that you can’t rely on one agent to do it all. Instead, the system treats formalization like a long-running engineering project with multiple specialist agents and a centralized process. The core data structure in LeanMarathon is a single Lean file blueprint that simultaneously holds (a) the formal Lean statements and (b) the original natural-language statements from the paper. In effect the blueprint is a dynamic proof DAG: each node corresponds to one statement (definition, lemma, or theorem) and records both its Lean type and the original LaTeX proof snippet. Dependencies between statements (who uses whom) form edges of the DAG. This evolving blueprint is the single source of truth. Crucially, the system never freezes the DAG; it can split nodes or repair incorrect ones on the fly. By growing and refining this proof graph incrementally, the harness can keep track of the whole development. Around this blueprint, LeanMarathon sets up four dedicated AI agents, each with a narrow job and limited scope. As the authors describe, these four contract-scoped agents coordinate to build the blueprint from bottom to top. Their responsibilities are:. Blueprinter: Given the paper’s text and the target theorems, the Blueprinter creates the initial blueprint (the Lean file skeleton). It lays out all the definitions, lemmas, and theorems from the paper with correct Lean statements, but leaves every proof body empty (just a placeholder ). In choosing how to break the content into declarations, it tries to minimize future rework. In practice the Blueprinter follows a published rubric to decompose the argument into pieces, writing the Lean type for each node so it type-checks, and putting a in each proof. Thus we start with a Lean file that compiles (because each is allowed) but has no actual proofs yet. Target Reviewer: This agent audits the Blueprinter’s initial draft for fidelity to the original paper. It looks at each theorem node and checks that the Lean statement actually matches the intended theorem from the source. If it finds a mismatch (say, a hypothesis was dropped or misstated), it files an “issue” in the system for human-like correction. The Target Reviewer does not try to fix anything itself – it simply points out problems in the statements. Worker: Many worker agents work in parallel. Each Worker picks one leaf node of the proof DAG (a theorem whose dependencies are already proved) and tries to fill in the proof. The Worker operates in a frozen environment, meaning it can only edit a bounded region of the Lean file (so it can’t accidentally touch other proofs). It attempts to prove the current goal, using Lean tactics and automation. If it succeeds, it generates a pull request (PR) that replaces the with the actual proof steps. All Worker edits go through the standard Lean compiler (CI) gate to check type correctness. If the PR passes, the node is marked proved; if it fails, that attempt is rejected. Refiner: The Refiner collects remaining issues or stuck nodes that need more complex changes. It can make multi-node edits in one PR. For example, if a Worker hits a fundamental obstacle (like a missing lemma or a flawed hypothesis), the Refiner might split one proof node into two sub-lemmas, or strengthen/modify a statement. Each refiner PR is also checked by CI. This agent bridges gaps that a single lemma fix can’t handle. On top of these agents is a simple orchestrator. It runs in two stages. In Stage 1 it repeatedly loops between the Target Reviewer and the Refiner on the blueprint until all target statements are certified faithful (no purple issues remain). Essentially, it ensures the blueprint’s statements match the paper before diving into proofs. In Stage 2 it repeatedly identifies all “ready” leaves of the proof DAG (those whose prerequisites have been proved) and assigns them to Worker agents in parallel. Each Worker tries to do its small task, and passes the PR through a strict CI verifier. Passing PRs are merged (squash-merged) immediately, in any order, because the system guarantees they touch disjoint parts of the file (so no merge conflicts can occur). Any PR that fails the CI is simply not merged, and the issue goes back to be refined. This two-phase approach effectively turns what would have been a single fragile multi-day run into many short, recoverable runs – a form of fault containment. In sum, LeanMarathon’s architecture enforces a strict “division of labor”: no single agent ever evaluates its own output or touches the entire file. Every proof step must pass an external checker (the Lean compiler) to count. Each agent has a narrow interface: the Blueprinter and Refiner see the natural language, the Worker sees only the Lean skeleton for one node, etc. By design, when one part goes wrong the damage can be contained without silently corrupting unrelated parts. As Zhang et al. put it, instead of chasing an infallible super-agent, the goal is a system of fallible agents with fault containment. In another way of saying it, we get “trusted CI and scoped editing [that] keep local mistakes from poisoning distant work”. Design Principles and Workflow. Underneath this pipeline are a few core principles Zhang et al. emphasize:. Dynamic Decomposition: The system never commits permanently to a single proof outline. The initial DAG may be coarse, and as issues arise, nodes can split into sub-proofs or merge if needed. In LeanMarathon, the blueprint evolves: nodes are refined downwards until each is manageable for a Worker. External Verification: Agents don’t trust themselves. Every change – proof or statement edit – is verified by Lean’s kernel. No agent self-certifies its work. This external CI gate is the final arbiter, so no false positives slip through unchecked. Restricted Scope: Each agent is confined to editing a limited region of the file. For example, a Worker editing one lemma is forbidden (by the orchestrator) from touching other declarations. This ensures that if a Worker goes off-track, at worst its PR is rejected, not that it corrupts another part of the proof. Informal/Formal Parity: The blueprint keeps the original human prose (LaTeX) right alongside the Lean formal text. This “two-column” proof graph means the system can detect drift. The CI even enforces that whenever a dependency changes in Lean, the corresponding natural-language part must also be updated. In effect, the natural proof and the formal proof must stay in lockstep. This guards against the familiar issue where an AI drifts from the intended meaning unnoticed. The four agents each follow a precise “contract” about what they know and what they output. For instance, only the Blueprinter ever sees the paper’s free-form source; the Target-Reviewer sees just the statements; Workers see one node at a time; the Refiner can rewrite multiple related pieces. Each has a limited “knowledge store” of instructions and partial context so that they act predictably and errors stay local. In practice the Blueprinter is guided by a learned rubric on how to chunk the proofs (the authors tune this from worked examples). The Workers use Lean’s automation tactics (via an LLM acting as a code assistant) and the Lean libraries, drawing on a curated skill set. If a Worker cannot solve a piece, it effectively flags that node as “failed”, passing it back for the Refiner to try different approaches. Experiments on Erdős Problems. To test the system, the team chose recent research-level mathematics from two 2026 papers, both focusing on famous Erdős problems in number theory. The first paper (Barreto et al., “Irrationality of rapidly converging series: an Erdős–Graham problem”) contained four target theorems (numbered #1051, #??? etc). The second (Alexeev et al., “Primitive sets and von Mangoldt chains: Erdős Problem #1196 and beyond”) had three theorems (#1196, #164, #1217). In total there were seven target theorems to prove. These papers involve a mix of combinatorics and analysis, and had never before been formalized; in some cases the formal Lean math library (Mathlib) lacked bits of the needed background. The harness was run fully autonomously three times. Each time, the pipeline agents had only the paper text and the target statements (no additional hints). In every run the LLMs used were copies of OpenAI’s Codex (GPT-5.5-xhigh mode) fine-tuned for Lean, spoken of as “GPT-5.5” by the authors. Importantly, the agents had read-only access to the internet (no Googling); they relied on Lean’s existing Mathlib and local recall. Run 1 (Erdős–Graham series paper): In 19 rounds of editing, LeanMarathon formalized all 4 theorems from Barreto et al. The final Lean file was 8513 lines long, with 39 definitions, 106 lemmas, and 5 theorems proved. All proof obligations were discharged: in the final blueprint, no node remained with a. Statistics: 58 Worker tasks were launched, yielding 53 successful PR merges; 7 Refiner edits were made; the system spent 21h 30m total agent time (about 11h critical path) and issued 308 million tokens to the LLM (about $257 in API equivalent cost). Run 2 (Erdős Problem #1196): The Arnold* et al.* paper for Problem #1196 was first run in isolation. This produced 3988 lines total, with 15 definitions, 43 lemmas, and 1 theorem. Again everything was proven: the last file had zero unfinished proofs. It took 17 rounds, 33 Worker tasks (32 merges), 6 Refiners, and ~16h agent time (11h critical) at ~245M tokens ($189). Run 3 (Incremental extension): Next, the authors tested incremental formalization. They took the finished #1196 blueprint from run 2 and added the two new targets #164 and #1217 to the blueprint. Then they reran LeanMarathon. Impressively, it reused all 59 existing nodes unchanged and only needed to add and prove 103 new lemmas for the two new theorems (145 new nodes total). The final file was 14,592 lines (definitions/lemmas up to 15/144/3) and fully proved. This shows LeanMarathon can extend an existing development without restarting. The incremental run took 40 rounds (a larger pool of workers), 111 Worker launches (93 successful merges), 25 Refiners, ~71h agent time (40h critical), and 796M tokens (~$624). In all three runs every target theorem was fully formalized. The system proved 258 distinct lemmas/theorems in total: 111 from the first paper, 44 from #1196, and 103 from #164 & #1217. None of the final branches contained any stubs – unlike prior approaches, LeanMarathon made no shortcuts. Table 2 of the paper (reproduced here) summarizes that result:. | | Erdős–Graham run | #1196 run | #164/#1217 run | |---|---|---|---| | Target theorems proved | 4 | 1 | 2 | | Total Lean lines | 8513 | 3988 | 14592 | | Nodes (defn / lem / thm) | 39 / 106 / 5 | 15 / 43 / 1 | 57 / 144 / 3 | | Proof nodes (lemmas to prove) | 111 | 44 | 147 | | Remaining | 0 | 0 | 0 | | Status | complete | complete | complete |. This is remarkable. Each run was autonomous: no human intervened to fix statements or proofs. When Workers got stuck, they simply left s (which the system refused to accept unless a Refiner fixed them). In practice almost every PR was checked by CI: of 58 Worker PRs in run 1, 44 merged and 14 were rejected, giving feedback to the Refiner. Crucially, parallelism never conflicted: up to 16 Worker PRs were merged simultaneously without a single Git conflict, thanks to the frozen-region design. In short, LeanMarathon converted one brittle multi-hour task into many concurrent micro-tasks. How Formalization Shaped the Math. An unexpected bonus of this process was that the formalization caught and corrected hidden errors or omissions in the papers themselves. Lean’s kernel provides strict logical checks that often caught false statements that human readers might overlook. Zhang et al. report several examples:. In one lemma, a Worker tried to instantiate a tail inequality and ended up with an obvious contradiction ($1\le 0$). The Lean type-checker refused to accept the proof, and that issue forced the Refiner to revise the hypothesis of that lemma. The original human proof had omitted a crucial condition, and the machine now insisted it be restored. In another case, Mathlib’s own conventions exposed a flaw: a non-summable real series is defined to be 0 in Lean, so a bound that was meant to apply to a convergent series erroneously held even for a divergent one. The system caught that too and demanded an extra hypothesis to ensure convergence. When a Worker encountered a complicated analytic statement about the Dirichlet eta function, failed tactic attempts and missing lemmas led the Refiner to the actual argument from the literature (using stochastic domination of Gamma distributions) instead of a false route. In practical terms, the harness “refused to believe” a step that was glossed over in the prose and forced the rigorous fix. Perhaps most strikingly, the system found a real gap in the published proof of one proposition. In “Case C” of Proposition 9, the paper assumed that the largest “peak” in a sequence satisfied an inequality that might not hold. A Worker flagged an unjustified step, and the Refiner had to weaken the selection lemma so that it admitted an extreme case the human paper missed. This adjusted lemma made the entire proof go through rigorously. In the authors’ words, this is exactly the kind of gap that “machine-checked formalization is built to surface.”. These examples show that LeanMarathon did not just mindlessly translate; it improved the mathematics by insisting on logical precision. In effect, the Lean checker served as a theorem-proving Kanban: blocked nodes became issues, and the feedback loop (issue → Refiner → revised proof) ensured mistakes were fixed. This is an important byproduct: even experienced mathematicians sometimes leave hidden assumptions, but the formal process must spell everything out. Comparison to a Single-Agent Baseline. LeanMarathon’s robust performance is all the more impressive beside what a monolithic system achieved. The authors compare to Aristotle (Achim et al., 2025), a commercial AI theorem-prover. They fed Aristotle the same inputs (paper text + targets) and let it run. The results were stark: after >40 hours on the first paper, Aristotle generated 751 lines of Lean but still had two proof placeholders (sorry) left. These two unfinished cases were exactly proposition 9’s tail bound and the nested-interval construction – the “deepest mathematical content” of the paper that even the paper called hard. On the second paper, Aristotle ran >24 hours and only produced a 24-line file with the single theorem still a ; the missing piece was the same challenging inequality about primitive sets. Achim et al. themselves noted that formalizing that part “typically requires a dedicated team effort”. In contrast, LeanMarathon closed exactly those gaps. It proved every target theorem fully, with no left. In concrete terms, Table 6 of the paper shows:. | | Erdős–Graham (Paper 1) | ESS #1196 (Paper 2) | |------------|------------------------|---------------------| | Aristotle ✔️ or not? | 0/3 proven (2 remaining) | 0/1 (1 remaining) | | LeanMarathon ✔️ or not? | 3/3 proven (0 remaining) | 1/1 (0 remaining) |. In sharp terms: Aristotle failed to complete any target, whereas LeanMarathon finished all of them. This head-to-head clearly demonstrates the value of the multi-agent, orchestrated approach. The single-agent system spent a day+ trying to brute-force those hard parts and came up short; LeanMarathon broke the work apart and solved them piece by piece, even leveraging adversarial review to catch mistakes. Limitations. LeanMarathon is powerful, but it has clear limits. The authors report a failure case on a very different problem: OpenAI’s recent disproof of the Erdős unit-distance conjecture. That proof leaned heavily on advanced algebraic number theory not present in the Lean library. The harness tried: without the necessary math, the Blueprinter had no grounded way forward. It ended up inventing a dummy “number field” record and proving something vacuously trivial (just type-checking but meaningless), and then got stuck. The lesson is clear: formalization can only go as far as the underlying library permits. LeanMarathon will contain the work and keep it consistent, but it can’t magically create missing mathematics. When the core prerequisites lie outside the agent’s “distribution” (its prior knowledge and data), the process stalls. This isn’t a flaw in the design so much as a reality check: any autoformalization system needs a sufficiently rich foundation of formalized math to build on. Emerging Impact and Future Directions. LeanMarathon is an exciting step toward reliable AI “co-mathematicians.” It shows that with the right orchestration, LLMs can handle long-horizon formal tasks that would overwhelm a naive approach. Key takeaways for our field:. System design matters. The architecture – multiple agents, blueprint DAG, CI gating – is as crucial as the underlying model. By compartmentalizing work and enforcing checks, errors are contained instead of spreading. This is reminiscent of software engineering best practices (modular testing, code review, CI) applied to theorem proving. Parallelism pays off. Instead of one giant sequential proof attempt, LeanMarathon effectively creates a bank of smaller jobs. Up to 16 tasks ran in parallel without conflict. For complex projects (think formalizing entire textbooks or research libraries), this idea of disjoint parallel proofs could be vital. Incremental formalization is feasible. The success of extending the #1196 results to #164/#1217 shows that we can build on prior work. In practical research, new results often generalize or build on old ones, and LeanMarathon can be rerun in an “incremental mode” on an existing development. Mathematical insight as byproduct. The fact that the formalization surfaced hidden errors suggests a future workflow: write a proof (or generate one with AI), run LeanMarathon, and get back a fully-verified proof plus a list of logical issues to fix. It could become like a meticulous proof assistant/editor that highlights exactly where assumptions were missing or claims were unjustified. How might other researchers use or build on this? Several avenues suggest themselves:. Broader domains. Erdős problems were a proving ground, but one could try LeanMarathon on other math areas (combinatorics, algebraic geometry, etc.) or other provers (Coq, Isabelle) if a similar harness can be built. The blueprint concept is general. Improved models. The runs used GPT-5.5 (Codex); future LLMs (or specialized proof assistants) could cut costs or speed. Also, reinforcement learning could replace some of the rule-based rubric (e.g. the Blueprinter’s decomposition) to optimize workflow. Human-in-the-loop modes. Currently LeanMarathon runs unattended. One could imagine semi-automated modes where mathematicians examine the blueprint or issues between rounds, guiding the agents only when needed. That could combine the AI’s brute rigor with human creativity. Library expansion. The failure case highlights that scaling this approach broadly requires larger libraries of formal math. Community efforts to formalize broad foundations (like Mathlib) will amplify what harnesses like LeanMarathon can achieve. In the bigger picture, LeanMarathon underscores that verifiable mathematics at AI speed is coming within reach. It's not just a more powerful GPT: it’s an AI-engineered system where the interplay of agents, verification, and data structure does the heavy lifting. For robotics and ML researchers, this work is a compelling example of multi-agent orchestration in a complex symbolic task. It shows how to manage extremely long-horizon problems by splitting them into many well-defined sub-agents with pipelined supervision. The techniques – CI checking, scoped editing, adversarial review – may find analogues in other fields where correctness is critical. Zhang et al. have open-sourced LeanMarathon (at ), so it can be further tested and extended. They describe LeanMarathon as a step toward “AI co-mathematicians whose long-running work stays legible, recoverable, and verifiable”. After seeing it tackle real research proofs end-to-end, we may be inclined to agree. References: The summary here is based critically on Zhang et al. (2026) “LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization” and its cited works. Additional context about AI in mathematics comes from Tao’s blog and recent NeurIPS papers on autoformalization.