자동 교재 형식화

Automatic Textbook Formalization

본 연구에서는 자동화된 AI 시스템이 500페이지가 넘는 대학원 수준의 대수 조합론 교재를 Lean으로 형식화하는 사례 연구를 제시합니다. 결과적으로 생성된 형식화는 교재 형식화의 규모와 숙련도 측면에서 새로운 이정표를 세웠으며, 이는 기존의 학부 위상수학 관련 초기 연구 및 기존 라이브러리 콘텐츠 재구성에서 벗어나, 대학원 교재 전체를 완벽하게 형식화한 것입니다. 이 형식화는 13만 줄의 코드로 구성되어 있으며, 5900개의 Lean 선언을 포함하고 있습니다. 이 작업은 총 30,000개의 Claude 4.5 Opus 에이전트가 버전 관리 시스템을 통해 공유 코드 베이스에 병렬로 협력하여 1주일 이내에 완료되었으며, 이는 실용적인 결과물을 산출하는 다중 에이전트 소프트웨어 엔지니어링 분야에서 새로운 기록을 세운 것입니다. 추론 비용은 인간 전문가 팀에 필요한 급여를 상회하거나 동등한 수준이며, 더 나은 모델이 필요하지 않더라도 상당한 효율성을 얻을 수 있을 것으로 예상됩니다. 저희는 생성된 코드, 결과 Lean 코드 베이스 및 비교 청사진 웹사이트를 오픈 소스로 제공합니다.

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.