무슨 일인가요
Anthropic은 9월 4일 연구 글에서 Claude가 11일 만에 페르마의 마지막 정리(FLT)에 대한 최초의 완결된 컴퓨터 검증 증명을 Lean으로 썼다고 발표했습니다. 공식 쓰인 모델은 "Claude Fable 5.1과 대략 비슷한 범용 내부 연구 모델"이고, 출력 토큰을 약 60억 개 소비했습니다. 공식 결과물은 Lean 코드 1,300만 줄로 Mathlib의 5배가 넘으며, 최종 증명에 쓰인 중간 정리가 29,500개, 과정에서 증명한 정리는 30,300개입니다. 공식 증명은 Wiles의 증명을 단순화한 Darmon·Diamond·Taylor의 해설을 따릅니다. 공식
60억
증명에 쓴 출력 토큰
Claude 에이전트 수십 개가 Prove2Me 플랫폼에서 11일간 협업 (Anthropic, 2026-09-04)
사람의 수학적 개입은 "Tianyi Peng의 가끔 있는 상위 지시"로 제한됐고, Anthropic은 예시로 "스킴으로서의 야코비안이 우선순위가 높아 보인다" 같은 지시를 들었습니다. 공식 작업은 Peng과 Columbia 대학교 협력자들이 만든 오픈 협업 플랫폼 Prove2Me에서 이뤄졌습니다. 정리 문장을 방향 그래프(DAG)로 두어 에이전트들이 일을 나누고, 정리문과 증명을 다른 파일로 분리하며, 자연어 설명으로 기존 정리를 검색해 재사용하는 구조입니다. 공식 로그에는 "The FLT root reads PROVED on prove2me at 02:00:57Z Aug-18"이라는 Claude의 메모가 남아 있습니다. 공식
검증은 어떻게 했나요
공개 저장소의 정리문은 a ^ n + b ^ n ≠ c ^ n(n은 3 이상, a·b·c는 양의 자연수)이고, 의존하는 공리는 Lean의 표준 공리 세 개(propext, Classical.choice, Quot.sound)뿐입니다. 공식 sorry, 추가 axiom, native_decide, unsafe 코드는 없습니다. 공식 Lean 4.33.1과 Mathlib v4.33.0을 쓰고, 모듈 60,475개 가운데 106개 파일은 Imperial College London FLT 프로젝트와 flt-regular 프로젝트에서 가져왔습니다. 공식
| 검증 방법 | 무엇을 확인하나 | 소요 시간 | 자원 |
|---|---|---|---|
| lake build (Lean 커널) | 모든 선언을 처음부터 컴파일 | 약 5.5시간 (96 병렬) | 디스크 약 67GB |
| comparator v4.33.0 | 증명한 문장이 Mathlib의 FLT 문장과 같은지 | 14시간 46분 | 최대 메모리 230GB |
| nanoda 0.4.13 (독립 Rust 커널) | 1,052,234개 선언 재검사 | 약 30분 (16 스레드) | 약 40GB |
세 방법 모두 저장소에 스크립트로 들어 있고, nanoda의 판정은 "Checked 1,052,234 declarations with no errors"였습니다. 공식
수학자는 어떻게 보나요
Imperial College London의 Kevin Buzzard는 증명을 검토했고, Anthropic 글에서 "수학의 공리 외에는 어떤 가정도 없이 페르마의 마지막 정리를 증명한 놀라운 자동 형식화 성과"라고 평했습니다. 공식 같은 날 자신의 블로그 글 "FLT: Anthropic has beaten me to it"에서는 선을 분명히 그었습니다. "수학적으로 이 작업은 본질적으로 아무것도 알려주지 않는다. 나는 FLT 증명이 옳다고 99.9% 확신한다고 공언해 왔다"는 것입니다. 보도 그는 코드가 1,340만 줄이 넘고 컴파일이 Mathlib보다 20배 오래 걸리며, 형식화가 "초기 문헌을 충실히 따랐을 뿐 더한 것이 없다"고 썼습니다. 보도 그럼에도 "수천 페이지의 문헌이 11일 만에 AI 군집에 의해 끝까지 형식화될 수 있다면, 앞으로 현대 연구의 형식화가 실시간으로 이뤄지는 것을 보게 될 것"이라고 했습니다. 보도 Buzzard가 이끄는 Imperial 프로젝트는 Khare·Wintenberger와 Kisin의 연구를 반영한 현대적 증명을 청사진과 함께 형식화하는 것이 목표이며, 그는 이 작업을 계속하겠다고 밝혔습니다. 공식
Anthropic도 한계를 적었습니다. 초기에 프로젝트 상태를 놓친 에이전트들의 실패한 시도가 최종 증명의 비상용구 줄 가운데 약 7%를 차지하고, 증명은 "필요한 것보다 훨씬 길 것"이며, 전체가 토큰 집약적인 프로젝트였다는 것입니다. 공식 글은 "리만 가설에 대한 최근 AI 작업이 새로운 수학을 만든 것과 달리, 여기서 새로운 것은 검증"이라고 못 박습니다. 공식
무엇을 보면 되나요
- 형식 검증 연구자: 저장소는 Apache 2.0이고 390MB 규모의 오프라인 문서에 의존 그래프가 붙어 있습니다. 이름이 기계 생성이라 읽기보다 검증에 맞춰져 있습니다. 공식
- 에이전트 개발자: Prove2Me 논문(arXiv 2608.28433)이 "미션" 단위로 사람과 에이전트가 증명을 쌓아 올리는 구조를 설명합니다. 논문
- 지켜볼 것: 이 코드가 Mathlib 기여로 이어질지, 다른 대형 정리에 같은 방식이 재현되는지.
