Anthropic은 9월 4일 Fermat의 마지막 정리에 대한 기계 검증 형식화를 Lean 4로 공개했다. GitHub API에 따르면 이 저장소는 14:21:04 UTC에 생성됐다. 널리 퍼진 주장은 Claude가 11일 만에 Fermat의 마지막 정리를 증명했다는 것이었다. 그러나 저장소의 자체 파일은 더 좁지만, 한편으로는 더 흥미로운 내용을 설명한다.
기여도 파일이 말하는 것
이 저장소는 Kevin Buzzard가 이끈 Imperial College London의 FLT 프로젝트와 flt-regular 프로젝트의 자료를 담은 106개 파일을 기록한 ATTRIBUTION.md를 포함한다. 그 내용은 "Definitions/ 아래 54개, P2M/Sol/ 아래 52개, 그리고 Mathlib 텍스트를 재현한 23개 파일"이라고 적혀 있다. 수십 개 행에는 "whole file (100%)"라고 적혀 있다. NOTICE 파일은 이 차용의 시점을 이렇게 적는다. "자료는 프로젝트의 main 브랜치에서 2026-05-21 시점 기준으로 가져왔다." Lean 4.33으로 툴체인을 포팅하는 과정에서 기여도 파일은 "나머지 41개를 바이트 단위로 동일하게 남겨뒀다"고 기록한다.
검증 자체는 실제다
그러나 그 사실이 검증을 무효화하지는 않는다. README에 따르면 60,475개 모듈이 모두 빌드됐고, #print axioms fermat_last_theorem은 표준 공리 3개로만 제한되며, 어떤 모듈에도 axiom, sorry, native_decide, unsafe, partial def가 없다고 적혀 있다. 컴파일에는 96개 작업으로 5시간 32분이 걸렸고, 메모리 사용량은 최대 153 GB였다. Anthropic이 제시한 자체 수치는 Lean 1,300만 줄, 최종 증명에 사용된 중간 정리 29,500개, 약 60억 개의 출력 토큰이다.
받아들여진 서술이 놓친 것
세 가지다. Claude가 새로 증명한 것은 없다. 이는 Wiles–Taylor–Wiles 논증을 설명한 1995년 Darmon–Diamond–Taylor 해설을 자동 형식화한 것으로, 인간이 31년 전에 완성한 증명이다. 또 단독 작업도 아니다. Anthropic의 자체 집계에 따르면 저장소의 9분의 1은 인간이 작성한 Lean 텍스트이며, 일부는 한 글자도 바꾸지 않은 그대로다. Anthropic이 인용한 수학자 Buzzard도 같은 날 자신의 블로그에 "수학적으로 이 Anthropic의 작업은 우리에게 본질적으로 아무것도 알려주지 않는다"고 썼으며, 그 형식화는 "증명의 초기 문헌을 충실히 따를 뿐 아무것도 더하지 않는다"고 적었다. 여러 매체가 이것을 동종 최대 파일이라고 부르기도 했지만, 이는 파일 하나가 아니라 60,475개 모듈이다.
정직한 주장도 여전히 크다
이제 기계는 수년간의 자원봉사 Lean 작업을 바탕으로, 기존 수학 문헌 수천 쪽을 2주 이내에 커널 검증 가능한 형식으로 옮길 수 있다. 이는 번역 속도에 관한 실제 성과다. 그러나 수학적 발견에 관한 성과는 아니다. README도 남은 간극을 스스로 인정한다. "각 중간 정리가 그 이름이 암시하는 의미를 실제로 뜻하는지까지 확인해 줄 도구는 없다."