앤트로픽, 페르마의 마지막 정리 정형 증명 오픈소스 공개… Claude가 전 과정 완수

앤트로픽이 페르마의 마지막 정리를 Lean 4로 완벽하게 기계 검증한 오픈소스 리포지토리 fermats-last-theorem을 깃허브에 공개했다. 총 29,511개의 정리와 1,450개의 정의 모듈, 1,300만 줄 이상의 방대한 코드로 구성되어 지금까지 작성된 Lean 증명 중 최대 규모를 자랑한다.

프라이, 세르, 리베, 와일스, 테일러-와일스로 이어지는 정통 수학적 증명 경로를 따랐으며, 아파치 2.0 라이선스로 배포된다. 전체 증명 단계를 오프라인 웹브라우저에서 둘러볼 수 있는 대화형 문서도 패키지에 포함되어 있다.

구현 방식과 검증 체계

이 프로젝트의 소스코드는 사람이 직접 작성하지 않고, 기존 오픈소스 Lean 코드를 바탕으로 AI 에이전트가 생성한 뒤 Lean 컴파일러를 엄격한 심판 삼아 완성했다. 사람이 읽기 위한 목적이 아니라 컴파일러 검증 통과를 목표로 작성되었기 때문에, 중간 정리 이름이나 변수는 기계가 생성한 식별자로 채워져 있다.

신뢰성은 완벽하게 담보되었다. 코드베이스 전체에 임시 증명 표시인 sorry나 추가 공리, 편법 연산인 native_decide가 일절 쓰이지 않았으며, Lean의 세 가지 표준 공리 위에서만 유도되었다.

앤트로픽은 검증의 확실성을 위해 이중 검증을 거쳤다. Lean 4.33.1 공식 커널과 비교 도구를 통과했을 뿐 아니라, 러스트로 작성된 독립 서드파티 Lean 커널인 nanoda로 환경 전체를 검증했다. nanoda는 1,052,234개의 선언을 단 하나의 오류도 없이 확인했다.

실행 방법과 하드웨어 사양

증명 전체를 로컬에서 처음부터 다시 빌드하려면 고사양 리눅스나 macOS 머신이 필요하며, 경로 길이 제한 문제로 윈도우는 지원하지 않는다.

하드웨어 요구치가 상당하다. 96개 스레드 기준 Lake 소스 빌드 시 병렬 작업당 약 5GB, 피크 메모리 153GB가 필요하며 약 5시간 32분이 소요된다. 임시 C 파일 등 빌드 디스크 공간도 200GB 이상 비워두어야 한다. 이후 단일 코어로 도는 검증 스크립트는 약 15시간 동안 최대 300GB의 램을 요구한다.

단순히 수학적 증명 구조를 살펴보고 싶은 이용자라면 무거운 전체 빌드를 돌릴 필요가 없다. 저장소 안에 포함된 약 390MB 크기의 html 폴더에서 index.html을 열면, 웹서버 설정 없이도 오프라인에서 모든 정리와 정의 간의 의존성 그래프를 직관적으로 탐색할 수 있다.

왜 중요한가

정형 검증 연구자, 수학자, AI 에이전트 파이프라인을 구축하는 엔지니어들이 즉시 살펴볼 만한 결과물이다. 사람이 수십 년간 매달려야 했던 방대한 수학 정형화 작업을 AI와 정리 증명기의 피드백 루프로 돌파할 수 있음을 완벽하게 보여주었다.

기계가 생성한 코드 특성상 사람이 교재처럼 한 줄씩 읽어나가기는 어렵지만, AI의 환각 문제를 컴파일러 수준에서 원천 차단하고 과학적 난제를 검증해 낼 수 있음을 입증한 중대한 전환점이다.