우리는 Dummit과 Foote의 교과서인 Abstract Algebra에서 추출한 430개의 정식화된 (formalized) 대학원 수준 대수학 문제인 Lean-GAP (Lean-Graduate Algebra Problems)을 선보입니다. 우리는 PDF-to-LaTeX 전처리, Lean 4로의 자동 정식화 (autoformalization), 그리고 비정식-정식 대응 관계의 검증 (verification)으로 구성된 확장 가능한 파이프라인을 개발했습니다. 전처리 및 자동 정식화 단계는 상당 부분 자동화될 수 있지만, 검증 단계는 여전히 가장 미묘하고 노동 집약적인 구성 요소로 남아 있으며 세심한 인간의 감독이 필요하다는 것을 발견했습니다. 우리의 기여는 다음과 같습니다: (i) 정식화된 연습 문제의 구조화된 데이터셋 구축, (ii) 교과서 수학을 정식화하기 위한 체계적인 방법론, (iii) 정식화 과정에서 반복되는 과제에 대한 분석. 또한 우리는 서로 다른 자동 정식화 모델의 성능을 비교하고, 비정식 진술을 정식 언어로 번역할 때 발생하는 주요 병목 현상을 강조합니다.