페르마 마지막 정리, Lean으로 종단 검증

11일·1300만 줄 형식화…새 증명이 아니라 기존 논증의 기계 검사본

2026년 9월 4일 앤트로픽은 내부 연구용 클로드가 Lean 4로 페르마 마지막 정리(FLT)의 종단 컴퓨터 검증 증명을 만들었다고 발표했다. 작업 기간은 약 11일, 산출물은 약 1300만 줄 Lean 코드와 최종 증명에 쓰인 약 2만 9500개 보조 정리였다. 이는 1637년 페르마의 주장이나 1995년 앤드루 와일스의 증명을 새로 만든 것이 아니라, 이미 성립한 논증을 증명 보조 언어로 옮겨 커널이 한 줄씩 검사할 수 있게 한 형식화다.

확인된 사실

무엇이 끝났는가

선언문은 Mathlib의 FLT와 같은 내용이다. 자연수 $n\ge 3$ 과 양의 정수 $a,b,c$ 에 대해 $a^n+b^n\neq c^n$ .
Lean 4.33.1과 Mathlib v4.33.0 위에서 lake 전체 빌드가 통과했다. 저장소 모듈은 6만 475개다.
leanprover/comparator가 Mathlib만 쓰는 도전 선언과 증명이 같고, 추가 공리가 없다고 확인했다.
독립 커널 nanoda가보내기된 환경을 오류 없이 재검사했다.
의존 공리는 Lean 표준 세 개(propext, Classical.choice, Quot.sound)뿐이다. sorry나 외부 결정 우회는 없다고 저장소가 명시한다.

규모

앤트로픽: Lean 약 1300만 줄, 증명된 정리 3만 300개, 최종 증명에 사용된 정리 2만 9500개.
저장소 HTML 안내: 정리 2만 9511개, 정의 모듈 1450개, 인용 간선 10만 6853개.
케빈 버저드(임페리얼 칼리지 런던)는 코드를 직접 컴파일했고 줄 수를 1340만 줄 이상으로 적었다. 96코어 기기에서 Mathlib보다 컴파일이 약 20배 길다고 했다.
출력 토큰은 약 60억. 모델은 공개 제품명이 아니라 내부 연구 모델이며, 회사는 클로드 페이블 5.1과 대략 비슷한 수준이라고 적었다.

어떻게 돌렸는가

콜롬비아대 톈이 펑 그룹이 만든 형식화 플랫폼 Prove2Me와 클로드 코드 기반 다중 에이전트 하네스를 썼다.
Prove2Me는 정리 의존 관계를 DAG로 유지하고, 정리 선언과 증명을 파일로 분리해 컴파일을 줄이며, 자연어 요약을 붙여 검색·재사용을 돕는다.
초기 시도는 프로젝트 상태를 놓치고 협업이 끊겨 실패했다. 실패한 가지가 최종본 비서식 줄의 약 7%를 남겼다.
인간 입력은 펑이 가끔 준 상위 지시로 설명된다. 예: 야코비안을 스킴으로 다루는 일을 우선하라, 마주르 정리를 빨리 끝내라.

수학적으로 무엇을 옮겼는가

경로

증명은 와일스–테일러–와일스 논증을 1995년 다르몽–다이아몬드–테일러가 정리한 해설을 따른다. 프레이 곡선, 세르 추측의 관련 부분, 리베의 레벨 내리기, 랭글랜즈–터널, 모듈러성 올림이 뼈대다. 버저드가 EPSRC 지원으로 진행 중인 임페리얼 FLT 프로젝트의 현대 경로(카레–윈텐베르거·테일러 계열)와는 다르다.

직접 커버 범위

버저드에 따르면 이 저장소의 핵심 논증은 소수 지수 $p\ge 17$ 에서 작동한다. 홀수 정규 소수 경우는 기존 flt-regular(베스트–버크벡–브라스카–로드리게스 등)가 이미 Lean으로 다뤘고, 가장 작은 비정규 소수가 37이므로 전체 FLT로 붙일 수 있다. 저장소도 임페리얼 FLT 프로젝트, flt-regular, Mathlib 일부를 Apache-2.0로 인용한다고 적는다.

새 수학이 아닌 이유

와일스 증명의 오류를 찾거나 더 짧은 초등 증명을 낸 작업이 아니다. 버저드는 “수학적으로 이 작업이 알려 주는 것은 본질적으로 없다. 초기 문헌을 충실히 따른 형식화”라고 썼다. 동시에 그는 코드를 빌드·비교기 검사까지 했고, 자동 형식화 성과 자체는 “수학 공리 외 가정 없이 FLT를 증명한다”고 평가했다.

왜 규모가 논점이 되는가

Mathlib와의 비교

앤트로픽은 이 증명이 Mathlib보다 5배 이상 길다고 했다. 각주도 Mathlib은 짧고 검토된 라이브러리인 반면, 이번 코드는 필요 이상으로 길 가능성이 높다고 인정한다. 긴 코드가 커널을 통과했다는 사실과, 커뮤니티 라이브러리로 쓸 수 있는 코드라는 사실은 별개다. 저장소는 연구 산출물이며 유지보수·기여를 받지 않는다.

