Axiom, 7,500페이지 Stacks Project를 Lean으로 완전 형식화하다

The Stacks Project, Formalized in Lean

Axiom이 현대 대수기하학의 기초를 담은 7,500페이지 분량의 Stacks Project 전체를 Lean으로 형식화해 공개했다. 1,600만 줄 규모로, 재사용 가능한 단일 기계 검증 라이브러리 중 최대다. AI 에이전트 군집을 동원해 수천 개 정리를 병렬로 번역·증명·통합했고, 원문의 영구 태그를 보존해 원문과 Lean 코드를 나란히 볼 수 있다. 형식화 과정에서 누락된 가설이나 반례가 있는 정리 수십 개를 발견해 수정하기도 했다.