대규모 수학 형식화

Formalizing Mathematics at Scale

본 논문에서는 Lean 4 환경에서 대규모 자동 형식 교재 라이브러리(Atlas)를 구축하기 위한 다중 에이전트 시스템인 AutoformBot을 소개합니다. AutoformBot은 수천 개의 LLM 에이전트를 활용하며, 각 에이전트는 형식 검증 도구와 의존성 기반 작업 스케줄링 및 협업 버전 관리를 갖추고 있습니다. 이를 통해 비형식적인 교재 내용을 기계적으로 검증 가능한 정의와 증명으로 변환합니다. 저희는 분석, 대수학, 위상수학, 조합론 및 확률을 포함하는 26개의 공개 접근 교재 모음에 이 방법을 적용하여 Atlas를 구축했습니다. Atlas는 45,000개 이상의 Lean 4 선언과 50만 줄의 코드를 포함하는 검증된 라이브러리입니다. 저희는 다음과 같은 두 가지 결과물을 제공합니다: (i) 오픈 소스 다중 에이전트 프레임워크인 AutoformBot 및 (ii) 결과물인 형식 라이브러리인 Atlas. 저희의 연구 결과는 대학원 수준의 핵심 수학 내용을 대규모로 자동 형식화하는 것이 이제 경제적, 기술적으로 실현 가능하다는 것을 시사합니다. 이는 인간과 기계가 생성한 수학 콘텐츠를 연구 수준에서 자동으로 검증할 수 있는 가능성을 열어줍니다.

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.