Anthropic의 페르마의 마지막 정리 Lean 증명: 직접 검증하는 방법

“Claude가 페르마의 마지막 정리를 풀었다”는 제목을 봤다면, 그중 한 단어부터 확인해야 한다. 바로 형식화다. Anthropic은 정리를 처음부터 끝까지 검사할 수 있다고 밝힌 공개 Lean 산출물을 내놨지만, 그 안에 담긴 수학적 경로는 새롭게 발견된 증명이 아니다. 수십 년 전 Andrew Wiles와 Richard Taylor가 완성한 Frey–Serre–Ribet–Wiles–Taylor-Wiles 논증을 기계가 확인할 수 있는 형태로 옮긴 것이다.

먼저 두 가지 주장을 나눠 보자

좁은 의미에서 답하면 그렇다. Anthropic은 페르마의 마지막 정리(FLT)를 Lean 4로 형식화한 공개 저장소를 배포했고, 저장소에는 빌드와 검증 방법도 포함돼 있다. 하지만 Claude가 이 유명한 문제를 독자적으로 풀었다는 식의 해석은 정확하지 않다. 수학적 돌파구를 마련한 사람은 수십 년 전의 Andrew Wiles와 Richard Taylor다.

FLT는 n > 2일 때 a^n + b^n = c^n을 만족하는 양의 정수해가 존재하지 않는다는 정리다. Wiles의 증명은 1995년에 발표됐고, Anthropic의 결과는 이미 확립된 증명 경로를 기계가 검사할 수 있는 산출물로 바꾼 것이다. 역사적 배경은 Lean Community의 FLT 프로젝트 발표문에서 확인할 수 있다.

Lean 증명이 답하는 질문은 비형식적인 수학 논문이 답하는 질문과 다르다. 특정 환경에서 정확하게 인코딩한 명제가 검사된 정의, 의존성, 공리로부터 따라오는지를 보여줄 수는 있다. 그러나 AI가 그 밑바탕의 수학을 발명했다거나, 정리 이름이 실제 내용을 정확히 설명한다고 증명해 주지는 않는다.

Anthropic이 실제로 공개한 것

Anthropic의 2026년 9월 4일 연구 글에 따르면 Claude는 11일 만에 FLT를 완전한 엔드투엔드 컴퓨터 검증 Lean 형식화로 만들었다. 이 글은 약 1,300만 줄의 Lean 코드와 증명된 정리 서술 30,300개, 최종 증명에 사용된 정리 29,500개를 제시한다. 출력 토큰은 약 60억 개였다고도 설명한다.

이 작업에는 Prove2Me가 사용됐다. Anthropic은 이 플랫폼을 정리 서술의 방향성 비순환 그래프를 관리하고 여러 에이전트를 조율하는 시스템이라고 설명한다. 형식화는 Frey, Serre, Ribet, Wiles, Taylor-Wiles와 연결된 기존 증명 경로를 단순화해 설명한 버전을 따른다고 Anthropic은 밝혔다.

주장을 실제로 확인하려면 발표문보다 공개 GitHub 저장소가 더 유용하다. 기본 대상은 FinalCheck.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

저장소는 스스로를 유지 관리하지 않으며 기여를 받지 않는 연구 산출물이라고 명시한다. Lean 4.33.1과 Mathlib v4.33.0을 고정하고 있으며, PROOF-PATH.md와 함께 정리 및 정의 그래프를 오프라인에서 탐색할 수 있는 HTML 렌더링도 제공한다.

저장소의 최종 검사는 추가 공리, sorry, native_decide, unsafe 또는 이와 비슷한 우회 수단에 의존할 경우 실패하도록 설계돼 있다. 스크린샷이나 설명문을 믿으라는 대신, 결과물을 직접 들여다볼 수 있게 만든 장치다.

재현 가능한 검증 순서

제대로 확인하려면 다른 프로젝트에 고립된 .lean 파일을 복사하는 대신, 저장소가 고정해 둔 환경부터 그대로 재현해야 한다. Lean Community의 검증 가이드가 이 점을 강조하는 이유도 여기에 있다. Lean은 매달 릴리스되고 Mathlib은 자주 바뀌며, 이전 버전과의 호환성이 보장되지 않기 때문이다.

