Research map / Multi-agent systems and games / LLM agents
Automatic Textbook Formalization
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Case study of a multi-agent Claude 4.5 Opus system that autoformalizes a 500+ page graduate algebraic combinatorics textbook into Lean, covering all 340 target theorems and definitions in one week for about $100K.
Problem
Automatic formalization of full graduate textbooks in Lean requires repository-scale coordination of many agents, which single-agent and bespoke systems do not provide; the paper asks whether multi-agent scaffolds can formalize textbooks at scale and at acceptable cost.
Approach
A multi-agent scaffold that borrows standard software engineering practices (git trunk-based development with short-lived branches, PR review by independent math and engineering reviewer agents, a merge queue keeping main building, and a file-based issue tracker) so that many coding agents can work in parallel on a shared Lean repository.
Key results
- All 340 target theorems and definitions were formalized and proved in about one week of runtime, with around 130K lines and 5,900 declarations at the end.
- Total usage was 83B input tokens and 561M output tokens over 30,046 agents, estimated at about $100K with caching (about $430K without).
- Of agent outcomes, 3,490 agents were merged, while 14,192 returned no PR and 6,120 were aborted, with aborted agents accounting for about half of input tokens.
Surprising findings
- Agents spontaneously pursued proofs of cited theorems and exercises (rabbit holes, e.g. Pfaffians/FKT for domino tilings), diverting resources from targets.
- Tight orchestration produced 'LLM bureaucrats' that documented blockers rather than making progress, while looser orchestration caused duplication and convention mismatches.
Limitations
- Cost estimate is a back-of-envelope calculation since token caching statistics were not logged.
- Statement faithfulness was checked by review agents and spot checks only, not fully verified.
- Early orchestration inefficiencies and iterative development inflate the cost; results come from a single textbook and a single model.
Experimental setup
Datasets: Darij Grinberg algebraic combinatorics textbook (public domain) Lean mathlib
Benchmarks: formalization of 340 target theorems and definitions in the algebraic combinatorics textbook
Metrics: number of target theorems formalized token usage cost in USD agent outcome rates lines of code and declarations
Baselines: single-agent formalization (Claude Code topology case study) Gauss system closed-source two-phase multi-agent scaffold
Builds on: Claude Code mathlib bors bot
Closest papers by meaning
- APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries (ICML 2026 · similarity 0.85)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.84)
- Lean Workbook: A large-scale Lean problem set formalized from natural language math problems (NeurIPS 2024 · similarity 0.83)
- ImProver: Agent-Based Automated Proof Optimization (ICLR 2025 · similarity 0.83)
- Adaptive Self-improvement LLM Agentic System for ML Library Development (ICML 2025 · similarity 0.83)
- Herald: A Natural Language Annotated Lean 4 Dataset (ICLR 2025 · similarity 0.83)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.