앤트로픽, 페르마의 마지막 정리 형식화 완성

앤트로픽(Anthropic)은 2026년 9월 4일 사이언스 연구 글로, 클로드(Claude)가 페르마의 마지막 정리(Fermat’s Last Theorem, FLT)를 처음부터 끝까지 컴퓨터로 검증한 린(Lean) 증명을 처음 완성했다고 밝혔다. 작업은 다중 에이전트와 클로드 코드(Claude Code) 하네스를 썼고, 소요는 11일, 표현은 ‘두 주가 조금 안 되는’ 수준이다. 새 정리를 낸 것이 아니라, 이미 알려진 와일스식 논증을 단순화한 경로를 기계가 끝까지 형식화했다는 점이 핵심이다.

정리 자체는 1637년경 피에르 드 페르마(Pierre de Fermat)가 디오판토스의 《산술》에 남긴 주장으로, 양의 정수 a, b, c와 n>2에 대해 aⁿ+bⁿ=cⁿ이 성립하지 않는다는 것이다. 1908년 현상금은 독일 금마르크 10만 마르크(오늘 가치로 약 100만~200만 달러)였고, 첫해에만 틀린 시도가 621건이었다. 앤드루 와일스(Sir Andrew Wiles)가 1993년 6월 강연으로 증명을 공개했고, 심사 약 두 달 만에 빈틈이 드러난 뒤 리처드 테일러(Richard Taylor)와 1년을 더 써서 1995년 5월에 출판했다. 인간 증명은 129쪽이었다.

형식화 아이디어는 1995년 발표 후 대략 10년 뒤에 얀 베르흐스트라(Jan Bergstra)가 와일스 증명을 컴퓨터로 옮기자는 제안으로 거슬러 올라간다. 임페리얼 칼리지 런던의 케빈 버저드(Kevin Buzzard)가 이끈 커뮤니티 FLT 린 작업은 2024년에 시작됐고, 초기 단계 청사진은 86쪽이었다. 게르하르트 프라이, 장피에르 세르, 켄 리벳, 배리 메이저, 로버트 랭글랜즈, 제럴드 터널, 유타카 타니야마, 고로 시무라, 앙드레 베유 같은 이름은 와일스–테일러 배경으로만 인용된다. 커뮤니티는 수년이 걸릴 것으로 봤고, 이번 결과는 그 로드맵과 별개의 클로드·Prove2Me 산출물이다.

경로 선택은 앙리 다르몽(Henri Darmon), 프레드 다이아몬드(Fred Diamond), 리처드 테일러의 해설을 따른 단순화 와일스다. 임페리얼 FLT 프로젝트와 flt-regular에서 일부를 가져와 맞췄다. 수학 입력은 앤트로픽 연구자 톈이 펑(Tianyi Peng)의 가끔 있는 고수준 지시로 제한됐다. 예시는 “야코비안을 스킴으로 다루는 일이 우선순위로 들린다”, “메이저 정리를 빨리 끝내라” 정도였다.

초반 다중 에이전트는 프로젝트 상태를 잃고 협업이 어긋나 실패했다. 전환점은 펑과 컬럼비아 그룹이 공동 설계한 공개 형식화 플랫폼 Prove2Me였다. 정리 문장을 DAG로 두고 다음에 무엇을 증명할지와 병렬 에이전트를 고르고, 문장과 증명은 파일을 나누며, 자연어 설명으로 검색·재사용한다. 협력자는 Chen, S., Marwaha, K., Lu, X., Yuen, H., Peng, T.이며 2026년 논문은 arXiv:2608.28433이다.

수십 개 클로드 에이전트가 개념을 정의하고 중간 정리를 쌓아 더 어려운 명제로 올라갔다. 최종 증명에 쓰인 중간 정리는 2만 9500개, 과정 중 증명한 정리는 3만 300개다. 초기의 실패한 시도가 최종본의 보일러플레이트 아닌 줄의 약 7%를 남겼다. 린 코드는 1300만 줄로 Mathlib 규모의 5배를 넘고, 앤트로픽은 지금까지 만든 린 증명 중 가장 크다고 적었다.