빌드 전에 환경부터 고정하자

저장소에 따르면 빌드는 Linux 또는 macOS에서 수행하도록 설계됐으며, elan, Git, Python, GNU coreutils가 필요하다. Lake가 고정된 의존성을 내려받고 빌드할 수 있도록 네트워크 연결도 필요하다. .lake 아래에 약 67GB가 사용되고, 이후 삭제할 수 있는 생성 C 파일이 약 220GB 추가로 생긴다고 저장소는 설명한다.

병렬 작업 하나당 메모리는 약 5GB가 필요하며, 일부 모듈은 최대 36GB를 요구한다고도 적혀 있다. 96개 작업을 사용한 저장소 자체의 빌드는 5시간 32분이 걸렸고 메모리 사용량은 최고 153GB에 도달했다. 이는 이 글에서 측정한 결과가 아니라 저장소가 보고한 수치다. 따라서 보장된 실행 시간이 아니라 준비 단계에서 참고할 경고로 보는 편이 맞다.

검증 수준을 선택하자

• 내용만 확인: 빌드하지 않고 FinalCheck.lean, PROOF-PATH.md, ATTRIBUTION.md를 읽는다.
• 전체 Lean 빌드: 고정된 툴체인을 사용해 lake build를 실행한다.
• 독립 재실행: 빌드와 내보내기가 끝나면 comparator와 nanoda 스크립트를 실행한다.

새로 클론한 저장소에서는 다음과 같은 순서를 안내한다.

git clone https://github.com/anthropics/fermats-last-theorem.git flt
cd flt

# 필요한 메모리를 확보할 수 없다면 숫자를 낮춘다.
LEAN_NUM_THREADS=96 lake build

# Mathlib만 사용하는 도전 과제 서술과 결과를 비교한다.
verification/comparator/run.sh

# comparator 검사 후 실행한다.
verification/nanoda/run.sh

각 단계의 역할은 서로 다르다.

Comparator는 정리 서술을 직접 읽는 일을 대신하지 않는다. 프로젝트가 약화됐거나 미묘하게 다른 명제를 증명하는 위험을 점검하는 장치에 가깝다. 저장소의 PROOF-PATH.md는 수학적 단계와 Lean 선언의 대응 관계를 정리하고, 생성된 HTML 페이지에서는 웹 애플리케이션을 실행하지 않고도 의존성을 살펴볼 수 있다.

저장소는 두 번째 검증에 필요한 추가 비용도 안내한다. 37.8GB짜리 내보내기 파일을 작성하려면 약 90GB의 메모리가 필요할 수 있고, nanoda 검증 과정에서는 약 40GB가 필요할 수 있다.

이 증거가 보여주는 것과 보여주지 못하는 것

Lean Community의 “Did you prove it?” 체크리스트가 제시하는 핵심 원칙은 분명하다. 컴파일은 인코딩된 명제를 검증할 뿐, 정리 이름이 의도한 비형식적 주장과 일치하는지까지 확인하지는 않는다. 이번 산출물에서는 comparator와 Mathlib 활용이 그 위험을 줄여주지만, 정리 선언과 증명 경로를 직접 읽어야 한다는 원칙까지 없애주지는 않는다.

이 산출물이 증명하는 것과 증명하지 않는 것

이번 시스템은 이례적인 규모의 형식 검증 Lean 산출물을 만들어냈다. 하지만 FLT로 가는 새로운 경로, 새로운 초등적 증명, 또는 Claude의 독립적인 수학적 발견을 보여주는 결과는 아니다.

Anthropic은 이 증명이 Wiles의 경로를 단순화한 버전을 따른다고 설명한다. 저장소 역시 기존 작업을 출처로 명시한다. ATTRIBUTION.md에 따르면 106개 파일에는 Imperial College London FLT 프로젝트 또는 flt-regular의 자료가 들어 있으며, Mathlib도 함께 사용된다. 공개된 산출물이 무엇을 기반으로 만들어졌는지 정확히 설명하려면 이러한 출처도 함께 봐야 한다.

