Automatic Textbook Formalization

TL;DR

This paper demonstrates a large-scale, automated formalization of a graduate textbook in algebraic combinatorics into Lean, showcasing significant progress in scale, efficiency, and multi-agent collaboration.

Contribution

It introduces a fully automated, large-scale formalization process of a graduate textbook using AI agents, achieving a new milestone in textbook formalization.

Findings

Formalized over 500 pages of graduate-level algebraic combinatorics into Lean.

Completed the formalization in one week with 30K AI agents working in parallel.

Achieved inference costs comparable to human expert salaries.

Abstract

We present a case study where an automatic AI system formalizes a textbook with more than 500 pages of graduate-level algebraic combinatorics to Lean. The resulting formalization represents a new milestone in textbook formalization scale and proficiency, moving from early results in undergraduate topology and restructuring of existing library content to a full standalone formalization of a graduate textbook. The formalization comprises 130K lines of code and 5900 Lean declarations and was conducted within one week by a total of 30K Claude 4.5 Opus agents collaborating in parallel on a shared code base via version control, simultaneously setting a record in multi-agent software engineering with usable results. The inference cost matches or undercuts what we estimate as the salaries required for a team of human experts, and we expect there is still the potential for large efficiencies to be made without the need for better models. We make our code, the resulting Lean code base and a side-by-side blueprint website available open-source.