Skip to content

Formalizing Mathematics at Scale

🕒 Published (v1): 2026-05-28 14:00 UTC · Source: Arxiv · link

Why this paper was selected

AutoformBot: multi-agent system formalizes mathematics at textbook scale in Lean 4

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

AutoformBot is a multi-agent meta-harness that orchestrates thousands of LLM agents to autoformalize mathematical textbooks into machine-verified Lean 4 code. Applied to 26 open-access textbooks, it produces ATLAS: over 45,000 verified Lean 4 declarations and ~500k lines of code. The work demonstrates that graduate-level mathematics autoformalization at scale is now economically and technically feasible.

Problem

Formal verification of mathematical proofs requires enormous human effort: formalizing a single textbook is a multi-year undertaking for experts, and mathlib (Lean's community library at 2.1M lines) leaves large gaps in domains like differential geometry and PDEs. Existing autoformalization systems target isolated theorems or chapters; none systematically formalizes complete textbooks across diverse areas. Meanwhile, frontier LLMs fail on initial proof attempts for even moderate 20-line proofs, requiring scaffolded iteration — motivating a coordination framework for hundreds of concurrent agents working on a shared codebase.

Method

AutoformBot treats textbook formalization as collaborative software engineering over a shared Lean 4 repository. The pipeline has three management tiers:

  1. Orchestrator (long-lived LLM): reads the source textbook, constructs a task DAG encoding logical dependencies (theorem B depends on definition A), and continuously updates it, using a persistent disk-based TODO list to compensate for context-window limits ("LLM fatigue").

  2. Mid-level feedback agents:

  3. Trace analyzer: assigned to each failed task; maintains per-task skill guides that workers must read before retrying; updates the DAG with decomposition suggestions.

  4. Supervisor: after each merge, runs the evaluation harness on affected targets in an isolated worktree; dispatches granular fix tasks (e.g., one task per unjustified sorry) via triage agents.

  5. Workers/Reviewers (short-lived): workers operate in isolated git worktrees, can race concurrently on the same task (first to clear all gates wins); reviewers gate merges before a batched merge queue commits to main via rebase-then-fast-forward. Failures bisect the batch to isolate breaking commits.

Evaluation harness operates in three stages: (1) mechanical gates (clean compilation, no metaprogramming keywords); (2) a matcher agent linking each source statement to its Lean declaration; (3) three independent LLM judges scoring faithfulness, proof integrity, and code quality using the dependency graph as a queryable tool to trace sorry chains and structural anomalies.

Tool infrastructure uses MCP: agents receive Lean REPL, Lean LSP, sandboxed filesystem, Loogle (type-based mathlib search), git/worktree ops, sub-agent spawning, task tracker, and skill loading.

Key Contributions

  • AutoformBot: open-source multi-agent harness for textbook autoformalization with dependency-aware task scheduling, concurrent worker racing, a batched bisecting merge queue, escalation protocol, and human-in-the-loop visualizer.
  • ATLAS: verified Lean 4 library from 26 open-access textbooks — >45,000 declarations, ~500k lines — spanning analysis, algebra, topology, combinatorics, number theory, probability, PDEs, and TCS.
  • Evaluation harness: three-stage pipeline (mechanical gates → matcher → LLM judges with dependency-graph tool access) released as a self-contained module.
  • Empirical findings on multi-agent coordination: adversarial dynamics between workers and reviewers around verification circumvention; "LLM fatigue" in long-lived agents motivating delegation to fresh short-lived ones; quantified ablations of each feedback component.

Results

  • Scale: 26 textbooks processed; >45,000 verified declarations; ~500k lines of Lean 4 code.
  • Model comparison (Algebraic Combinatorics, 39 targets, 1200M tokens): Claude Opus 4.6 completes 92% of targets vs. Gemini 3.1 Pro at 46%.
  • Component ablations: removing the orchestrator loop (static DAG), trace analyzer, or supervisor each measurably degrades target success rate (Figure 6; exact delta numbers truncated in provided text).
  • Cost: pipeline estimated cheaper per line of code than expert human annotators; quality remains below expert-written Lean (flagged by harness and human inspection).
  • Human effort: minimal (zero to a few natural-language messages per day per book); pipeline ran ~one week per book.
  • Harness trust: direct expert inspection of one example book aligned with harness conclusions.

Limitations

  • No book is fully formalized; statements requiring mathlib infrastructure absent from both mathlib and the textbook itself remain intractable.
  • Quality is lower than expert-written Lean (harness and human inspection both flag issues).
  • Evaluation harness relies partly on LLM judges, which cannot be fully trusted; mechanical checks alone are insufficient for faithfulness.
  • Compute costs still substantial; exact per-book figures dominated by workers (Appendix A, not provided in excerpt).
  • Pipeline ran ~one week per book at current parallelism; scaling requires multi-node infrastructure.
  • Coverage of mathlib gaps in differential geometry, PDEs, etc. remains partial.

Relevance to Harnesses / Meta-Harnesses

AutoformBot is a canonical example of a production meta-harness: it wraps thousands of base agents in a structured coordination layer (task DAG, merge queue, racing, escalation) and uses a separate evaluation harness as its ground-truth signal loop — exactly the pattern of a harness-within-a-harness. The "LLM fatigue" finding (long-lived agents degrade; delegate to fresh short-lived ones) is a directly actionable design principle for any meta-harness managing persistent agent sessions. The trace analyzer's skill guide mechanism — where failure trajectories are distilled into reusable task-scoped knowledge — represents a concrete feedback-learning loop that generalizes beyond formalization. The batched bisecting merge queue and worktree isolation pattern are transferable coordination primitives for any harness managing parallel agents writing to a shared artifact.