1637년 무렵 페르마가 책 여백에 적은 한 문장은 358년 뒤인 1995년 앤드루 와일즈의 논문으로 증명됐고, 2026년 9월 4일 Anthropic은 그 증명을 컴퓨터가 처음부터 끝까지 확인할 수 있는 형태로 옮겼다고 발표했습니다. Claude 에이전트들이 11일 동안 Lean 코드 1,300만 줄을 써서 해낸 일입니다.

이번 결과는 새로운 증명이 아니에요. 이미 받아들여진 증명을 기계로 다시 확인한 것이고, Anthropic도 새로운 점은 검증에 있다고 적었습니다. 수학자들은 이 일을 큰 기술적 성과로 보면서도 수학에는 새로 알려 준 것이 없다고 평가합니다.

Anthropic 기술 문서 Formalizing Fermat's Last Theorem in Lean 첫 쪽, 11일 동안 증명한 정리 수 누적 그래프 Anthropic 기술 문서 Formalizing Fermat’s Last Theorem in Lean 첫 쪽, 11일 동안 증명한 정리 수 누적 그래프 — 출처: Anthropic

페르마의 마지막 정리는 무엇이었나

정리는 한 줄입니다. n이 3 이상이면 aⁿ + bⁿ = cⁿ을 만족하는 양의 정수 a, b, c는 없다. n이 2일 때는 3² + 4² = 5²처럼 답이 무수히 많은데, 지수가 하나만 올라가도 답이 하나도 없다는 주장이에요.

페르마는 고대 그리스 수학자 디오판토스의 책 《산술》을 읽다가 여백에 이렇게 적었습니다. 세제곱수를 두 세제곱수로, 네제곱수를 두 네제곱수로, 일반적으로 2보다 큰 거듭제곱을 같은 차수의 두 거듭제곱으로 나눌 수는 없다, 나는 이것의 놀라운 증명을 찾았지만 여백이 좁아 적지 않는다.

1670년판 디오판토스 산술 제2권 8번 문제 아래 실린 페르마의 관찰(OBSERVATIO DOMINI PETRI DE FERMAT) 1670년판 디오판토스 산술 제2권 8번 문제 아래 실린 페르마의 관찰(OBSERVATIO DOMINI PETRI DE FERMAT) — 출처: Wikimedia Commons / Diophantus, Arithmetica 1670년판

이 메모는 페르마가 죽은 뒤 아들이 1670년 여백 메모를 붙여 다시 펴낸 판본으로 세상에 알려졌습니다. 이후 수학자들이 n = 3, 4 같은 개별 지수를 하나씩 풀었지만 모든 n에 대한 증명은 3세기 넘게 나오지 않았어요.

증명은 페르마의 식을 직접 다루는 대신 타원곡선을 거쳤어요. 반례가 있다고 가정하면 그 수로 특별한 타원곡선(elliptic curve), 곧 y² = x³ + ax + b 꼴의 곡선을 하나 만들 수 있고(프라이 곡선), 켄 리벳은 1986년 이 곡선이 모듈러(modular) 성질을 가질 수 없다는 것을 보였습니다.

와일즈는 1993년 반례에서 나오는 종류의 타원곡선은 모두 모듈러라는 것을 증명했다고 발표했고, 그 뒤 발견된 빈틈을 1994년 제자 리처드 테일러와 함께 메워 1995년 논문으로 냈습니다. 모듈러일 수 없는 곡선이 모듈러여야 하니 반례는 없다는 결론이에요.

형식화, 증명을 기계가 읽는 코드로 옮기는 일

Lean은 증명 보조기(proof assistant)입니다. 정의와 논증을 프로그래밍 언어처럼 적어 넣으면 커널이라고 부르는 작은 검사 프로그램이 모든 단계가 규칙에 맞는지 대조하고, 빈 곳이 하나라도 있으면 통과시키지 않아요. 이렇게 옮기는 작업을 형식화(formalization)라고 부릅니다.

