Anthropic, Claude로 페르마의 마지막 정리 기계 검증 증명 공개

Anthropic이 AI 모델 Claude를 활용해 **페르마의 마지막 정리(FLT)**의 첫 완전 기계 검증 증명을 공개했다. 이는 1995년 앤드류 와일즈의 증명을 Lean 증명 보조기를 통해 형식화한 것으로, 새로운 수학적 발견이 아닌 기존 증명의 컴퓨터 검증이다.

프로젝트 규모 및 성과

해당 프로젝트는 11일간의 자율 작업을 통해 진행되었으며, 약 1,300만 줄의 Lean 코드와 29,500개의 중간 정리를 생성했다. 이는 기존 Mathlib 라이브러리의 5배 이상 규모다. Tianyi Peng이 주도하고 Kevin Buzzard 교수가 검증한 이 증명은 수학 공리 외에는 어떠한 가정도 포함하지 않으며, 대수, 조화해석, 기하, 정수론 등 광범위한 분야를 형식화했다.

검증 과정 및 기술적 특징

증명은 Prove2Me라는 멀티 에이전트 하네스를 통해 완성되었으며, 출력 토큰은 약 60억 개에 달한다. Lean 표준 공리 3개에만 의존하며, axiom이나 sorry 같은 미완성 코드는 금지되었다. 외부 도구(comparator, nanoda)를 통해 진술 일치 및 타이핑 규칙을 재검증했으며, Claude 스스로 오류를 발견하고 수정하는 과정을 거쳤다.

한계 및 향후 과제

현재 증명은 독립적인 재검증을 대기 중이며, Mathlib과의 통합에는 주석 부재, 파일 구조 비효율성, 중복 선언 등의 기술적 장벽이 존재한다. Anthropic은 형식화가 수학 지식의 신뢰성을 높이는 도구가 되기를 기대하지만, AI 생성 논증의 평가 어려움과 홍보 과대평가 가능성에 대한 학계의 우려도 함께 언급했다. 해당 저장소는 Apache License 2.0으로 공개되어 연구 및 상업적 사용이 가능하다.