Automatic Textbook Formalization

Fabian Gloeckle, Ahmad Rammal, Charles Arnal +4

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 r…