사람이 쓴 이번 증명의 목표 명제는 한 줄이었습니다. n ≥ 3이고 a, b, c가 0보다 큰 자연수면 aⁿ + bⁿ ≠ cⁿ. Lean 커뮤니티가 함께 만드는 수학 라이브러리 Mathlib 위에서, 이 한 줄이 참이라는 것을 기계가 끝까지 확인하면 형식화가 끝납니다.

확인 기준은 두 가지입니다. 아직 증명하지 못한 자리를 임시로 메우는 표시인 sorry가 하나도 없어야 하고, 증명이 기대는 공리가 Mathlib이 원래 쓰는 propext·Classical.choice·Quot.sound 셋을 넘지 않아야 해요. 이번 증명은 둘 다 통과했습니다.

AI 가 27년 묵은 수학 난제를 풀었다 — 검증은 누구나 할 수 있다

11일 동안 무슨 일이 있었나

작업은 8월 7일 새벽(미국 동부 시간)에 시작해 17일 밤 10시에 마지막 정리가 닫혔습니다. Claude 에이전트 여럿이 컬럼비아대 Tianyi Peng 연구실이 만든 Prove2Me 플랫폼에서 동시에 일했고, 한 에이전트가 정리 문장을 쓰면 다른 에이전트가 그 문장이 맞게 적혔는지 확인한 뒤 증명에 들어갔습니다.

여러 작업 모듈이 하나의 의존 관계 트리에 조각을 동시에 채워 넣는 개념 컷 여러 작업 모듈이 하나의 의존 관계 트리에 조각을 동시에 채워 넣는 개념 컷 — 출처: 개념 컷 · agy 자가 생성

사람의 몫은 작았습니다. Anthropic 기술 문서는 사람이 가끔 우선순위를 말하거나 격려했을 뿐, 목표 정리 한 줄 말고는 수학도 Lean 코드도 쓰지 않았다고 적었어요.

쓰인 모델은 공개 제품이 아닌 내부 연구 모델로, 성능은 Claude Fable 5.1과 비슷하고 출력 토큰은 약 60억 개를 썼습니다.

첫 시도는 실패했습니다. 최종 코드의 약 7%에 해당하는 초기 작업은 정리 사이의 의존 관계를 관리하는 Prove2Me를 붙이고 나서야 이어졌습니다.

증명 경로는 다몽·다이아몬드·테일러가 1995년에 정리한 와일즈·테일러 논증을 따랐습니다.

날짜 끝낸 단계
1일 차 (8월 7일) 테일러-와일즈 소수의 존재
5일 차 마주르 정리(필요한 경우)
9일 차 아이힐러-시무라 합동 16단계
11일 차 오전 랭글랜즈-터넬 정리(필요한 경우)
11일 차 밤 10시 페르마의 마지막 정리

최종 정리가 기대는 정리는 2만 9,511개, 증명 파일 안의 보조 정리는 약 53만 3,000개, 코드는 약 1,300만 줄(자동 생성된 상용구를 빼면 약 1,050만 줄), 파일은 6만 474개예요. Anthropic은 이 줄 수가 Mathlib 전체의 5~6배라고 했지만, 기술 문서 속 Claude의 평가대로 짜임이 다른 것을 줄 수로 센 값이라 수학의 양을 뜻하지는 않습니다.

어떻게 검산했나

플랫폼이 붙이는 증명됨 표시만으로는 부족했습니다. Prove2Me는 정리마다 따로 컴파일해 바로 아래 정리들의 명제만 믿고 확인하기 때문에, 전체를 한 프로젝트로 묶어도 맞는지는 따로 봐야 해요. 마지막 정리가 닫힌 11일 차 밤, 한 에이전트가 동료에게 과장을 막으려고 독립 재검산 전까지는 형식화가 끝났다고 말하면 안 된다는 답을 보낸 기록도 기술 문서에 실려 있습니다.

