Claude, 페르마의 마지막 정리 11일 만에 완전 형식화… 1,300만 줄 Lean 코드 생성

Anthropic의 연구원 Tianyi Peng과 Columbia University 팀은 Claude를 활용해 **페르마의 마지막 정리(Fermat's Last Theorem, FLT)**를 Lean 프로그래밍 언어로 완전 형식화하는 데 성공했다. 이 과정은 약 11일 동안 주로 자율적으로 진행되었으며, 최종적으로 1,300만 줄의 Lean 코드와 29,500개의 증명된 중간 정리를 산출했다. 이는 기존 커뮤니티 라이브러리인 Mathlib의 5배 이상 규모로, 수학 역사상 가장 큰 규모의 컴퓨터 검증된 증명 중 하나다.

멀티 에이전트 협업 플랫폼 'Prove2Me'의 역할

성공적인 형식화를 위해 연구팀은 Prove2Me라는 오픈 협업 플랫폼을 사용했다. 이 플랫폼은 여러 Claude 에이전트가 효과적으로 협업할 수 있도록 다음과 같은 기능을 제공한다.

• DAG 유지보수: 정리 문장들의 Directed Acyclic Graph(DAG)를 관리하여 에이전트 간 메모리 저하를 방지하고 병렬 작업을 가능하게 함
• 파일 분리 전략: 정리 문장과 증명을 분리하고 링크를 독립적으로 유지하여 Lean 컴파일 속도를 높이고 리소스 소비를 최소화함
• 자연어 설명: 각 정리에 대한 자연어 설명을 유지하여 검색 및 재사용을 통해 더 간단한 증명 경로를 유도함

초기 시도에서는 에이전트들이 프로젝트 상태를 잃어버리는 등의 실패가 있었으나, Prove2Me 도입 후 수십 개의 에이전트가 개념 정의부터 복잡한 명제 증명까지 분담하며 문제를 해결했다. 인간의 개입은 고수준 지시 수준으로 제한되었다.

수학 검증의 새로운 패러다임

이번 성과는 AI가 복잡한 수학적 논리를 알고리즘적으로 검증하는 능력을 입증했다. Kevin Buzzard(Imperial College London)는 이 작업이 현대 수학 문헌의 자동 형식화를 향한 큰 진전이라고 평가했다. 형식화된 증명은 인간이 이해하기 어려운 복잡한 논리적 사슬의 오류를 줄이고, AI 생성 수학 결과에 대한 신뢰성을 확보하는 핵심 도구가 될 전망이다.

또한, Anthropic 연구원들은 3개의 개인 Claude Max 플랜을 사용해 Vinogradov의 세 소수 정리 형식화를 3일 만에 완료하는 실험에도 성공했다. 이는 적절한 스캐폴드와 협업 플랫폼이 있다면 소비자용 AI 구독으로도 주요 수학적 결과를 형식화할 수 있음을 시사한다. 향후 이러한 기술은 수학 지식 기반의 오류를 뿌리 뽑고 신규 연구 심사 부담을 경감하는 데 기여할 것으로 기대된다.