- 무슨 일: Anthropic은 Claude가 페르마의 마지막 정리의 기존 증명을 Lean으로 형식화한 결과를 2026년 9월 4일 공개했습니다.
- 왜 중요한가: 새 정리를 찾았다는 뜻이 아니라, 긴 수학 증명을 컴퓨터가 재검사할 수 있는 형태로 옮기는 자동화의 규모가 커졌다는 뜻입니다.
- 아직 모르는 것: 이 결과가 일반 수학 연구나 공개 Claude 제품에서 곧바로 재현되는지는 발표만으로 확인되지 않습니다.
Anthropic 공식 발표는 Claude가 페르마의 마지막 정리의 새 증명을 발견한 것이 아니라, 이미 알려진 증명을 Lean 언어로 형식화해 컴퓨터가 점검할 수 있게 만든 작업이라고 설명합니다.
Anthropic은 이 작업을 2026년 9월 4일 공개했습니다. 회사 발표에 따르면 Claude 에이전트들은 11일 동안 주로 자율적으로 작업했고, 최종 결과는 Lean에서 끝까지 점검 가능한 형태로 구성됐습니다.
제목만 보면 AI가 오래된 난제를 새로 풀었다고 읽히기 쉽습니다. 하지만 페르마의 마지막 정리는 앤드루 와일스의 증명으로 1995년에 이미 해결됐습니다. 이번 발표의 핵심은 그 증명의 논리 사슬을 기계가 검사할 수 있는 언어로 세밀하게 옮긴 데 있습니다.
새 정리 발견이 아니라 ‘형식화’입니다
수학자가 읽는 증명은 많은 중간 단계를 공유된 지식으로 생략할 수 있습니다. 반면 Lean 같은 증명 보조기는 각 단계와 의존 관계를 코드로 명시해야 하므로, 사람이 납득하는 증명을 컴퓨터가 재현 가능한 증명으로 바꾸는 과정 자체가 큰 작업이 됩니다.
Anthropic은 이 결과에서 새로움이 수학적 발견 자체보다 검증에 있다고 구분합니다. 즉 페르마의 마지막 정리의 결론을 바꾼 것이 아니라, 기존 논증을 더 엄격하게 재검사할 수 있는 산출물로 만든 것입니다.
11일·1,300만 줄·2만9,500개가 말하는 작업 범위
공식 발표에 따르면 Claude는 11일 동안 약 1,300만 줄의 Lean 코드를 작성했고, 최종 증명에 사용된 중간 정리는 2만9,500개였습니다. 이 숫자는 정리 하나를 짧은 답변으로 푼 사례가 아니라, 많은 하위 정리와 검증 단계를 쌓는 프로젝트였다는 점을 보여 줍니다.
Anthropic은 완성된 증명이 Lean의 표준 공리 세 가지를 사용했고, comparator 도구가 Mathlib에 있는 페르마의 마지막 정리 문장과의 일치를 확인했다고 설명합니다. 이는 회사가 공개한 검증 절차의 범위이며, 이 글에서는 이를 새 수학적 발견의 증거로 확대해 해석하지 않습니다.
왜 AI 수학 기사에서 이 차이가 중요할까요
AI가 ‘증명했다’는 표현은 두 가지를 섞기 쉽습니다. 하나는 이전에 없던 정리나 방법을 발견하는 일이고, 다른 하나는 이미 있는 추론을 형식 언어로 바꿔 오류 검사를 가능하게 하는 일입니다. 이번 사례는 후자에 해당합니다.
그렇다고 의미가 작다는 뜻은 아닙니다. 긴 증명을 형식화하는 데 걸리는 시간과 협업 비용이 줄어들면, 사람이 쓴 연구나 AI가 만든 초안을 더 자주 기계적으로 점검할 수 있는 기반이 커질 수 있습니다. 다만 그 가능성은 연구 현장의 일반적 적용과는 구분해서 봐야 합니다.
공개 Claude에서 바로 할 수 있는 일은 아닙니다
Anthropic은 이 작업에 Claude Code 기반 다중 에이전트 체계와 Prove2Me 협업 플랫폼을 사용했다고 설명합니다. 따라서 발표만으로 일반 사용자가 공개 Claude 서비스에서 같은 규모의 형식화를 재현할 수 있다고 말할 수는 없습니다.
이번 소식의 한 줄 결론은 분명합니다. Claude가 페르마의 마지막 정리를 새로 발견한 것이 아니라, 이미 알려진 증명을 컴퓨터가 확인할 수 있는 Lean 형식으로 대규모 자동화했다는 발표입니다. 원문에는 작업 방식과 공개된 증명 자료가 함께 안내돼 있습니다.
Anthropic 공식 발표에서 형식화 과정과 원문 보기 · 공개된 증명 저장소 보기