Lean-GAP: A Dataset of Formalized Graduate Algebra Problems
For researchers in automated theorem proving and formal mathematics, this provides a structured benchmark and methodology, though the contribution is incremental.
The authors created Lean-GAP, a dataset of 430 formalized graduate-level algebra problems from a standard textbook, using a semi-automated pipeline. They found that verification of formal-informal correspondence remains the most labor-intensive step, requiring human oversight.
We present Lean-GAP (Lean-Graduate Agebra Problems), 430 formalized graduate-level algebra problems from the textbook Abstract Algebra by Dummit and Foote. We develop a scalable pipeline consisting of PDF-to-LaTeX preprocessing, autoformalization into Lean 4, and verification of informal-formal correspondence. While the preprocessing and autoformalization stages can be largely automated, we find that verification remains the most subtle and labor-intensive component, requiring careful human oversight. Our contributions include (i) the construction of a structured dataset of formalized exercises, (ii) a systematic methodology for formalizing textbook mathematics, and (iii) an analysis of recurring challenges in the formalization process. We also compare the performance of different autoformalization models and highlight key bottlenecks in translating informal statements into formal language.