클로드, 페르마의 마지막 정리 형식화 (9월 5일) — 11일에 1,300만 줄
Anthropic announced on September 5, 2026 that Claude had produced the first end-to-end, machine-checked proof of Fermat's Last Theorem in the Lean proof assistant, working largely autonomously over eleven days. The run generated about 13 million lines of Lean code, proved 30,300 theorems of which 29,500 were used in the final proof, and consumed roughly six billion output tokens. The first attempt failed; the run succeeded only after a harness built on Prove2Me — an open-source platform from a Columbia University group led by Anthropic researcher Tianyi Peng — was added mid-run. Anthropic is explicit that the result rests on community infrastructure it did not build: Kevin Buzzard's Fermat's Last Theorem formalization project at Imperial College London, and Mathlib, Lean's mathematics library. The distinction that matters is between discovering a proof and formalizing one. Andrew Wiles proved the theorem in 1994; what Claude did was translate that proof into a form a computer can verify line by line, a task experts had expected to take many years
앤스로픽이 2026년 9월 5일 클로드가 페르마의 마지막 정리를 Lean 증명 보조기에서 처음으로 끝까지 형식화했다고 발표했다. 기계가 한 줄씩 검증할 수 있는 형태의 완전한 증명이 나온 것은 처음이다. 작업은 11일 동안 대체로 자율적으로 진행됐고, 그 사이 약 1,300만 줄의 Lean 코드가 생성됐다. 증명된 정리는 3만 300개였고 그중 2만 9,500개가 최종 증명에 쓰였다. 출력 토큰은 약 60억 개가 들었다. 첫 시도는 실패했고, 컬럼비아대 연구진이 만든 오픈소스 도구 Prove2Me 기반 하네스를 작업 도중 추가한 뒤에야 완주했다. 앤스로픽은 이 결과가 자기들이 만들지 않은 공동체 인프라 위에 서 있다고 명시했다 — 임피리얼칼리지 케빈 버자드의 페르마 정리 형식화 프로젝트와 Lean의 수학 라이브러리 Mathlib이다. 여기서 구분해야 할 것이 하나 있다. 정리를 증명한 사람은 1994년의 앤드루 와일스다. 클로드가 한 일은 그 증명을 기계가 검증할 수 있는 형태로 옮긴 것이다
3줄 요약
- 결과 — 페르마의 마지막 정리를 Lean에서 처음으로 끝까지 기계검증 가능한 형태로 형식화. 11일, 대체로 자율
- 규모 — Lean 코드 약 1,300만 줄, 증명한 정리 3만 300개(최종 사용 2만 9,500개), 출력 토큰 약 60억
- 구분 — 증명한 것은 1994년 와일스다. 이번 작업은 그 증명을 기계가 한 줄씩 검증하는 형태로 옮긴 것이다
핵심 질문
- 클로드가 페르마의 마지막 정리를 증명한 건가
- **아니다. 증명한 사람은 1994년의 앤드루 와일스이고, 클로드가 한 일은 그 증명의 형식화다.** 이 구분은 기사 제목만 보면 자주 뒤집히므로 먼저 정리해 둘 필요가 있다. | 구분 | 누가 | 무엇을 | |---|---|---| | **증명(proof)** | 앤드루 와일스 (1994년) | 사람이 읽는 수학 논증을 만들었다 | | **형식화(formalization)** | 클로드 (2026년) | 그 논증을 **기계가 한 줄씩 검증**할 수 있는 코드로 옮겼다 | **그렇다고 형식화가 단순 번역인 것도 아니다.** 사람의 논문은 "명백하다", "유사하게", "자세한 것은 생략한다" 같은 표현으로 수많은 단계를 건너뛴다. 형식화는 그 생략된 단계를 **하나도 빠짐없이 채워 넣는 일**이다. 페르마의 마지막 정리처럼 와일스의 논문만 100쪽이 넘고 그 아래 20세기 정수론 상당 부분이 깔려 있는 경우, 채워야 할 칸이 수만 개가 된다. **이번 작업에서 증명된 정리가 3만 300개였다는 숫자가 그 규모다.** 형식 증명이 왜 필요한지는 따로 정리한 적이 있다(「형식 증명이란」).
- 어떻게 11일 만에 됐나
- **세 가지가 이미 있었고, 하나가 도중에 추가됐다.** | 요소 | 만든 곳 | 역할 | |---|---|---| | **Mathlib** | Lean 공동체 | 수학 라이브러리. 기초 정리들이 이미 형식화돼 있다 | | **버자드 FLT 프로젝트** | 임피리얼칼리지 케빈 버자드 | 페르마 정리 형식화의 설계도와 진행분 | | **Lean** | Lean 개발자들 | 증명 보조기 자체 | | **Prove2Me** | 컬럼비아대 (톈이 펑 그룹) | **작업 도중 추가된 하네스** | **앤스로픽이 이 목록을 스스로 밝혔다는 점이 중요하다.** 회사는 이 성과가 자기들이 만들지 않은 공동체 인프라 위에 서 있다고 명시했다. **즉 '클로드가 혼자 해냈다'가 아니라 '수년간 사람들이 깔아둔 길 위를 클로드가 11일에 달렸다'가 정확한 서술이다.** 그리고 **첫 시도는 실패했다.** 완주는 Prove2Me 기반 하네스를 중간에 붙인 뒤에야 이뤄졌다. 톈이 펑은 앤스로픽 소속 연구자이면서 컬럼비아대 그룹을 이끄는 인물이다.
- 60억 토큰은 얼마나 되는 양인가
- **상업 API 가격으로 환산하면 규모가 보인다.** 출력 100만 토큰에 20달러대인 최근 프런티어 모델 가격을 그대로 대입하면(「GPT-5.6 Sol API 가격 인하 (8월 21일)」·「AI 토큰 가격이란」), **60억 토큰 × 20달러/100만 = 약 12만 달러**다. 실제로는 앤스로픽이 자사 모델을 자체 인프라에서 돌렸으므로 이 값은 청구액이 아니라 **"바깥에서 같은 일을 하려면 대략 이 정도"** 라는 눈금이다. | 항목 | 값 | |---|---| | 기간 | **11일** | | 생성된 Lean 코드 | 약 **1,300만 줄** | | 증명된 정리 | **30,300개** (최종 사용 **29,500개**) | | 출력 토큰 | 약 **60억 개** | | 상업 가격 환산(참고) | 약 **12만 달러** 수준 | **주목할 비율은 30,300 대 29,500이다.** 증명한 정리의 **97.4%가 최종 증명에 실제로 쓰였다.** 헛돈 작업이 2.6%뿐이었다는 뜻인데, 이는 목표에서 역으로 필요한 보조정리를 뽑아 내려가는 방식이 작동했음을 시사한다. 다만 **'800개가 안 쓰였다'는 것이 낭비였는지 탐색의 정상 비용이었는지는 공개 자료로 판단할 수 없다.**
"AI가 페르마의 마지막 정리를 증명했다"는 문장은 틀렸다. 증명한 사람은 1994년의 와일스다. 이번에 일어난 일은 다른 것이고, 그 다른 것이 더 흥미롭다.
1. 무엇이 있었나
앤스로픽은 2026년 9월 5일, 클로드가 페르마의 마지막 정리를 Lean 증명 보조기에서 처음으로 끝까지 형식화했다고 발표했다.
| 항목 | 값 |
|---|---|
| 기간 | 11일 (대체로 자율) |
| 생성된 Lean 코드 | 약 1,300만 줄 |
| 증명된 정리 | 30,300개 |
| 최종 증명에 사용 | 29,500개 (97.4%) |
| 출력 토큰 | 약 60억 개 |
2. 증명과 형식화는 다르다
| 구분 | 누가 | 무엇을 했나 |
|---|---|---|
| 증명 | 앤드루 와일스 (1994) | 사람이 읽는 수학 논증 |
| 형식화 | 클로드 (2026) | 기계가 한 줄씩 검증하는 코드 |
그렇다고 형식화가 받아쓰기인 것은 아니다. 사람의 논문은 "명백하다", "유사하게", "자세한 것은 독자에게 맡긴다" 로 단계를 건너뛴다. 형식화는 그 건너뛴 칸을 전부 채우는 일이다.
와일스의 논문은 100쪽이 넘고, 그 아래에 20세기 정수론의 상당 부분이 전제로 깔려 있다. 채워야 할 칸이 3만 개였다는 것이 이번 숫자의 의미다. 형식 증명이 왜 필요한 장치인지는 따로 정리한 적이 있다(「형식 증명이란」).
3. 클로드 혼자 한 것이 아니다
앤스로픽은 이 결과가 자기들이 만들지 않은 인프라 위에 서 있다고 스스로 밝혔다.
| 요소 | 만든 곳 | 역할 |
|---|---|---|
| Lean | Lean 개발 공동체 | 증명 보조기 |
| Mathlib | Lean 공동체 | 수학 라이브러리 — 기초 정리가 이미 형식화돼 있다 |
| FLT 프로젝트 | 임피리얼칼리지 케빈 버자드 | 페르마 정리 형식화의 설계도와 기존 진행분 |
| Prove2Me | 컬럼비아대 톈이 펑 그룹 | 첫 시도 실패 뒤 도중에 붙인 하네스 |
첫 시도는 실패했다. 완주는 Prove2Me 기반 하네스를 중간에 추가한 다음에 이뤄졌다. 회사가 이 실패와 외부 의존을 함께 공개했다는 점은, AI 성과 발표에서 흔한 방식이 아니다.
4. 왜 이 일이 중요한가
AI가 만든 수학을 사람이 다 읽지 않고도 믿을 수 있게 하는 경로이기 때문이다. AI가 수학 미해결 문제를 건드렸을 때 매번 따라온 질문이 "이걸 누가 검증하나" 였다(「AI가 수학 미해결 문제 10개를 건드렸다」). 형식 증명은 그 질문에 기계로 답한다. Lean이 통과시켰다면, 사람이 그 코드를 읽지 않아도 논리적으로 빈 칸이 없다는 뜻이다.
그리고 속도의 의미가 있다. 전문가들은 이 형식화가 여러 해 걸릴 일로 봤다. 11일은 그 예상과 자릿수가 다르다. 다만 11일은 인프라가 이미 깔린 상태에서의 11일이다. Mathlib과 버자드 프로젝트에 들어간 시간은 이 숫자에 포함돼 있지 않다.
5. 남은 것과 확인되지 않은 것
- 앤스로픽 기술 보고서 원문을 직접 대조하지 못했다. 수치는 보도 인용값이다.
- "대체로 자율적"의 범위가 명확하지 않다. 사람이 몇 번, 어떤 성격으로 개입했는지 요약에 없다.
- 외부 수학자의 독립 검토 여부와 Mathlib 병합 계획을 확인하지 못했다.
- 60억 토큰의 비용 12만 달러는 이 기사의 추정치다. 회사가 밝힌 값이 아니다.
- 발표일이 매체에 따라 9월 4일과 5일로 갈린다. 공식 게시 시각을 특정하지 못했다.
- 같은 주에 오픈AI는 자사 모델의 감시 가능성이 떨어졌다고 적었다(「GPT-6 아스트라 시스템 카드」). 한쪽에서는 AI의 논증을 기계로 검증하는 길이 열렸고, 다른 쪽에서는 AI의 사고 과정을 사람이 읽지 못하게 됐다. 같은 주의 두 소식이다.
출처
- Anthropic — Formalizing Fermat's Last Theorem
- Anthropic — Formalizing Fermat's Last Theorem in Lean (기술 보고서 PDF)
- SiliconANGLE — Anthropic uses Claude to formalize proof of Fermat's Last Theorem
- AI Weekly — Claude formalized Fermat's Last Theorem in 11 days: Anthropic
- AI Weekly — Anthropic's Claude formalizes Fermat's Last Theorem in Lean