앤스로픽, 페르마의 마지막 정리 Lean 4 완전 형식검증 공개

ai.euno.news 자동 뉴스 요약

앤스로픽이 페르마의 마지막 정리를 정리 증명 언어 Lean 4로 완전히 형식검증한 코드베이스를 공개했다.¹ 깃허브 저장소 anthropics/fermats-last-theorem에는 프레이, 세르, 리벳, 와일스, 테일러-와일스로 이어지는 고전적 증명 경로를 그대로 따라간 모듈들이 담겨 있고, 이 전체가 Lean 커널에 의해 검사됐다.

증명의 핵심 명제는 Theorems/Thm_fermat_last_theorem.lean에 정의된 fermat_last_theorem으로, 3 이상인 자연수 n과 양의 자연수 a, b, c에 대해 a^n + b^n ≠ c^n이 성립한다는 내용이다. 빌드 스크립트 FinalCheck.lean은 이 정리가 propext, Classical.choice, Quot.sound라는 Lean의 표준 공리 세 개에만 의존하는지를 #guard_msgs로 강제 확인하도록 짜여 있어, sorry나 추가 공리, native_decide가 하나라도 섞이면 빌드 자체가 실패한다. 저장소는 2026년 커널 안전성 수정을 포함한 Lean 4.33.1과 Mathlib v4.33.0을 기반으로 처음부터 다시 빌드됐고, 6만475개 전체 모듈이 통과했다.

검증은 한 번에 그치지 않았다. leanprover 팀의 comparator v4.33.0은 증명된 명제와 그 안의 모든 상수가 Mathlib만으로 서술한 도전 명제(Challenge.lean)와 동일하고, 다른 공리를 쓰지 않았으며, Mathlib을 포함한 전체 증명이 Lean 커널을 통과한다는 점을 확인해 “Your solution is okay!”라는 판정을 내렸다. 여기에 러스트로 작성된 독립 커널 nanoda 0.4.13이 같은 환경을 lean4export로 내보낸 결과물을 받아 105만2234개 선언을 오류 없이 검사했다. 앤스로픽은 nanoda에 진행 상황 표시와 정의 동치 탐색 속도 개선을 위한 패치 네 개를 직접 적용했지만, 타입 규칙 자체는 건드리지 않았다고 밝혔다.

저장소 안에는 axiom, sorry, native_decide, unsafe 같은 키워드가 도전 명제 파일을 제외하면 어디에도 없다. 두 검증을 합치면, 이 명제가 Lean 커널(또는 nanoda)과 검사 도구를 신뢰한다는 전제 아래 세 공리로부터만 도출된다는 점이 확인된다. 다만 앤스로픽은 각 중간 정리가 이름이 암시하는 내용과 실제로 일치하는지는 어떤 도구도 검사할 수 없고, 이는 PROOF-PATH.md에 정리된 단계별 대응을 보고 읽는 사람이 직접 판단할 몫이라고 밝혔다.

증명 전체는 약 390MB 용량의 html 폴더로도 제공된다. 2만9511개 정리와 1450개 정의 모듈 각각에 개별 페이지가 있고, 의존성 그래프와 검색 기능을 갖춰 웹서버 없이 브라우저에서 오프라인으로 열람할 수 있다. 저장소는 연구 산출물로 공개된 것이며, 유지보수나 외부 기여는 받지 않는다고 명시돼 있다.

읽기 목록은 이 브라우저에 저장됩니다.