Anthropic이 페르마의 마지막 정리의 첫 컴퓨터 검증 증명을 완성했습니다. Claude는 11일간 자율적으로 작업하여 Lean 프로그래밍 언어로 완전한 증명을 작성했습니다. 이는 단순히 새로운 수학 결과를 찾아낸 것이 아니라, 350년 전 페르마의 난제에 대한 증명을 컴퓨터가 한 줄도 빠짐없이 검증할 수 있는 형태로 변환해낸 것입니다. 이 성과는 미래 수학 연구의 신뢰성과 검증 방식에 깊은 의미를 갖습니다.
350년을 기다린 증명
1637년경, 수학자 페르마는 책의 여백에 "양의 정수 a, b, c가 n > 2일 때 aⁿ + bⁿ = cⁿ을 만족할 수 없다"는 주장을 남겼습니다. 이것이 페르마의 마지막 정리(Fermat's Last Theorem, FLT)입니다. 이후 350년 이상 세대를 거친 수학자들이 이 난제의 증명을 찾으려 애썼습니다. 1908년에는 증명에 성공하는 사람에게 100,000마르크(현재가로 100만~200만 달러)의 상금까지 걸렸고, 첫 해에만 621개의 틀린 증명이 제출되었습니다. 이는 증명의 어려움이 얼마나 컸는지를 생생하게 보여줍니다.
와일스의 증명과 검증의 고난
1993년 6월, 수학자 앤드루 와일스가 증명이라고 주장하는 것을 발표했습니다. 그러나 검증 과정에서 심각한 허점이 발견되었습니다. 와일스는 그것을 고치기 위해 1년을 더 소비했고, 결국 1995년 5월에 정식 증명을 발표했습니다. 증명은 129페이지였고 검증만 수개월이 걸렸습니다. 흥미롭게도 와일스의 증명은 페르마 시대(1637년)에 존재하지 않던 현대 수학 기법을 사용했으므로, 수학 커뮤니티는 페르마의 본래 "멋진 증명"이 실제로는 틀렸을 가능성이 높다고 봅니다. 이 사례는 수학 증명의 검증이 얼마나 복잡하고 시간이 오래 걸리는지를 보여줍니다.
형식화란 무엇인가
증명의 정확성을 확인하는 한 방법은 컴퓨터가 검증하도록 하는 것입니다. Lean 같은 증명 보조기구(proof assistant)는 증명의 논리를 알고리즘으로 검증해 정확성을 의심의 여지 없이 보여줍니다. 이를 "형식화"라고 부릅니다. 어려운 부분은 인간 증명을 Lean이 이해할 수 있도록 다시 작성하는 것입니다. 인간은 자명한 단계를 생략하고 축약 기호를 사용하지만, Lean은 모든 단계를 명시적으로 봐야 합니다. 또한 인간의 증명은 수백 년 발표된 연구의 토대 위에 서지만, 형식화는 이미 형식화된 수학 부분에서만 시작해야 합니다. 이 때문에 처음엔 페르마의 마지막 정리 형식화가 수년이 필요할 것으로 예상되었으며, 수학 커뮤니티가 작성한 초기 단계 설명서만 86페이지였습니다.
Claude의 기적적인 11일 완성
그런데 Claude는 11일 만에 완료했습니다. 과정에서 13백만 줄의 Lean 코드를 작성했고, 최종 증명에 사용된 29,500개를 포함해 총 30,300개의 정리를 증명했습니다. 이는 약 60억 개의 출력 토큰을 소비한 결과입니다. 수십 개의 Claude 에이전트가 협력해 개념을 정의하고, 중간 정리를 증명했으며, 이를 바탕으로 더 어려운 명제를 증명했습니다. Claude의 증명은 기초가 된 Mathlib(수학 증명의 주요 커뮤니티 라이브러리)보다 5배 이상 큽니다. 인간의 입력은 최소한이었으며, Tianyi Peng이 "야코비안을 스킴으로 높은 우선순위로 다루자"나 "Mazur 정리를 빨리 끝내자" 같은 고수준 지침만 제공했습니다.
Prove2Me 플랫폼의 핵심 역할
초기 시도는 실패했습니다. 에이전트들이 초반에 일부 성공했으나 프로젝트 상태를 추적하지 못해 협력이 무너졌기 때문이며, 이러한 초기 실패는 최종 증명의 약 7%를 차지했습니다. 전환점은 Prove2Me라는 개방형 협업 플랫폼 도입이었습니다. Tianyi Peng과 콜럼비아 대학교 협력자들이 설계한 이 플랫폼은 세 가지를 제공했습니다. 첫째, 정리 명제의 방향 비순환 그래프(DAG)를 유지해 에이전트들이 다음 증명 대상을 결정하도록 도왔습니다. 둘째, 정리 명제와 증명을 분리해 다른 파일로 저장하면서 Lean 컴파일을 가속화하고 리소스 사용을 최소화했습니다. 셋째, 각 정리의 자연언어 설명을 유지해 검색과 재사용을 가능하게 했으며, 더 간단한 증명 경로를 찾을 수 있게 했습니다.
형식화가 나타내는 미래
형식화는 수학 연구의 신뢰성을 높입니다. AI가 점점 더 많은 증명을 생성하는 상황에서, 형식화된 증명은 인간 검증자의 부담을 급격히 줄입니다. Kevin Buzzard(임페리얼 칼리지 런던)는 "AI가 생산하는 증명이 늘어날수록, 형식화는 인간 검증자의 부담을 줄이는 주요 요소가 될 것"이라고 말합니다. 앞으로 "인간 독자를 위한 설명과 함께 형식화된 증명을 함께 제시하는 것이 일반화될 것"이라고 예측합니다. Anthropic 연구원들이 세 개의 개인용 Claude Max 구독으로 작업했을 때, 에이전트들은 Prove2Me를 통해 단 3일 만에 비노그라도프의 세 소수 정리를 완성했습니다. 이는 향후 형식화가 일반 AI 사용자도 접근할 수 있는 수준이 될 수 있음을 시사합니다. Anthropic을 비롯한 AI 연구소는 외부 연구자(순수 수학자와 형식화 연구자 포함)를 지원하기 위해 무료 및 할인 구독, 연구 크레딧, 전용 그랜트를 제공하고 있습니다. 이러한 지원은 다른 주요 정리의 형식화나 Lean·Mathlib 개선을 포함할 수 있습니다.
정리
페르마의 마지막 정리를 형식화한 Anthropic의 작업은 AI가 수학 연구에 미치는 영향을 보여줍니다. 350년 난제의 증명을 컴퓨터가 검증할 수 있는 형태로 변환했다는 것은, AI 시대 수학 지식의 신뢰성을 어떻게 유지할지에 대한 하나의 명확한 답을 제시합니다. 형식화는 새로운 수학 결과가 쏟아지는 시대에, 수학의 근본적인 신뢰성을 지킬 수 있는 길을 제시합니다.