facebookresearch/atlas-lean

ATLAS – 대규모 자동 형식화 교과서 라이브러리

정의 – ATLAS는 Lean 4 증명 보조기에서 형식화된 연구급 수학 라이브러리입니다. 코드베이스에는 핵심 수학 라이브러리(Mathlib)를 확장하고 학부 및 대학원 교과서에서 추출한 새로운 정리와 정의를 추가하는 여러 Lean 패키지가 포함되어 있습니다. 형식화 작업은 대규모 언어 모델을 사용하여 교과서의 진술과 증명을 Lean 코드로 변환하는 자동 형식화 파이프라인(AutoformBot)에 의해 구동됩니다.

중요성 – 형식화된 수학은 인간과 기계 모두가 수학적 결과를 절대적 확실성으로 추론할 수 있게 합니다. 교과서 자료를 자동으로 재사용 가능한 Lean 라이브러리로 변환함으로써 ATLAS는 다음에 사용할 수 있는 대규모 고품질 형식 라이브러리 생성을 가속화하는 것을 목표로 합니다:

• 해석학, 대수학, 기하학, 위상수학, 확률론, 통계학, 이론 컴퓨터 과학에서의 검증된 연구.
• 정리 증명을 지원하는 AI 시스템 훈련 및 평가.
• 프로젝트 간에 참조할 수 있는 기계 검증 가능한 수학의 공유 저장소 구축.

주요 구성 요소

구성 요소	역할
MathlibExt/	표준 Mathlib 라이브러리에 대한 새롭고 완전히 증명된 확장.
MathlibExtTest/	MathlibExt의 확장에 대한 테스트, 벤치마크 및 진단.
CSLibExt/	MathlibExt 위에 구축된 형식화된 컴퓨터 과학 결과.
CSLibExtTest/	컴퓨터 과학 확장에 대한 테스트 및 진단.
WantedExt/	식별되었지만 아직 형식화되지 않은 중요한 결과를 위한 자리 표시자.

저장소에는 루트 Lake 패키지에 대한 전체 검증 스위트를 실행하는 check.sh 스크립트가 포함된 scripts/ 폴더도 포함되어 있습니다.

시작 방법

1. Lean 4(v4.34.1 이상) 및 Lake 빌드 도구를 설치합니다.
2. 저장소를 클론하고 루트 검사를 실행합니다:

   scripts/check.sh
   

3. Lean 호환 편집기(예: Lean 확장이 있는 VS Code)에서 .lean 파일을 열어 라이브러리를 탐색합니다.
4. 원래의 더 큰 형식화된 교과서 컬렉션을 보려면 보관된 v1/ 디렉토리로 전환하여 빌드합니다:

   cd v1
   lake build
   

   v1 릴리스에는 평가 보고서, 문서 및 관련 연구 논문도 포함되어 있습니다.

상태 – 현재 저장소에는 활발히 개발 중인 ATLAS v2의 뼈대가 포함되어 있습니다. 이전 v1 릴리스는 보관되었지만 완전히 기능하며 문서화되어 있습니다.

라이선스 – 새로운 기여는 Apache 2.0 라이선스 하에 있습니다. 보관된 v1/ 코드는 원래 라이선스를 유지합니다.

---

ATLAS는 형식 방법과 AI 기반 자동화의 교차점에 있는 진정한 연구 프로젝트이며, 튜토리얼 목록이나 간단한 데모가 아닙니다.