Claude, Lean으로 페르마의 마지막 정리 형식화… 11일 만에 1300만 줄

Anthropic는 2026년 9월 4일, 자사 AI인 Claude가 페르마의 마지막 정리에 대해 처음부터 끝까지 컴퓨터로 검증 가능한 증명을 완성했다고 발표했다. 이 정리는 정수 n이 2보다 클 때 a^n+b^n=c^n을 만족하는 양의 정수 a, b, c가 존재하지 않는다는 내용이다. 수학자 앤드루 와일스가 1995년 129쪽 분량의 증명을 발표한 지 30여 년이 지났지만, 그 논리 전체를 기계적으로 검증한 사례는 이번이 처음이다. Claude는 11일 동안 대부분 자율적으로 작업하며 증명 보조 시스템 Lean으로 약 1,300만 줄의 코드를 작성했다.

이 프로젝트는 AI를 이용한 수학 형식화를 연구하는 Anthropic 연구원 티엔이 펑(Tianyi Peng)이 주도했다. 작업 과정에서 Claude는 약 3만 300개의 중간 정리를 컴퓨터로 검증 가능한 형태로 증명했으며, 이 중 약 2만 9,500개가 최종 증명에 실제로 사용됐다. 생성된 코드 규모는 Lean의 대표적인 커뮤니티 수학 라이브러리인 Mathlib의 5배를 넘는다. 수십 개의 Claude 에이전트가 병렬로 작업하며 개념을 정의하고 중간 정리를 증명한 뒤, 점차 더 어려운 명제로 나아갔다. 초기 시도는 여러 차례 실패했다. 각 에이전트가 프로젝트 전체 진행 상황을 놓쳐 서로의 결과물을 효과적으로 재활용하지 못하는 문제가 반복됐다. 최종 증명에서 반복되지 않는 코드의 약 7%는 이런 실패한 시도에서 비롯된 것이다.

컴퓨터로 검증된 형식 증명이란 무엇인가

인간 독자를 위해 쓰인 수학 논문은 흔히 "명백하다"고 여겨지는 단계를 생략한다. 하지만 Lean 같은 증명 보조 시스템은 그럴 수 없다. 아무리 사소한 단계라도 빠짐없이 명시해야 한다. 기존 증명을 이런 형태로 다시 쓰는 작업을 "형식화"라고 부른다. 논리적 연결 고리가 단 한 곳이라도 끊어지면 그 이후의 모든 결론이 무너질 수 있기 때문에, 형식화된 증명은 Lean의 기계적 검사를 통과해야만 사람의 재검토에 의존하지 않는 정확성 보증을 얻는다. Claude의 증명은 Lean의 표준 공리 3개에만 의존하며, 증명을 일시적으로 건너뛰게 해주는 표시인 "sorry"는 단 한 번도 쓰이지 않았다. 비교 도구를 통해 Claude가 증명한 명제가 Mathlib에 기록된 페르마의 마지막 정리 서술과 정확히 일치함이 확인됐고, Rust로 독립적으로 작성된 Lean 커널 "nanoda" 역시 100만 건이 넘는 선언을 오류 없이 검증했다.

페르마의 마지막 정리가 상징적인 사례인 이유

이 정리는 17세기 프랑스 수학자 피에르 드 페르마가 1637년경 디오판토스의 저서 《산술》 여백에 남긴 메모에서 이름을 따왔다. 그는 "정말로 놀라운 증명을 발견했지만 여백이 너무 좁아 적을 수 없다"고 적었지만, 그 증명은 후대에 전해지지 않았다. 이후 350여 년 동안 수많은 수학자가 이 증명을 찾으려 했지만 실패했다. 1908년에는 오늘날 가치로 100만~200만 달러에 해당하는 상금이 걸렸고, 첫해에만 621건의 잘못된 증명이 제출됐다. 1993년 6월, 앤드루 와일스는 사흘간의 연속 강연에서 자신의 증명을 발표했지만, 약 두 달 뒤 검증 과정에서 한 심사자가 치명적인 결함을 지적했다. 와일스는 옛 제자 리처드 테일러와 함께 거의 1년에 걸쳐 이를 수정한 끝에 1995년 5월 최종 증명을 발표했다. 이 증명은 129쪽에 달했고, 수학계가 정확성을 확인하는 데만 수개월이 걸렸다. 국제 독자들에게 흥미로운 대목은, 와일스 증명의 토대가 된 타니야마-시무라 추측이 1950년대 일본 수학자 타니야마 유타카와 시무라 고로에 의해 제기됐다는 점이다. 이번에 Claude가 형식화한 것은 다몽(Darmon), 다이아몬드(Diamond), 테일러(Taylor)가 제시한 와일스 증명의 단순화된 버전이다.

