Anthropic, Claude로 페르마의 마지막 정리 11일 만에 완전 형식화 검증 성공

Anthropic 연구팀이 AI 모델 Claude를 활용해 수학 역사상 가장 유명한 난제 중 하나인 **페르마의 마지막 정리(Fermat's Last Theorem)**를 11일 만에 완전한 컴퓨터 검증 형태로 형식화하는 데 성공했다. 이는 인간이 수개월에서 수년이 걸리는 복잡한 논리 검증 과정을 AI가 자율적으로 수행할 수 있음을 입증한 사례다.

형식화 과정과 기술적 성과

이번 프로젝트는 Columbia University의 Tianyi Peng와 협력하여 개발된 개방형 협업 플랫폼 Prove2Me를 기반으로 진행되었다. 수십 개의 Claude 에이전트가 병렬로 작업하며 개념 정의, 중간 정리 증명, 최종 명제 증명을 수행했다.

• 코드 규모: 최종 증명은 1,300만 줄의 Lean 코드로 구성되었으며, 이는 주요 수학 라이브러리인 Mathlib의 5배 이상 규모다.
• 증명 구조: 총 30,300개의 정리에 대한 검증 가능한 증명을 생성했으며, 그중 29,500개가 최종 증명에 사용되었다.
• 핵심 메커니즘: 에이전트 간 협력을 위해 정리 명제의 **Directed Acyclic Graph(DAG)**를 유지하고, 증명 파일과 명제 파일을 분리해 컴파일 속도를 최적화했다.

검증의 신뢰성과 의미

Kevin Buzzard(Imperial College London)는 이번 성과가 수학의 공리(axioms) 외에는 어떤 가정도 없이 FLT를 증명했다고 평가했다. 생성된 증명은 GitHub에 공개되었으며, Lean의 표준 공리 3개만을 사용해 논리적 결함이 없음을 확인했다.

기존에는 Wiles의 증명(1995년)처럼 복잡한 논리 체인을 인간이 검증하는 데 수개월이 소요되었으나, 이번 형식화를 통해 AI가 생성한 수학 결과의 신뢰성을 확보하는 부담이 크게 줄어들 것으로 기대된다. 특히 Anthropic은 소비자 구독 수준인 Claude Max 플랜 3개로도 Vinogradov’s Three Primes Theorem을 3일 만에 형식화하는 실험에 성공하며, 적절한 스캐폴드(scaffold)만 있다면 대규모 형식화가 가능함을 시사했다.