Automatic Textbook Formalization

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.

Figures (7)

• Figure 1: Progress of the automatic formalization system. Two phases are clearly discernible: continuous code base expansion (including unnecessary rabbit hole content) and cleanup triggered by an update in agent prompts. Each commit represents a separate agent that merges its work into the main branch. At the end, all 340 target theorems and definitions are present and proved.
• Figure 1: Formalization statistics
• Figure 2: Number of agents by type
• Figure 3: Overview of the contents from the source textbook grinberg2025introduction.
• Figure 4: Histograms of agent PR line counts. The histograms show the number of agents that return within a given range of added, removed or net added lines. The multi-agent setup ensures that pull requests are granular and atomic, comprising around 100 lines. Refactorings that reduce the overall code size are rare, but PRs frequently replace code while extending the code base overall.