클로드, 페르마의 마지막 정리 첫 컴퓨터 검증 증명 완성

1637년 피에르 드 페르마는 디오판토스의 산술책 여백에 한 문장을 적어놨어요. 2보다 큰 어떤 지수 n에 대해서도 양의 정수 a, b, c가 a^n + b^n = c^n을 만족할 수 없다는 주장이었어요. 여백이 좁아 증명을 적지 못했다는 메모까지 남겼지만, 정작 그 증명은 350년 넘게 나오지 않았어요. 1995년 앤드루 와일스가 129쪽 분량의 증명을 내놓기까지 숱한 시도가 있었고, 1908년에는 정답자에게 당시 가치로 100만~200만달러에 해당하는 상금까지 걸렸는데 첫해에만 621건의 오답이 쏟아졌을 정도였어요. 와일스의 증명도 발표 직후 검증 과정에서 중대한 허점이 발견돼 그가 1년을 더 매달린 끝에야 완성됐어요.

10년 뒤 네덜란드 컴퓨터과학자 얀 베르흐스트라가 이 증명을 공식화하자고 제안했어요. 사람이 읽는 논리를 컴퓨터가 검증할 수 있는 형태로 바꾸자는 아이디어였죠. 이후 임페리얼칼리지런던의 케빈 버저드가 2024년부터 Lean 증명 보조기를 이용한 다년간의 커뮤니티 작업을 이끌어 왔고, 이 초기 단계만 정리한 청사진 문서도 86쪽에 달했어요.

풀어서 설명하면, 앤드루 와일스가 1995년에 손으로 완성한 129쪽짜리 증명은 사람이 읽고 확인하는 데도 수개월이 걸렸는데, 이걸 컴퓨터가 한 줄씩 검증할 수 있는 Lean이라는 언어로 다시 써내는 작업이 공식화예요. 앤스로픽은 이 공식화를 클로드에게 맡겨 11일 만에 끝냈는데, 이는 지난달 테렌스 타오가 경고한 것처럼 AI가 수학적 성과를 검증하는 문지기 역할까지 맡을 수 있다는 신호로 읽혀요.

클로드가 11일 동안 한 일

컬럼비아대에서 AI 공식화 도구를 연구하는 앤스로픽 연구원 티안이 펑이 클로드가 FLT 공식화에서 진전을 낼 수 있는지 시험해봤어요. 결과는 그의 예상을 훨씬 뛰어넘었어요. 클로드는 11일 만에 처음부터 끝까지 이어지는 컴퓨터 검증 증명을 완성했고, 그 과정에서 3만300개의 정리를 증명해 이 중 2만9500개를 최종 증명에 사용했어요. 수십 개의 클로드 에이전트가 개념을 정의하고 중간 정리를 증명하며 점점 더 어려운 명제를 풀어가는 방식으로 협업했어요.

클로드의 증명은 다르몽, 다이아몬드, 테일러가 정리한 와일스 증명의 단순화 버전을 따랐어요. 인간이 개입한 부분은 티안이 펑이 이따금 던진 고차원 지시 정도였어요. "야코비안을 스킴으로 다루는 게 우선순위가 높아 보인다" 같은 조언이었죠.

비교 항목	와일스 증명(1995)	클로드 공식화(2026)
분량	129쪽	Lean 코드 1300만 줄
검증 소요	수개월(사람 검토)	11일(AI 자율 작업)
중간 정리	별도 집계 없음	2만9500개 사용(3만300개 생산)

실패를 넘어선 프로세스, Prove2Me

처음부터 순탄하지는 않았어요. 초기 시도에서 에이전트들은 어느 정도 성과를 냈지만 곧 작업 상태를 놓치고 서로 효과적으로 협업하지 못했어요. 이 실패한 시도들이 최종 증명의 비보일러플레이트 코드 중 약 7%를 차지했다고 해요.