프로젝트는 실행 과정에서 30,300개의 정리 서술을 증명했고 최종 증명에는 약 29,500개가 사용됐다고 보고한다. 한편 저장소에는 정리 페이지가 29,511개라고 적혀 있다. 이는 형식 선언과 의존성의 수이지, 새롭게 발견된 수학적 결과가 29,511개라는 뜻은 아니다. 형식 증명은 사람이 쓴 증명에서 숙련된 독자의 이해에 맡길 수 있는 암묵적 단계, 타입, 형 변환, 정의, 라이브러리 의존성을 모두 펼쳐놓는다.

저장소는 소스가 읽기보다 검사를 위해 작성됐다고 설명한다. 이름은 기계가 생성했고, P2M 같은 표기는 파이프라인 라벨이며, 무엇보다 권위 있는 것은 이름이 아니라 명제의 실제 서술이다. 그래서 최종 정리만큼이나 증명 경로와 comparator가 중요하다.

이전 Lean 작업을 2026년 주장과 한데 묶어서는 안 된다. 2023년에 발표된 정규 소수에 대한 페르마의 마지막 정리 논문은 Kummer 정리의 제1 경우를 완전하고 sorry 없이 형식화했다고 보고했다. 다만 제2 경우와 Kummer의 보조정리는 여전히 상당한 작업으로 남아 있다고 설명했다. 2025년 개정판은 정규 소수에 대한 형식화가 그 좁은 범위의 경우를 완전히 증명한 것이라고 설명한다.

Imperial/Lean FLT 프로젝트는 현대 수론의 형식화를 단순히 정리 하나를 번역하는 작업이 아니라 더 넓은 기반 시설 구축 노력으로 설명한다. Anthropic의 공개 결과는 기존 형식 생태계 안에서 여러 AI 에이전트를 조율했을 때 무엇을 할 수 있는지 보여주는 보완적 증거로 이해하는 편이 적절하다. 이전 프로젝트의 목표가 더는 중요하지 않다는 증거로 볼 수는 없다.

무엇을 어느 수준까지 믿어야 할까

소식 자체만 확인하려는 경우라면 공식 발표문과 저장소만으로 프로젝트의 존재를 확인할 수 있다. 감사를 수행하려면 고정된 환경에서 빌드를 재현하고 정리 서술을 직접 읽어야 한다. AI 연구를 평가한다면 오케스트레이션, 기존 라이브러리, 선행 형식화, 컴퓨팅 자원까지 시스템의 일부로 함께 고려해야 한다.

FAQ

Claude가 페르마의 마지막 정리에 대한 새로운 증명을 발견했나?

아니다. Anthropic의 산출물은 Frey, Serre, Ribet, Wiles, Taylor-Wiles와 연결된 기존 증명 경로를 형식화한 것이다. 성과의 핵심은 새로운 수학적 해법이 아니라, 기계가 검사할 수 있는 Lean 산출물을 이례적인 규모와 속도로 만들어냈다는 데 있다.

Lean 빌드가 성공하면 비형식적인 정리도 증명된 것인가?

해당 Lean 환경에서 검사된 의존성으로부터 인코딩된 명제가 따라온다는 뜻이다. 하지만 그 명제와 정의가 실제로 주장하려는 비형식적 정리와 대응하는지는 별도로 확인해야 한다.

저장소가 sorry나 추가 공리를 사용하나?

저장소는 최종 검사가 sorry, 추가 공리, native_decide, unsafe 및 몇 가지 유사한 우회 수단을 거부한다고 설명한다. 예상되는 공리 목록은 Lean의 표준 공리 세 가지인 propext, Classical.choice, Quot.sound이다. 발표문만 믿지 말고 직접 검사를 재현하는 것이 좋다.

일반적인 노트북에서도 결과를 재현할 수 있나?

저장소를 살펴보거나 일부를 빌드하는 것은 가능할 수 있지만, 전체 검증은 가볍게 실행할 수 있는 일반적인 작업이 아니다. 저장소는 빌드에 최대 153GB, comparator에 최대 230GB의 메모리가 필요했다고 보고하며 디스크 공간도 많이 요구한다. 따라서 하드웨어가 핵심 제약 조건이다.

이 주장을 정확히 확인하려면 고정된 GitHub 산출물에서 시작해, 헤드라인보다 먼저 정리 선언을 읽어야 한다. 그리고 결과는 알려진 수학을 대규모로 AI 지원 형식화한 사례라고 설명하는 것이 가장 정확하다.