350년 넘게 수학자들을 괴롭혀 온 페르마의 마지막 정리(FLT)가 이번에는 조금 다른 방식으로 다시 화제에 올랐다. Anthropic은 클로드가 리드(Lean) 언어로 작성한, 최초의 완전한 컴퓨터 검증 FLT 증명을 공개했다. 1637년 페르마가 디오판토스의 책 여백에 'n이 2보다 클 때 aⁿ + bⁿ = cⁿ을 만족하는 양의 정수 a, b, c는 없다'고 적은 이 명제는, 1995년 앤드루 와일스가 129쪽에 달하는 증명을 내놓기까지 풀리지 않았다. 그 증명을 검증하는 데만 여러 수학자가 수개월을 매달려야 했다.
이번 작업의 핵심은 새로운 수학을 만든 것이 아니라 '검증'에 있다. 형식화(formalization)란 사람이 읽도록 쓰인 증명을, 컴퓨터가 논리의 모든 단계를 자동으로 확인할 수 있는 형태로 바꾸는 일이다. 사람용 증명은 '자명한' 단계를 생략하지만, 리드 같은 증명 보조기는 아무리 사소한 단계라도 빠짐없이 명시해야 한다. 게다가 형식화는 이미 형식화된 극히 일부의 수학 위에서만 출발할 수 있어, 인류가 수백 년간 쌓아 온 축적을 처음부터 다시 코드로 깔아야 하는 부담이 크다.
11일, 1,300만 줄의 리드 코드
Anthropic 연구자이자 컬럼비아대에서 AI 형식화 도구를 만드는 텐이 펑(Tianyi Peng)이 클로드가 FLT 형식화에 얼마나 기여할 수 있는지 시험한 것이 출발점이었다. 결과는 예상을 넘어섰다. 클로드는 11일 동안 대체로 자율적으로 작업하며 1,300만 줄의 리드 코드를 작성했고, 그 과정에서 3만 300개의 정리를 증명해 그중 2만 9,500개를 최종 증명에 사용했다. 이는 이 정리가 기반으로 삼는 커뮤니티 표준 라이브러리 Mathlib의 5배가 넘는 분량이며, 지금까지 만들어진 리드 증명 중 최대 규모다. 사람이 개입한 부분은 '스킴으로서의 야코비안이 우선순위가 높아 보인다'거나 '마주어 정리를 빨리 끝내라' 같은 텐이 펑의 간헐적 고수준 지시에 그쳤다.
증명은 와일스의 증명을 다르몽·다이아몬드·테일러가 단순화한 판본을 따랐다. 처음부터 순탄했던 것은 아니다. 초기 시도에서 여러 에이전트는 잠깐의 성과를 낸 뒤 프로젝트의 전체 상태를 놓치고 협업이 무너졌다. 이렇게 실패한 시도들이 최종 증명의 비(非)보일러플레이트 코드 중 약 7%로 남았다. 전환점은 텐이 펑과 컬럼비아대 협력자들이 설계한 개방형 협업 플랫폼 Prove2Me로 갈아탄 순간이었다. 클로드 코드 기반의 멀티에이전트 구조와 결합하자, 여러 에이전트가 개념을 정의하고 중간 정리를 증명하며 점점 더 어려운 명제로 나아가는 협업이 2주 남짓 만에 완주로 이어졌다.
소비된 것과 확인된 것
이 프로젝트는 약 60억 개의 출력 토큰을 소비했다. 사용된 모델은 클로드 페이블(Fable) 5.1과 대략 비슷한, 범용 사내 연구용 모델로 소개됐다. 완성된 증명은 리드가 검증했고, 리드의 표준 공리 세 개만을 사용했으며, 별도 비교기가 이 정리의 진술이 Mathlib에 담긴 FLT 진술과 일치함을 확인했다. 즉 '무엇을 증명했는가'와 '올바르게 증명했는가'가 모두 기계적으로 담보됐다는 뜻이다. 원래 수학계는 이 초기 단계 형식화만 해도 수년이 걸릴 것으로 봤고, 그 청사진 문서만 86쪽에 달했다.
실무적 함의는 검증 부담의 재분배에 있다. AI와 AI 보조 수학자가 점점 더 많은 (증명이라 주장되는) 결과를 쏟아내는 상황에서, 한 편의 새 결과를 깊이 이해하고 신뢰하기까지 수개월에서 수년이 걸리는 심사 과정은 병목이 된다. 형식화가 쉬워지면 사람 심사자의 짐을 덜 수 있고, 사람용 해설과 함께 형식 증명을 첨부하는 관행이 자리 잡을 수 있다. FLT 프로젝트를 이끈 케빈 버저드는 이번 성과가 '모든 수학을 손쉽게 검증할 수 있는 미래로 가는 의미 있는 진전'이라고 평가했다. 다만 Anthropic도 형식 증명이 사람이 이해할 수 있는 서술을 대체해서는 안 된다고 선을 그었다. 형식화는 신뢰를 담보하는 장치이지 설명을 대신하는 것이 아니다.
한계도 분명히 짚을 필요가 있다. 이 작업은 새 수학을 발견한 것이 아니라 이미 존재하는 증명 노선을 코드로 옮긴 것이며, 60억 토큰이라는 막대한 계산 자원이 투입된 대형 프로젝트였다. 그럼에도 규모의 문턱이 절대적이지는 않다는 신호도 있다. Anthropic 연구자들은 개인용 클로드 맥스 요금제 세 개만으로 Prove2Me를 통해 협업해, 하디-리틀우드 원 방법의 응용인 비노그라도프의 세 소수 정리를 사흘 만에 형식화했다. 적절한 골격만 갖추면 소비자용 구독으로도 주요 정리의 협업 형식화가 가능하다는 것이다.
흥미로운 부수 효과는 형식화가 거꾸로 AI의 추론을 돕는다는 관찰이다. 최근 클로드가 만든 여러 결과는 증명과 형식화가 병행됐는데, 클로드는 수치 시뮬레이션으로 방향을 점검하듯 부분 형식 증명을 자기 가설의 검산 도구로 활용하는 모습을 보였다. AI가 수학 연구의 풍경을 빠르게 바꾸는 가운데, 적어도 형식화는 검증 가능성과 신뢰라는 명확한 가치를 제공하는 영역으로 보인다. 전체 증명과 서술형 해설은 깃허브에 공개돼 있어, 관심 있는 실무자라면 코드 구조와 협업 방식을 직접 들여다볼 수 있다.