다음 날 아침 팀은 2만 9,511개 정리를 플랫폼 밖에서 원본부터 다시 컴파일했고, 이튿날에는 전체를 하나의 Lean 프로젝트로 빌드했습니다. 이 빌드는 최종 정리가 표준 공리 셋 외에 무엇이든 기대거나 sorry가 하나라도 있으면 실패하게 짜여 있어요.

외부 도구 둘을 더 돌렸습니다. Lean 개발 조직이 만든 comparator는 증명된 명제가 Mathlib만 불러온 기준 파일의 명제와 똑같은지 확인하고 증명 전체를 Lean 커널로 처음부터 다시 돌렸고, Rust로 따로 구현한 Lean 커널 nanoda는 선언 105만 2,234개를 오류 없이 통과시켰습니다.

전체 빌드·comparator·nanoda 검산 소요 시간 막대 차트 전체 빌드·comparator·nanoda 검산 소요 시간 막대 차트 — 출처: anthropics/fermats-last-theorem README 기반 자가 렌더

누구나 다시 해 볼 수는 있지만 개인 컴퓨터로는 어렵습니다. 공개 저장소 안내에 따르면 병렬 작업 96개로 빌드에 5시간 32분, 메모리는 최대 153GB를 썼고, comparator는 14시간 46분에 메모리 230GB가 들었어요.

도구가 확인하지 못하는 것도 저장소가 직접 적어 두었습니다. 중간 정리 하나하나가 이름이 말하는 그 내용인지는 기계가 판단할 수 없고, 읽는 사람이 판단할 몫이라고 했어요. 최종 명제만은 comparator가 Mathlib 기준과 같다고 확인했기 때문에, 중간 정의가 어떻든 결론이 약해질 수는 없습니다.

수학자들의 평가, 새로 알려 준 것은 없다

영국 임페리얼 칼리지 런던의 Kevin Buzzard는 2024년 10월부터 영국 공학·물리과학 연구위원회(EPSRC) 지원을 받아 5년 계획으로 페르마의 마지막 정리를 사람 손으로 형식화해 온 사람입니다. Anthropic 발표 당일 올린 블로그 글의 제목은 Anthropic has beaten me to it이었어요.

Kevin Buzzard의 Xena Project 블로그 글 제목과 수학적으로는 새로 알려 준 것이 없다고 쓴 문단 Kevin Buzzard의 Xena Project 블로그 글 제목과 수학적으로는 새로 알려 준 것이 없다고 쓴 문단 — 출처: Xena Project / Kevin Buzzard (하이라이트 추가)

그는 이번 결과가 수학적으로는 거의 아무것도 알려 주지 않는다고 적었습니다. 자신은 와일즈 증명이 맞다고 99.9% 확신한다고 이미 밝혔고 정수론 학계 대부분은 100% 확신하는데, 이번 형식화는 초기 문헌을 충실히 따랐을 뿐 거기에 더한 것이 없다는 이유예요.

경로도 다릅니다. Buzzard의 프로젝트는 리처드 테일러가 설계한 현대적 경로를 따르며, 사람이 읽고 다시 쓸 수 있는 라이브러리를 Mathlib 기준에 맞춰 조금씩 올리는 방식입니다. 그는 자신의 연구비가 무의미해지지 않는다고 했는데, 약속한 결과물이 형식화 자체보다 현대 정수론의 기본 개념을 Mathlib에 넣는 일에 가깝기 때문이라고 설명했어요.

기계가 쓴 증명이 어떤 상태인지는 기술 문서에 실린 Claude의 자기 평가가 가장 자세합니다. 증명 속 리벳·와일즈·마주르·랭글랜즈-터넬 정리는 이 논증에 필요한 만큼으로 좁힌 버전이라, 저장소 문서도 이것을 일반 정리의 형식화로 인용하면 안 된다고 적었어요.

기계가 쓴 증명의 한계

Claude는 자기 증명이 Mathlib에 들어가기 어려운 이유를 넷으로 들었습니다. 수학으로 읽을 수 없고, 일반적이지 않고, 같은 내용이 파일마다 반복되고, 쉽게 깨지면서 비싸다는 것이에요.

