페르마의 마지막 정리, AI가 11일 만에 완전 증명
원제: Formalizing Fermat's Last Theorem
왜 중요한가
AI가 수백 년간 미해결 난제의 컴퓨터 검증 증명을 자율 수행하며 수학 연구 검증 방식의 근본적 변화 가능성을 제시했다.
Anthropic은 2026년 9월 4일, Claude가 11일간 자율 작업을 통해 페르마의 마지막 정리(FLT)의 최초 완전 컴퓨터 검증 증명을 완성했다고 발표했다. Claude는 Lean 언어로 1,300만 줄을 작성하고 2만 9,500개의 중간 정리를 증명했으며, 수학 공리 외 추가 가정은 없다.
페르마의 마지막 정리(FLT)는 1637년 피에르 드 페르마가 'n > 2인 경우 aⁿ + bⁿ = cⁿ을 만족하는 양의 정수 a, b, c는 존재하지 않는다'고 주장한 명제로, 1995년 앤드루 와일스(Andrew Wiles)가 129페이지 분량의 논문으로 처음 증명했다. 그 후 수학자들은 이 증명을 컴퓨터가 자동으로 확인 가능한 형식으로 변환하는 '형식화(formalization)' 작업을 추진해 왔으며, 2024년 임페리얼 칼리지 런던의 Kevin Buzzard를 중심으로 Lean 증명 보조 도구를 이용한 커뮤니티 프로젝트가 진행 중이었다.
Anthropicの 연구자 Tianyi Peng은 Claude가 FLT 형식화에 기여할 수 있는지 테스트했고, 결과는 예상을 뛰어넘었다. Claude는 11일 만에 수학 공리 외 어떠한 추가 가정 없이 FLT의 단대단(end-to-end) 컴퓨터 검증 증명을 완성했다. 이 과정에서 Claude는 Lean 언어로 1,300만 줄의 코드를 작성하고, 대수학·조화 해석·기하학·수론 분야에 걸쳐 2만 9,500개의 중간 정리를 증명했다.
Kevin Buzzard는 이 성과를 '수학 공리만을 전제로 FLT를 증명한 탁월한 자동 형식화 업적'이라고 평가하며, 증명이 다층적 구조를 갖추고 있어 AI 형식화 결과물이 후속 연구에 활용될 만큼 견고하다고 밝혔다. Anthropic은 AI가 점점 더 많은 증명을 생성함에 따라 형식화 기술이 새로운 결과물의 검증 부담을 줄이고 수학 지식 체계의 신뢰성을 높이는 데 기여할 것으로 전망했다.