Automatic Textbook Formalization
Fabian Gloeckle, Ahmad Rammal, Charles Arnal, Remi Munos, Vivien Cabannes, Gabriel Synnaeve, Amaury Hayat
cs.AI
2026-04-03
A FAIR team ran 30,000 Claude 4.5 Opus agents in parallel to formalize a 500-page graduate algebraic combinatorics textbook into Lean in a week, proving all 340 target theorems for about $100K.
Mathematics has a refereeing crisis. Journal referees rarely have time to verify every line of a proof; in practice they convince themselves the methods are strong enough to imply the main results, and occasionally a wrong proof or even a wrong statement slips through. Proof assistants like Lean collapse all of that trust down to a small, validated kernel: if the machine accepts the proof, the proof is correct.
The catch is that doing this by hand is prohibitively slow. Lean's mathlib has grown to roughly 2.2 million lines, but its growth has stabilized to an approximately linear rate, which raises real questions about scaling a purely human-driven effort. The paper frames two bottlenecks: most textbook-level foundations are still not in any proof assistant, and the time, expertise, and effort to formalize must come down.
The question this work takes on is whether current models and agent orchestration can formalize an entire graduate textbook automatically.
The target is Darij Grinberg's An introduction to algebraic combinatorics, a roughly 500-page graduate text released into the public domain. The choice is deliberate: the material is reachable from what mathlib already provides, but most of it is not yet in mathlib, which keeps the system from merely regurgitating memorized content.
The interesting part is the orchestration. The hard problem in multi-agent systems is coordination: how a swarm works on one codebase consistently instead of tearing it apart. The authors do not invent a clever scheduler. They copy the standard practices of human software engineering:
Together these give what the authors call fearless concurrency, without heavy orchestration logic in the Python layer. Agents split by role: Sketchers write definitions and theorem statements (leaving proofs as a sorry placeholder), Provers fill them in, two kinds of Reviewers cover mathematical correctness and engineering quality, Maintainers work the issue tracker, and Triage, Scan, and Progress agents patrol the codebase.
Over one week, 30,000 Claude 4.5 Opus agents formalized and proved all 340 target theorems and definitions from the textbook.
| Metric | Value |
| Target theorems and definitions | 340 (all proved) |
| Lines of Lean code | 130,000 |
| Lean declarations | 5,900 |
| Lean source files | 52 |
| Runtime | one week |
| Agents total / successful | 30,000 / 3,300 |
| Input / output tokens | 83B / 561M |
| Cost (no caching) | $430K |
| Cost (estimated with caching) | $100K |
| Per page / per target theorem | $200 / $300 |
Cost is the headline the authors push hardest. With prompt caching, the whole textbook came to about $100,000, around $200 a page, which they say already matches or undercuts the salaries of a team of human experts.
This pushes multi-agent software engineering to a new scale of usable output. The more valuable claim is diagnostic: the bottleneck for formalizing the mathematical corpus is no longer a lack of logical reasoning in models but the orchestration of their collective labor.
On orchestration the authors build nothing new, and that is the point. The human toolkit of git, pull requests, merge queues, and issue trackers works for agent swarms too. On cost, $100K finishes work that would take a human team years, and the authors explicitly flag a 3x to 10x further efficiency gain without changing the model. They frame textbook formalization as infrastructure investment that lowers the cost of every future research-level formalization in the field.
For practitioners, this is a clean example of agentic coding reaching the point of delivering large, usable artifacts, with a reusable orchestration pattern that does not depend on any proprietary magic.
The authors are candid about a long list of issues. The cost is an overestimate: the process was iteratively developed, agents did unnecessary work on exercises and cited theorems, and there was no dependency tracking, so they believe the real cost can still fall 3x to 10x. About half of the input tokens were spent on agents that ended up aborted.
Coordination failures were real. An N-partition data type was written independently three times; Bender-Knuth involutions had inconsistent definitions, which caused sustained agent churn. There were also rabbit holes, where agents defied orders and wandered off to prove things mentioned in passing, such as Kasteleyn's formula pulling them into Pfaffians and the FKT algorithm, draining resources from the real targets. A single merge queue became a choke point, and NFS bandwidth caused timeouts.
The sharpest caveat is structural. This is a single textbook, not a controlled experiment, so n=1. All 340 proved means the Lean kernel accepted those proofs, but the kernel only checks that the proofs the agents wrote entail the statements the agents wrote. If a statement was mistranslated from the textbook in the first place, the kernel will not catch it. The authors only spot-checked key statements manually, and they concede that individual theorems may not have been translated faithfully.