증명 파일의 중복·상용구·버전 업 영향 비율 막대 차트 증명 파일의 중복·상용구·버전 업 영향 비율 막대 차트 — 출처: Anthropic, Formalizing Fermat’s Last Theorem in Lean (2026) 기반 자가 렌더

[읽을 수 없다] 주석 없이 공개됐고 보조 정리 이름이 기계식이며, Mathlib 상한 1,500줄을 넘는 파일이 900개 이상(Mathlib 전체는 2개)

[반복된다] 정리 문장 다섯 중 둘이 다른 파일과 글자까지 같고, 기본 보조 정리 하나가 300개 넘는 파일에 따로 선언됨

[쉽게 깨진다] Lean 4.30에서 4.33으로 올리자 증명 파일의 26%가 바뀌고 19%는 하나씩 손봐야 했음

[비싸다] 깨끗한 빌드에 96코어·메모리 512GiB로 5시간 52분

Mathlib 쪽 사정도 있습니다. 2026년 중반 기준 검토를 기다리는 요청이 2,600건이 넘어, Mathlib 기여 안내는 빨리 움직이려는 프로젝트에 별도 저장소를 권하고, 저장소 README도 이 증명을 연구 결과물로만 두고 유지 보수나 기여는 받지 않는다고 밝혔어요.

비용은 공개되지 않았습니다. 출력 토큰 60억 개를 공개 API 단가로 계산하면 약 4억 200만 원(30만 달러)이라는 추정이 Buzzard 블로그 댓글과 매체에 돌았지만, 내부 모델이라 실제 비용은 다를 수 있습니다. 비교하자면 Buzzard의 5년 연구비는 약 18억 2,000만 원(100만 파운드)이에요.

앞으로 무엇이 달라지나

Buzzard가 본 변화는 속도 쪽입니다. 수천 쪽의 문헌을 AI 에이전트 여럿이 11일 만에 끝까지 형식화할 수 있다면, 앞으로는 새 연구 논문을 쓰는 동시에 형식화하는 일이 생기고 기존 문헌의 빈틈과 오류도 기계로 샅샅이 확인할 수 있다는 것이에요. 그는 사람이 다듬는 Mathlib과 AI가 만든 라이브러리가 따로 커 가고, AI 쪽이 훨씬 많은 수학을 담게 되겠지만 틀린 정의나 거친 증명이 섞일 수 있다고 내다봤습니다.

필요한 규모도 작아지고 있습니다. Anthropic은 같은 플랫폼에서 개인용 Claude Max 구독 세 개로 비노그라도프의 세 소수 정리(충분히 큰 홀수는 소수 셋의 합)를 사흘 만에 형식화했다고 밝혔습니다.

Claude는 한국 원화 정가 없이 달러 정가만 공개하는데, Max는 월 약 13만 4,000원(100달러)부터 시작하고 표시 가격에 세금이 빠져 있어요. 가장 낮은 단계 셋이면 월 약 40만 2,000원(300달러)에 부가세 10%가 더해지며, 어느 단계를 썼는지는 공개되지 않았습니다.

국내 연구 기관이 이런 대규모 형식화에 참여한다는 공개 발표는 확인되지 않았습니다. Anthropic은 순수 수학·형식화를 연구하는 외부 연구자에게 무료·할인 구독과 연구 크레딧, 큰 과학 프로젝트용 연구비를 제공한다고 밝혔고, 발표문에 국가 조건은 따로 적혀 있지 않습니다.

정리

페르마의 마지막 정리 Lean 형식화 정리 카드 페르마의 마지막 정리 Lean 형식화 정리 카드 — 출처: Anthropic·Xena Project 기반 자가 렌더

358년 걸려 사람이 찾은 증명을 기계가 11일 만에 옮겨 적은 사건이고, 그 결과가 맞다는 확신은 이제 커널 검사 두 번과 비교 도구 하나가 받쳐 줍니다.

참고 출처