벤치마크로서의 의미

버저드는 이번 결과가 프리크 비데이크의 ‘형식화 100정리’ 목록에서 마지막 항목을 채웠다고 적었다. 이 목록은 약 20년간 증명 보조계의 공통 목표였다. 목록 완료와 현대 연구 문헌 전체의 형식화는 난이도가 다르다. 후자는 정의 체계를 Mathlib에 넣는 일과 사람용 해설을 같이 요구한다.

반응을 가르는 지점

형식검증·정수론 쪽

커널·비교기·제3 커널까지 통과한 종단 FLT는 이전에는 없었다.
대수, 조화해석, 기하, 정수론 조각을 한 캠페인 안에서 쌓아 올린 점이 평가 대상이다.
버저드는 자동 형식화가 가능해지면 문헌 오류 점검과 심사 부담 완화, LLM이 만든 수학의 기계 검사로 이어진다고 봤다.
같은 글에서 그는 EPSRC 과제가 끝난 것은 아니라고 했다. Mathlib 반영, 현대 경로, 사람이 탐색할 수 있는 동적 문서는 남아 있다.

일반 기술 보도

“AI가 페르마를 증명했다”는 문장이 먼저 퍼진다. 정확한 문장은 “와일스 계열 증명을 기계가 재검사할 수 있는 형태로 옮겼다”이다. 두 문장의 차이가 토론의 핵심이다.

회의 측에서 나오는 질문

‘거의 자율’의 개입 비율, 실패한 가지 수, 재시도 비용은 논문 수준으로 공개되지 않았다.
임페리얼 FLT와 flt-regular의 스캐폴딩 없이 같은 기간에 끝났는지는 비교 실험이 없다.
1300만 줄은 검증 가능성과 유지 가능성을 동시에 보여 준다. 컴파일 시간과 저장소 탐색 비용이 이미 병목이다.
쇼케이스성 대형 과제라는 지적과, 커널이 통과한 산출물이라는 지적은 같이 성립한다.

에이전트와 인프라

모델만으로 설명되지 않는 부분

초기 다중 에이전트는 상태를 잃고 멈췄다. 전환점은 Prove2Me의 과제 그래프, 선언·증명 분리, 재사용 가능한 정리 목록이다. 장기 에이전트 실험에서 흔히 나오는 패턴이다. 추론 능력과 작업 메모리·스케줄러를 나눠 봐야 한다.

비용

60억 출력 토큰은 연구 예산 규모의 한 런이다. 회사는 별도 소규모 실험으로 개인 클로드 맥스 구독 3개를 써서 3일 만에 비노그라도프 삼소수 정리를 형식화했다고 적었다. 대형 기념비 과제와 중간 규모 정리가 같은 파이프라인에 올라올 수 있는지가 다음 관측 포인트다.

산업·연구로 옮길 때

바로 옮기기 쉬운 것

이미 증명된 논증, 규격, 프로토콜을 기계 검사 가능한 형태로 옮기는 일이다. 수학 문헌, 암호 구현, 타입 안전한 API, 규제 문서의 ‘이 주장이 저 공리·저 스펙에서 따라오는가’가 같은 종류다. Lean FRO 쪽 연대기에도 수학 형식화와 소프트웨어·암호 검증이 한 줄에 적혀 있다.

바로 옮기기 어려운 것

열린 추측을 푸는 일, 짧은 새 아이디어를 내는 일, 라이브러리 품질의 정의를 커뮤니티 표준에 맞게 다듬는 일이다. 2026년 8월 앤트로픽이 리만 제타 영점 비율 하한을 올린 작업은 ‘기존 문헌 위에서의 개선 + Lean 검증’에 가깝고, 이번 FLT는 ‘고전 증명의 완결 이식’에 가깝다. 둘을 한 능력으로 묶으면 과장이 된다.

수학 커뮤니티에 남는 일

이번 코드를 Mathlib 스타일로 줄이고 일반 정의만 업스트림할 주체
현대적 FLT 경로의 형식화와 교육용 문서
AI가 쓴 증명을 사람이 읽을 수 있게 재서술하는 도구

버저드는 앤트로픽이 이 후속 작업을 할 가능성은 낮다고 봤다. 목표가 종단 형식화에 맞춰져 있기 때문이다.

정리하면

이번 발표의 검증 가능한 핵은 세 문장이다.

와일스 계열 FLT 논증의 종단 Lean 증명이 커널과 비교기와 제3 커널을 통과했다.
산출 규모는 현재 Lean 생태계에서 이례적으로 크고, 코드 품질·유지보수·인간 가독성은 별 문제다.
장기 에이전트가 먼저 값을 낸 지점은 새 발견보다, 사람이 이미 아는 긴 논증을 기계가 감사할 수 있는 형태로 옮기는 일이다.

“페르마를 AI가 풀었다”는 말은 사실이 아니다. “페르마 증명을 기계가 끝까지 재검사할 수 있게 됐다”는 말은, 공개된 저장소와 버저드의 재빌드가 있는 한, 현재 시점에서 성립한다.

#언어모델 #에이전트