출력 토큰은 약 60억으로, 범용 내부 연구 모델은 클로드 페이블 5.1(Claude Fable 5.1)과 대략 비슷한 급이라고 했다. 검사는 린의 표준 공리 세 개만 쓴다. 비교기가 정리 문장이 Mathlib FLT 문장과 같음을 확인했다. 에이전트 로그 시각은 prove2me에서 FLT 루트가 PROVED된 시각이 8월 18일 02:00:57Z(동부 8월 17일 오후 10시 57분)다.

로그에는 “FLT 루트가 Proved로 읽힌다… 재확인을 전제로 한 역사적 순간”, “R=T가 닫히고 루트까지 cascaded… prove2me에서 종단 FLT”라는 식의 기록이 있다. 버저드는 증명을 검토했고, 11일 자동형식화가 수학 공리 외 가정을 두지 않으며 대수·조화해석·기하·정수론을 함께 옮겼고 산출물이 쌓아 올릴 만큼 튼튼하며 다층이라고 평가했다. 검토 뒤에는 FLT를 이렇게 옮길 수 있다면 현대 문헌 자동형식화로 큰 한 걸음이며, 오류 탐지와 심사 부담 완화, 지금은 비싼 인간 검수인 LLM 수학의 엄밀 점검에 쓸 수 있다고 했다.

같은 글의 작은 실험은 개인 클로드 맥스 플랜 3개가 Prove2Me로 협력해 비노그라도프 세 소수 정리(하디–리틀우드 원 방법 응용)를 3일 만에 형식화한 것이다. 올바른 골격이 있으면 소비자용 구독만으로도 대형 결과 형식화가 가능하다는 주장이다. 전체 증명은 깃허브와 글로 된 해설, 사고 발췌와 함께 공개됐다.

한계는 분명하다. 새 FLT 증명이 아니라 단순화 와일스 논증의 컴퓨터 검증이며, 사람이 읽기 좋은 해설을 대체한다고 하지 않았다. 최근 AI의 리만 가설 쪽 시도와 달리 여기는 검증의 새로움이지 정리의 새로움이 아니다. 로그 스스로도 ‘재확인을 전제’했고, 토큰 비용이 크다. 헤일스/케플러, 페렐만/푸앵카레, 헬프곳/약한 골드바흐처럼 긴 증명 검증이 어렵다는 각주는 FLT 린 주장 본체가 아니다.

앤트로픽과 ‘다른 랩’은 순수수학·형식화를 포함한 외부 연구자에게 무료·할인 구독과 연구 크레딧을 늘렸고, 다른 대형 정리나 린/Mathlib 같은 더 큰 과학 과제용 전용 지원도 언급했다. 린 FRO와 Mathlib 생태계 위에 커뮤니티 FLT·flt-regular가 이미 있었고, 이번 산출물은 그 위에 ple어 올릴 수 있다는 버저드의 평가와 맞물린다. 형식화의 병목이 ‘무엇을 증명할지’와 ‘에이전트가 상태를 공유할지’에 있었다는 점이, Prove2Me DAG와 문장·증명 분리로 드러난다.

요컨대 1637년 메모에서 1995년 129쪽 인간 증명, 2024년 커뮤니티 린 착수, 2026년 8월 18일 UTC 새벽의 루트 Proved 시각까지가 한 줄로 이어진다. 11일, 1300만 줄, 중간 정리 2만 9500개, 출력 토큰 약 60억, 표준 공리 세 개라는 숫자는 ‘와일스를 다시 발명했다’가 아니라 ‘알려진 경로를 기계가 끝까지 닫았다’는 주장의 크기만 가리킨다. 다음 질문은 다른 거대 정리를 같은 골격으로 옮길지, 그리고 인간 심사와 LLM 생성 수학의 검수를 얼마나 줄일지다.

https://www.anthropic.com/research/formalizing-fermats-last-theorem