Automatic Textbook Formalization

Fabian Gloeckle; Ahmad Rammal; Charles Arnal; Remi Munos; Vivien Cabannes; Gabriel Synnaeve; Amaury Hayat

cs.AIApr 3, 2026

Automatic Textbook Formalization

Authors: Fabian Gloeckle, Ahmad Rammal, Charles Arnal, Remi Munos, Vivien Cabannes, Gabriel Synnaeve, Amaury Hayat

Organizations: FAIR, Meta · CERMICS, ENPC, Institut Polytechnique de Paris · Korea Institute for Advanced Study

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 & tables

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.

Panel of Figure 3 — Figure 3: Overview of the contents from the source textbook ( Grinberg, 2025 ) .

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.

Agent Type	Count	In (M)	Out (M)	Total (M)	Avg In (K)	Avg Out (K)	Turns	Avg Turns
Sketcher	85	6	0.0	6	71	0.4	5084	59.8
Prover	8704	25012	194.2	25206	2874	22.3	435471	50.0
Maintainer	6467	44770	277.1	45047	6923	42.9	814363	125.9
Math Reviewer	6797	3759	42.9	3802	553	6.3	147753	21.7
Eng. Reviewer	6805	1542	20.7	1563	227	3.0	86118	12.7
Triage	550	2747	13.1	2760	4994	23.8	68827	125.1

Table 2: Token usage by agent type. See Sections 2.4 and 2.5 for descriptions of the different roles.

Outcome	Count	In (M)	Out (M)	Total (M)	Avg In (K)	Avg Out (K)	Turns	Avg Turns
Merged	3490	16477	96.4	16574	4721	27.6	299143	85.7
Approved	589	1298	7.2	1305	2203	12.2	20832	35.4
Max Revisions	976	6935	46.5	6981	7105	47.7	131609	134.8
Max Iterations	11	101	0.8	102	9216	70.4	1408	128.0
No PR	14192	7448	76.4	7524	525	5.4	259003	18.2
No PR (blocked)	4668	8012	55.8	8068	1716	12.0	146026	31.3

Table 3: Token usage by agent outcome. See Section 3.4 for the taxonomy of agent outcomes.

Figure 5: Agent outcomes over time by amount (left) and proportion (right) of tokens spent. See Section 3.4 for the taxonomy of agent outcomes. The data is averaged over rolling windows of 400 agents and excludes short debugging runs that marginally contributed to the repository. Dotted vertical lines indicate interventions or restarts (typically minor code changes for efficiency and better observability). Detailed token statistics are not available for the first hours of the run. It can be seen that the initial code suffered from performance issues (especially regarding NFS bottlenecks, git worktree timeouts and merge queue congestion), resulting in a large number of tokens spent on aborted agents. Later versions removed these problems, and mainly suffered from issue dependencies as evidenced by a large number of blocked agents. This could be resolved with a targeted intervention of status agents that cleaned up stale issues, analyzed the dependencies and suggested a course of action, resulting in an increased success rate in the latest stage of the run. Note that merged PRs can also exclusively touch issue files, especially in the case of maintainer agents, and hence success rates of close to 100% should be achievable.

Figure 6: Comparing prover and maintainer agents. (a) Net line change statistics on Lean files and coordination files (“other”) for prover and maintainer agents. For readability, the plot uses a symlog axis and Gaussian jitter with

\sigma=0.3

grid units. (b) Histogram of the number of Lean files edited for both agent types. Prover agents work on a single file by design, maintainer agents most frequently, too, but can also conduct large refactorings involving up to 14 files.

Explore similar work

Formalizing Mathematics at Scale
May 28, 2026Ahmad Rammal, Niket Patel, Fabian Gloeckle +5Formal Verification Lean Theorem Proving
1FAIR at Meta · 2CERMICS, ENPC, Institut Polytechnique de Paris · 3New York University +2
M2F: Automated Formalization of Mathematical Literature at Scale
Feb 19, 2026Zichen Wang, Wanli Ma, Zhenyu Ming +3Autoformalization Formal Verification
School of Mathematical Sciences, Peking University · Beijing International Center for Mathematical Research, Peking University · Huawei Technologies +1
Lean-GAP: A Dataset of Formalized Graduate Algebra Problems
May 20, 2026Seewoo Lee, Byung-Hak Hwang, Hyojae Lim +10Mathematical Reasoning Benchmarks Formal Verification
KAIST · Ethereum Foundation

May 28, 2026J/K move · Enter open · S save

Formalizing Mathematics at Scale

Ahmad Rammal, Niket Patel, Fabian Gloeckle, Amaury Hayat+4

1FAIR at Meta · 2CERMICS, ENPC, Institut Polytechnique de Paris · 3New York University+2

Formal Verification Lean Theorem Proving Autoformalization Multi-Agent LLMs

Open paper AskPDF arXiv

We present AutoformBot, a multi-agent system for building an Autoformalized Textbook Library At Scale (Atlas) in Lean 4. AutoformBot orchestrates thousands of LLM agents, equipped with formal verification tools, dependency-aware task scheduling, and collaborative version control, to translate informal textbook prose into machine-checked definitions and proofs. We apply our methods to a corpus of 26 open-access textbooks spanning analysis, algebra, topology, combinatorics, and probability, producing Atlas: a verified library of over 45,000 Lean 4 declarations and 500 thousand lines of code. We release two artifacts: (i) AutoformBot, the open-source multi-agent framework; and (ii) Atlas, the resulting formal library. Our results suggest that autoformalizing the core content of graduate-level mathematics at scale is now economically and technically feasible. This opens the door to the automated verification of both human- and machine-generated mathematics at a research level.

Abstract

Explore similar work

Formalizing Mathematics at Scale

M2F: Automated Formalization of Mathematical Literature at Scale

Lean-GAP: A Dataset of Formalized Graduate Algebra Problems