앤트로픽, 클로드로 페르마의 마지막 정리 형식화 완료

앤트로픽은 4일(현지시간) 공식 발표를 통해 클로드가 페르마의 마지막 정리를 Lean 증명 보조기에서 처음부터 끝까지 확인할 수 있는 형태로 형식화했다고 밝혔다. 회사 설명에 따르면 클로드는 11일 동안 대부분 자율적으로 작업했으며, 완성된 증명은 Lean으로 검증됐다.

이번 작업은 새로운 수학적 증명을 발견한 것이 아니라 앤드루 와일스의 기존 증명을 컴퓨터가 점검할 수 있도록 논리 단계별 코드로 옮긴 것이다. 사람이 읽는 증명은 자명한 단계를 생략할 수 있지만, 형식 증명은 사용한 정의와 추론을 빠짐없이 명시해야 한다.

앤트로픽에 따르면 클로드는 최종 증명에 쓰인 2만9,500개를 포함해 3만300개의 중간 정리를 증명하고 약 1,300만 줄의 Lean 코드를 작성했다. 여러 클로드 에이전트는 정리 사이의 의존관계를 그래프로 관리하는 공개 플랫폼 Prove2Me와 클로드 코드 기반 다중 에이전트 환경에서 병렬로 작업했다.

완성된 증명은 Lean의 표준 공리 세 가지만 사용했으며, 비교 도구를 통해 정리의 문장이 Mathlib에 수록된 페르마의 마지막 정리와 일치하는지도 확인했다. 앤트로픽은 전체 코드와 설명 자료를 GitHub에 공개했다.

다만 이번 결과는 형식 검증이 사람이 이해할 수 있는 수학적 해설을 대체한다는 뜻은 아니다. 앤트로픽도 완성된 증명이 필요한 수준보다 훨씬 길 가능성을 인정했다. 그럼에도 대규모 증명을 컴퓨터가 검사 가능한 형태로 바꾸는 시간이 크게 줄었다는 점에서, AI가 만든 수학 결과를 검증하고 학술 심사의 부담을 낮추는 도구로 활용될 가능성을 보여준다.

출처: Anthropic 공식 발표, “Formalizing Fermat's Last Theorem” (2026년 9월 4일) https://www.anthropic.com/news/formalizing-fermats-last-theorem
Anthropic GitHub 저장소, “fermats-last-theorem” https://github.com/anthropics/fermats-last-theorem