2026년 9월 4일, Anthropic은 학계를 뒤흔든 소식을 발표했습니다. 수십 개의 AI 에이전트 군단이 단 11일 만에 페르마의 마지막 정리에 대한 기계 정식화 및 검증을 완료했다는 것입니다. 이에 반해 임페리얼 칼리지 런던의 정상급 수학자 연구팀은 100만 파운드의 연구비를 지원받아 동일한 작업에 무려 5년의 일정을 계획하고 있었습니다.
350년 넘게 인류를 괴롭혀온 이 수학적 난제는 이미 1995년 영국의 수학자 앤드루 와일스(Andrew Wiles)에 의해 증명되었습니다. 오늘날 벌어진 11일 대 5년의 대결은 수학 자체의 지평을 넓힌 사건은 아닙니다.
이 대결이 진정으로 무너뜨린 것은 지식의 신뢰를 구축하기 위해 인간 전문가에게 의존해 온 오랜 방식입니다. 최고 권위의 논문 검증이 ‘인간 동료들의 수년에 걸친 오류 가능성을 안은 검토’에서 ‘기계가 단 몇 분 만에 논리적 결함을 확인하는 방식’으로 근본적인 전환을 맞이한 것입니다.
350년 난제가 드러낸 인간 검토 시스템의 한계
페르마의 마지막 정리 증명의 역사를 돌아보면, 그것은 인간 동료 평가 시스템이 겪은 지속적인 실패의 기록이기도 합니다. 1908년 독일에서는 증명을 제시하는 이에게 10만 금마르크의 볼프스켈 상금을 내걸었습니다. 막대한 상금에 힘입어 첫해에만 621편의 엄밀해 보이는 답안이 접수되었으나, 예외 없이 모두 치명적인 오류가 발견되었습니다.
인간의 두뇌는 방대하고 복잡한 논리를 다룰 때 본질적으로 사각지대를 갖습니다. 1993년 6월, 와일스는 케임브리지 아이작 뉴턴 연구소에서 사흘간 강연을 열고 페르마의 마지막 정리를 증명했다고 전 세계에 선언했습니다. 그러나 두 달 뒤, 심사위원들이 일상적인 검토 과정에서 제기한 날카로운 질문 하나가 증명 체계 내의 치명적인 허점을 정면으로 드러냈습니다.
와일스는 이를 바로잡기 위해 한때 포기를 생각할 만큼 고통스러운 1년을 더 보낸 끝에, 1995년 5월이 되어서야 129쪽에 달하는 최종 논문을 공식 발표할 수 있었습니다. 밀실에 모인 소수의 천재 수학자들이 100쪽이 넘는 빽빽한 필사본을 일일이 검토하는 장인 방식의 검증은, 당시 이미 인간 인지 능력의 물리적 한계에 다다르고 있었습니다.
그림: Anthropic 공식 발표 페이지. 출처: Anthropic
11일 만에 작성된 1,300만 줄의 기계 코드
기호로 가득 찬 수학적 증명을 어떻게 기계가 검증하도록 만들 수 있을까요? 여기에는 ‘정식화(formalization)’ 과정이 필수적입니다. 인간의 직관과 비약이 담긴 산문 형태의 증명을, 문장부호 하나조차 틀려서는 안 되는 기계 코드로 번역하는 작업입니다. 과거에는 극소수의 열정적인 연구자들만이 감당하던 고된 수작업이었습니다.
임페리얼 칼리지 런던의 케빈 버저드(Kevin Buzzard) 교수는 페르마의 마지막 정리를 정식화하기 위해 5년 일정의 커뮤니티 프로젝트를 이끌고 있었습니다. 번역 경로를 안내하는 ‘청사진(blueprint)’ 문서를 작성하는 데만 86쪽을 썼을 정도였습니다.
Anthropic의 내부 연구 모델 Claude는 Prove2Me 플랫폼에서 이 기나긴 일정을 2주도 되지 않는 시간으로 압축했습니다. 1995년의 고전적인 간소화 논증 경로를 그대로 따르면서도, 무려 1,300만 줄이 넘는 코드를 생성해 냈습니다. 이는 해당 플랫폼의 공식 수학 라이브러리에 존재하는 모든 코드를 합친 것보다 5배 이상 방대한 규모입니다.
이 코드베이스에는 30,300개에 이르는 정리의 증명 과정이 포함되었으며, 최종적으로 29,500개가 증명 그래프에 반영되었습니다. 수십 개의 AI 에이전트가 지치지 않는 톱니바퀴처럼 병렬로 협업하며, 모호한 인간의 직관을 잘게 쪼개어 기계가 한 줄씩 실행할 수 있는 논리 사슬로 구축했습니다.
30만 달러로 구매한 절대적 확실성
산업 수준의 연산 능력이 투입되면서, 기존의 막대한 인건비는 명확한 연산 비용 청구서로 대체되었습니다. 버저드 교수 팀의 5년 계획은 100만 파운드의 예산을 필요로 했으며, 이는 수학자들의 두뇌와 급여, 그리고 오랜 소통 비용에 의존하는 구조였습니다.
반면 Claude의 이번 검증에는 약 60억 개의 출력 토큰이 소모되었습니다. 현재 공개된 API 가격을 기준으로 추산하면 이 비용은 약 30만 달러 안팎입니다. 인간의 5년에 걸친 노력이 필요한 절대적 확실성을 30만 달러의 연산 자원으로 확보했다는 점에서, 최전선 학술 탐구의 비용 구조는 되돌릴 수 없는 재편을 겪고 있습니다.
기계가 처음부터 완벽했던 것은 아닙니다. 초기 시도에서는 에이전트 간의 협업 오류로 프로젝트 상태를 유실하기도 했습니다. 그러나 시스템은 시행착오를 통해 빠르게 대응했으며, 실패한 시도들 역시 최종 코드에서 보일러플레이트가 아닌 핵심 행의 약 7%를 차지하며 기여했습니다. Anthropic의 연구원들은 최상위 지침만 제시했을 뿐, 세부적인 디버깅과 장애 해결은 기계가 자율적으로 해결했습니다.
그림: Prove2Me 플랫폼의 증명 경로 DAG 그래프. Claude가 보조 정리를 분해하며 단계적으로 정리에 접근하는 과정을 보여준다. 출처: Anthropic
과학적 신뢰의 주도권이 컴파일러로 넘어가다
케빈 버저드 교수가 천만 줄이 넘는 이 방대한 코드를 직접 검증했고, 컴파일러는 오류 없이 통과했습니다. 비교 분석 도구를 통해서도 모든 정리의 서술이 기존 수학 라이브러리와 완벽히 일치함이 확인되었습니다. 이로써 20년 역사를 지닌 ‘100대 정식화 과제’ 벤치마크 목록도 완전히 마무리되었습니다.
버저드 교수 본인이 언급했듯 수학적으로 새로운 정리가 발견된 것은 아닙니다. 하지만 자동 정식화 영역에서 이번 성과는 매우 강력한 실증적 증거를 제공합니다. 129쪽에 달하는 복잡한 수학 증명이 소프트웨어 엔지니어링의 소스 코드처럼 컴파일될 수 있다면, 학계의 신뢰 네트워크는 근본적으로 대체됩니다.
과거에는 저명한 석학들이 보증했기 때문에 정리가 참이라고 신뢰했습니다. 이제 그러한 중앙집권적 권위 모델은 힘을 잃고 있습니다. 코드가 컴파일러를 통과하기만 한다면 진리는 그 누구의 보증도 필요로 하지 않습니다. 컴파일러가 과학적 진실의 최후 방어선을 넘겨받았습니다.
참고 링크:
- Anthropic Research
- HN 토론