전환점은 프로젝트가 Prove2Me라는 플랫폼으로 옮겨가면서 왔어요. 티안이 펑과 컬럼비아대 동료들이 만든 이 오픈 협업 플랫폼은 세 가지로 작업을 도왔어요. 정리 문장들의 방향성 비순환 그래프(DAG)를 유지해 에이전트가 다음에 무엇을 증명할지 판단하게 했고, 정리 문장과 증명을 별도 파일로 분리해 Lean 컴파일 속도를 높였고, 각 정리에 자연어 설명을 붙여 검색과 재사용을 쉽게 했어요.

앤스로픽은 완성된 증명을 케빈 버저드에게 공유했고, 그는 이렇게 평가했어요.

"이 특별한 자동 공식화 성과는 수학 공리 외 다른 가정 없이 페르마의 마지막 정리를 증명한다" - 케빈 버저드(임페리얼칼리지런던)

증명 코드는 공개돼 있다

전체 Lean 코드와 증명 그래프는 github.com/anthropics/fermats-last-theorem 저장소에서 확인할 수 있어요. 수학자나 개발자라면 클로드가 실제로 어떤 순서로 정리를 쌓아 올렸는지 코드 단위로 열람할 수 있어요.

리만 가설, 그리고 이어지는 질문들

앤스로픽이 수학 난제에 클로드를 붙인 건 이번이 처음이 아니에요. 지난달에는 외부에 공개되지 않은 연구용 클로드로 리만 가설에 도전해 제타 함수 영점 비율의 하한을 기존보다 높였다고 보고한 적이 있어요. 이 흐름 위에서 필즈상 수상자 테렌스 타오는 국제수학자대회 에세이를 통해 AI가 수학계에 1900년대 초 기초 위기에 준하는 혼란을 불러올 수 있다고 경고했는데요, 이번엔 수학적 진리 자체가 아니라 무엇을 성과로 인정하고 누구의 공로로 볼지를 정하는 암묵적 가치체계가 시험대에 올랐다는 진단이었어요.

에디터의 시선

이번 발표에서 진짜 새로운 건 증명이 아니라 검증이에요. 최근 리만 가설 관련 작업이 새로운 수학적 발견을 목표로 했다면, 이번 FLT 공식화는 이미 30년 전에 증명된 결과를 컴퓨터가 한 치의 의심 없이 확인하는 작업이었어요. 앤스로픽 스스로도 이걸 강조하는데, 논리적으로 옳다고 믿는 것과 실제로 옳다는 걸 계산기로 검산하듯 확인하는 건 전혀 다른 일이거든요.

세대 비교로 보면 체감이 확실해요. 와일스의 증명은 발표 후 두 달 만에 검토자의 질문 하나에서 치명적 허점이 드러났고, 그 허점을 메우는 데만 1년이 걸렸어요. 사람이 129쪽짜리 논리를 눈으로 좇으며 검증하는 데는 근본적 한계가 있다는 뜻이에요. 클로드는 같은 논리를 1300만 줄의 기계 검증 코드로 풀어냈고, Lean이 그 사슬 하나하나를 자동으로 확인했어요. 사람이 놓칠 수 있는 틈을 기계가 대신 메운 셈이에요.

실무적으로 보면 이 사건은 두 갈래 신호를 줘요. 하나는 수학 연구자에게고, 다른 하나는 이 흐름을 지켜보는 모든 지식 산업 종사자에게예요. 수학계에는 이제 새 결과를 검증하는 데 걸리던 수년의 시간을 줄일 도구가 생겼다는 뜻이고, 다른 분야에는 사람이 검증하기 벅찬 복잡한 논리 구조를 AI가 대신 formal하게 재구성해줄 수 있다는 선례가 생긴 셈이에요. 다만 이 작업도 초기 시도에서 에이전트들이 상태를 잃고 협업에 실패했다는 점은 기억해둘 만해요. 좋은 인프라(Prove2Me 같은 상태 관리 도구) 없이는 AI 에이전트의 자율 작업이 금방 흐트러진다는 증거이기도 하니까요.

앞으로 몇 주 안에는 다른 난제에 같은 방식이 적용되는 사례가 더 나올 가능성이 높아요. 오픈AI도 최근 장기 미해결 수학 문제 해법을 냈다고 주장한 바 있어서, 두 회사가 수학 공식화와 증명 검증을 놓고도 경쟁 구도를 만들어갈 것으로 보여요.