무엇인가
2026년 9월 Anthropic이 공개한 페르마의 마지막 정리(FLT)의 완전한 Lean 4 형식 증명 저장소입니다. Claude 에이전트 수십 개가 8월 7일부터 17일까지 11일 동안 대체로 자율적으로 작업해, 최종 정리가 의존하는 29,511개 정리를 Mathlib 위에서 증명했습니다. 코드는 약 1,300만 줄로 Mathlib 전체의 5배가 넘습니다.
FLT는 1995년 와일스(와 테일러–와일스)가 이미 증명했습니다. 이번에 새로운 것은 그 증명을 커널이 한 단계도 빠짐없이 확인할 수 있는 형태로 옮긴 일입니다. 사람의 증명은 "자명하다"며 계단을 건너뛰고, 129쪽짜리 와일스 논문도 검증에 몇 달이 걸리고 그 과정에서 구멍이 발견됐습니다. Lean은 모든 계단을 직접 밟아 봅니다. 증명 경로는 다르몽–다이아몬드–테일러 해설을 따라 프레이 곡선 → 마주르(기약성) → 와일스(모듈러성, R = T) → 리벳(레벨 낮추기) → 레벨 2에서 모순으로 갑니다.
어떻게 동작하나
성공의 열쇠는 모델보다 하네스였습니다. 첫 시도는 에이전트들이 프로젝트 상태를 놓치고 협업을 멈춰 실패했고, 두 번째는 컬럼비아대의 오픈 플랫폼 Prove2Me(arXiv:2608.28433) 위에서 진행됐습니다.
8월 17일 밤 마지막 잎이 닫히자 연쇄가 루트까지 올라갔습니다. 그래도 에이전트는 "재검사가 끝나기 전까지 정직한 문장은 'FLT가 형식화되었다'가 아니라 'prove2me에서 증명됨, 독립 재검사 대기 중'이다"라고 보고했고, 이후 플랫폼 밖 재컴파일과 두 개의 독립 검사기를 거쳤습니다.
빠른 시작
저장소의 목표 문장은 Lean 내장 자연수와 연산만으로 쓰여 있습니다.
theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
(ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a ^ n + b ^ n ≠ c ^ n
기본 빌드 목표 FinalCheck.lean은 #print axioms 출력이 정확히 표준 공리 셋(propext, Classical.choice, Quot.sound)이 아니면 실패하므로 sorry·새 axiom·native_decide가 끼어들 수 없습니다. 직접 확인하려면 README의 명령을 씁니다(Linux 또는 macOS, elan 필요).
git clone https://github.com/anthropics/fermats-last-theorem flt && cd flt
LEAN_NUM_THREADS=96 lake build # 병렬 작업 하나당 메모리 약 5 GB
verification/comparator/run.sh # Lean FRO의 comparator로 문장·공리·전체 재생 검사
verification/nanoda/run.sh # 러스트로 독립 구현한 커널 nanoda로 재검사
빌드는 96 병렬에서 5시간 32분, 최대 메모리 153 GB였고, comparator는 약 15시간(최대 230 GB, README는 300 GB 확보 권장)이 걸립니다. 증명을 읽기만 하려면 html/index.html을 브라우저로 열거나 공개 문서 사이트를 보면 됩니다. 29,511개 정리마다 Lean 문장, 인용 관계, 의존 그래프가 있고, PROOF-PATH.md가 각 단계의 Lean 정리 이름과 "여기서 증명된 고전 결과가 정확히 얼마나 강한지"를 적어 둡니다.
언제 쓰고, 언제 피하나
- 잘 맞는다: 대규모 형식화를 에이전트로 쪼개는 구조(불변 문장, 스케치, 감사 표면 고정)를 연구하거나 따라 할 때. AI가 낸 증명을 "커널을 통과시켜라"로 검증하는 파이프라인을 설계할 때. 같은 구조는 소프트웨어(인터페이스를 먼저 고정하고 모듈별 검증)에도 옮겨진다.
- 다른 방법을 먼저 본다: 사람이 읽고 재사용할 라이브러리가 필요하면 임페리얼 칼리지 FLT 프로젝트(2024~2029)와 Mathlib이 기준이다. 이 저장소는 README 스스로 "읽기보다 검사를 위해 쓰였다"고 밝힌 연구 산출물이고 유지보수·기여를 받지 않는다.
한계와 주의
- 수학으로 읽을 수 없다. 이름은 기계가 지었고 주석은 지워졌으며, 1,500줄을 넘는 파일이 900개 이상이다(Mathlib 전체엔 2개). 이름과 문장이 어긋나면 증명된 것은 문장이다.
- 일반 정리가 아니다. '마주르', '리벳', '와일스', '랭글랜즈–터널'이 모두 이 논증에 필요한 제한 버전이다. 일반 고전 정리의 형식화로 인용하면 안 된다.
- 중복과 취약성. 정리 문장 약 5개 중 2개가 다른 파일과 글자까지 같고, 툴체인 한 번 업데이트(Lean 4.30→4.33)에 파일 19%가 개별 수리를 요구했다.
- 기계가 못 보는 것. 커널은 "증명이 문장에 맞는가"를 보증하지만 중간 정리가 이름대로의 뜻인지는 사람의 몫이다. 최종 문장은 초등적이고 comparator가 Mathlib 표준 문장과의 동일성을 확인했으므로 결론은 약해지지 않는다.
- "사람은 목표 문장 한 줄만 썼다"의 정확한 뜻. 실행 중 사람이 쓴 수학·Lean은 그것뿐이지만, 저장소
ATTRIBUTION.md는 106개 파일이 임페리얼 FLT 프로젝트와 flt-regular의 사람이 쓴 오픈소스 코드에서 왔다고 밝힌다. - 줄 수는 공개 글 기준 1,300만, Claude의 자체 평가 기준 1,350만으로 출처마다 조금 다르다.