Anthropic 연구진에 따르면 단 11일 만에 이뤄진 이 놀라운 자동 형식화 성과는, 수학의 공리 외에는 어떤 가정도 없이 페르마의 마지막 정리를 증명했다. 그 과정에서 대수학, 조화 해석학, 기하학, 정수론의 자동 형식화를 확인할 수 있으며, AI가 만든 자동 형식화 결과물이 이제 그 위에 다른 성과를 쌓아 올릴 수 있을 만큼 견고해졌다는 사실도 알 수 있다. 이 증명은 여러 층으로 이뤄져 있다.

• 작업 기간: 11일, 대부분 자율 작업
• 생성된 Lean 코드: 약 1,300만 줄, Mathlib의 5배 이상
• 증명한 정리 수: 약 3만 300개, 이 중 2만 9,500개를 최종 증명에 사용
• 소비한 출력 토큰: 약 60억 개, Claude Fable 5.1과 유사한 범용 연구 모델 사용
• 의존한 공리: Lean의 표준 공리 3개뿐, "sorry" 사용 0건

Claude가 실제로 한 일, 그리고 그 한계

분명히 해둘 점은 Claude가 와일스의 원래 증명을 스스로 "발견"한 것이 아니라는 사실이다. 수학적 논증 자체는 1995년 와일스와 그의 동료들이 확립한 것이며, Claude가 한 일은 그 논증의 단순화된 버전을 Lean이 검증할 수 있는 엄밀한 기호 형태로 다시 쓰고 이를 기계적으로 검사받게 한 것이다. 이는 "형식화"이지 "발견"이 아니다. 이는 새로운 수학적 성과를 만들어내는 것을 목표로 했던 최근 리만 가설 관련 AI 연구와는 성격이 다르다. Anthropic은 이번 작업의 새로움이 발견이 아니라 검증에 있다고 명확히 밝혔다. 이 작업은 티엔이 펑이 만든 수학 형식화 협업 플랫폼 Prove2Me에 의존했는데, 이 플랫폼은 정리들 사이의 의존 관계를 방향성 비순환 그래프(DAG)로 관리해 여러 Claude 에이전트가 다음에 어떤 정리를 공략해야 할지 파악할 수 있도록 했다. 사람의 개입은 "야코비안을 스킴으로서 우선 처리하라"와 같은 펑의 고차원적 지시에 그쳤다.

AI가 더 많은 수학 증명을 만들어낼수록 이를 사람이 직접 검증해야 하는 부담도 커진다. Anthropic은 앞으로 인간 독자를 위한 논문과 함께 컴퓨터로 검증 가능한 형식화된 증명을 함께 내놓는 것이 일반적인 관행이 될 것으로 내다본다. 2024년부터 임페리얼 칼리지 런던에서 Lean으로 페르마의 마지막 정리를 형식화하는 다년간의 커뮤니티 프로젝트를 이끌어온 케빈 버자드는—초기 작업 계획서만 해도 86쪽에 달했다—이번 성과를 현대 수학 문헌의 자동 형식화를 향한 큰 진전이라고 평가하며, 기존 수학 체계의 오류를 찾아내고 심사자의 부담을 덜어주며 AI가 생성한 수학을 엄밀하게 검증할 수 있는 수단이 될 것이라고 말했다.

한국의 기술·연구 기관에도 이번 사례가 주는 의미는 수학적 성과 하나에 그치지 않는다. 이 정리를 검증한 것과 같은 증명 보조 시스템은 이미 암호 프로토콜, 컴파일러의 정확성, 반도체 설계나 항공 분야의 안전 필수 코드를 검증하는 데 쓰이고 있다—국내 대학과 KAIST, ETRI 등 연구기관이 형식 검증 분야에 꾸준히 투자해 온 영역이기도 하다. AI 에이전트가 수년이 아니라 며칠 만에 기계로 검증된 코드를 수백만 줄 생성할 수 있다는 사실은, 오랫동안 너무 느리고 전문적이라 확장하기 어렵다고 여겨졌던 형식 검증이 순수 수학을 넘어 일반 엔지니어링 팀에도 훨씬 더 가까워질 수 있다는 구체적인 신호다. 다만 Anthropic 스스로 강조하듯, 이런 검증 능력을 새로운 수학을 스스로 발견하는 능력으로 착각해서는 안 된다.