1600만줄 수학 코드 공개…AI 작성분은 사람 검토 남아
제목 연관성·주요 수치·시장 영향·향후 전망을 기준으로 핵심 문장을 선별한 요약 브리핑입니다.
핵심 포인트
- Axiom Math가 대수기하학 참고서 Stacks Project의 형식화 가능한 항목을 약 1600만 줄의 Lean 코드로 공개했다.
- AI 에이전트가 작성한 코드 일부는 아직 사람 검토를 거치지 않았다.
- Axiom Math가 대수기하학 참고서 Stacks Project에서 형식화할 수 있는 수학 항목을 약 1600만 줄의 Lean 코드로 공개했다.
본문
Axiom Math가 대수기하학 참고서 Stacks Project의 형식화 가능한 항목을 약 1600만 줄의 Lean 코드로 공개했다. AI 에이전트가 작성한 코드 일부는 아직 사람 검토를 거치지 않았다. Axiom Math가 대수기하학 참고서 Stacks Project에서 형식화할 수 있는 수학 항목을 약 1600만 줄의 Lean 코드로 공개했다. AI 에이전트가 작성한 증명도 컴퓨터로 검사하도록 구성했지만, AI 작성분을 원문과 대조하는 작업은 남아 있다. Axiom Math는 4일 발표문에서 약 7500쪽 분량의 Stacks Project를 재사용 가능한 하나의 형식 수학 라이브러리로 만들었다고 밝혔다. 공개 저장소는 원문 항목과 이에 대응하는 형식 명제를 연결해 제공한다. 공개 저장소 README에 따르면 코드는 Lean 4와 수학 라이브러리 Mathlib을 기반으로 하며 Apache 2.0 라이선스를 적용했다.
‘StacksCore’는 사람이 원문과 대조해 검토한 부분이고, ‘StacksFrontier’는 AI 에이전트가 작성해 아직 사람 검토를 거치지 않은 부분이다. Axiom Math는 형식화 과정에서 원문 명제 수십 건에 추가 가정이 필요하거나 특정 조건에서 성립하지 않을 가능성이 있는 사례를 찾았다고 밝혔다. 11월 5일 공개 저장소에는 두 파일을 수정해 빌드 오류를 고치려는 커밋이 올라왔다. AI가 수학 문제의 답을 제시하는 데서 나아가 풀이를 형식적으로 검증하는 연구 흐름은 구글 딥마인드의 수학 협력과 형식 증명 시스템을 다룬 본지 보도에서도 소개됐다. 이번 작업은 AI가 작성한 수학 코드의 규모와 사람 검토의 필요성을 함께 보여준다.