Claude가 페르마 정리를 1300만 줄로 검증했다, 새 증명은 아니다
Anthropic의 2026년 9월 4일 연구 발표 에 따르면 Claude 기반 다중 에이전트 시스템은 기존 페르마의 마지막 정리 증명을 11일 동안 약 1300만 줄의 Lean 코드로 형식화했다. Claude가 코드를 작성하고 Lean이 이를 처음부터 끝까지 검사해, 정리의 완전한 기계 검증본이 만들어졌다.
이 9월 4일 공개 결과는 Claude가 미해결 문제를 새로 풀었다는 뜻이 아니다. Nature의 9월 7일 보도 도 기존 수학자들의 작업이 처음으로 컴퓨터 검증 코드로 전환됐다고 설명했다. 새로워진 것은 정리나 풀이가 아니라 기존 논증을 기계가 확인할 수 있게 만든 형식이다.
11일과 1300만 줄이 보여주는 성과
11일은 페르마의 마지막 정리를 발견하거나 새로운 자연어 논문을 쓰는 데 걸린 시간이 아니다. 기존 문헌에 있는 정의와 보조정리, 추론 관계를 Lean이 처리할 수 있는 명제로 세분화하고, 필요한 증명 항목을 작성해 전체 의존 관계를 닫은 기간이다.
이 과정에서 3만300개의 정리가 증명됐고 그중 2만9500개가 최종 증명에 사용됐다. 수십 개의 Claude 에이전트가 개념 정의와 중간 정리를 나눠 맡았으며, 전체 실행에는 약 60억 개의 출력 토큰이 쓰였다. 완성된 코드는 주요 Lean 수학 라이브러리인 Mathlib보다 다섯 배 이상 크다.
1300만 줄을 새로운 수학적 아이디어의 수나 증명의 난도로 읽어서는 안 된다. 인간용 논문은 공유된 배경지식과 자명한 단계를 생략하지만, Lean 코드는 정의와 자료형, 변환 규칙, 중간 추론을 명시해야 한다. 자동 생성 과정에서 나온 반복적인 코드도 전체 분량에 포함된다.
따라서 숫자가 직접 보여주는 것은 풀이의 독창성보다 형식화의 규모와 속도다. 여러 해가 걸릴 것으로 예상됐던 작업을 다수의 에이전트가 병렬로 수행하고, 서로 완성한 정리를 검색해 재사용하며 하나의 검증 가능한 결과로 연결했다.
발견·자연어 증명·형식화·검증은 다르다
이번 결과는 수학 작업을 네 단계로 구분하면 명확해진다. 첫째인 발견은 알려지지 않은 명제나 해결 방법을 찾아내는 일이다. 둘째인 자연어 증명은 수학자가 그 아이디어와 논리 전개를 사람이 읽을 수 있는 논문이나 해설로 구성하는 단계다.
셋째인 형식화는 자연어 논증을 Lean의 엄밀한 문법과 논리 체계로 다시 작성하는 작업이다. Claude가 수행한 핵심 역할이 여기에 해당한다. 이번 코드는 새로운 경로를 만든 것이 아니라 앤드루 와일스와 리처드 테일러의 성과를 바탕으로 앙리 다르몽, 프레드 다이아몬드, 리처드 테일러가 정리한 기존 전개를 따른다.
넷째인 커널 검증에서는 Lean의 작은 신뢰 기반이 제출된 코드의 추론을 검사한다. 생성 모델이 그럴듯한 설명을 출력했다고 정리가 참으로 인정되는 것이 아니다. 각 증명 항목이 요구되는 타입과 논리 규칙을 충족해야 최종 정리가 닫힌다.
이 구분에서 “Claude가 페르마의 마지막 정리를 증명했다”는 표현은 조건부로만 정확하다. 새로운 수학적 풀이를 발견했다는 의미라면 틀리다. 기존 증명을 완전한 형식 코드로 옮겨 Lean 검사를 통과시켰다는 의미라면 맞다.
Lean 검증이 보장하는 것과 보장하지 않는 것
Lean이 확인하는 것은 입력된 형식 명제와 증명 코드 사이의 논리적 정합성이다. 지정된 공리와 라이브러리 정의, 이미 검증된 정리, Lean의 추론 규칙을 전제로 결론이 실제로 따라오는지 검사한다. 중간 단계 하나라도 필요한 명제나 타입을 충족하지 못하면 전체 증명은 정상적으로 완성되지 않는다.
완성된 증명은 Lean의 표준 공리 세 개를 사용한다. 별도의 비교 도구는 최종 코드가 증명한 명제가 Mathlib에 기록된 페르마의 마지막 정리 명제와 일치하는지도 확인했다. 이는 더 약하거나 다른 명제를 증명하고 원래 목표를 달성했다고 표시할 가능성을 줄이는 절차다.
다만 기계 검증이 모든 종류의 오류를 무조건 제거하는 것은 아니다. 신뢰 범위에는 Lean 커널과 실행 환경, 사용된 공리와 정의, 가져온 라이브러리, 그리고 형식 명제가 사람이 의도한 수학적 내용을 정확히 표현하는지가 포함된다. 이번 결과는 “컴퓨터가 수학 전체를 이해했다”가 아니라 “명시된 형식 체계 안에서 이 증명 코드가 검사를 통과했다”는 뜻이다.
자연어 해설의 역할도 남는다. 1300만 줄의 코드는 생략된 논리 단계가 없는지 검사하는 데 유용하지만, 어떤 아이디어가 결정적이었는지 배우거나 증명의 큰 구조를 파악하기에는 지나치게 크다. 사람이 읽는 설명과 기계가 검사하는 형식 코드는 서로 다른 목적을 가진다.
모델보다 협업 구조가 대규모 작업을 가능하게 했다
Claude 모델 하나가 긴 파일을 처음부터 끝까지 순서대로 작성한 작업은 아니다. 초기 실행에서는 에이전트들이 프로젝트 상태를 놓치고 협업을 이어가지 못했다. 이후 컬럼비아대 연구진이 개발한 협업 플랫폼 Prove2Me와 Claude Code 기반 다중 에이전트 장치를 결합하면서 전체 작업이 진행됐다.
Prove2Me는 증명할 명제들을 방향성 비순환 그래프로 관리해 완료된 보조정리와 남은 작업을 추적했다. 명제 선언과 실제 증명을 서로 다른 파일로 분리해 컴파일 부담을 줄였고, 각 명제에 자연어 설명을 붙여 다른 에이전트가 완성된 결과를 검색하고 재사용할 수 있게 했다.
인간의 개입이 완전히 사라진 것도 아니다. 연구진은 특정 수학적 대상이나 정리를 먼저 처리하라는 높은 수준의 지침을 간헐적으로 제공했다. 결과의 정확한 주체는 단일 챗봇이 아니라 Claude 에이전트들, 작업 조정 플랫폼, 다중 에이전트 장치, Lean 검증기를 결합한 연구 시스템이다.
달력상 11일이라는 기간 역시 인간 한 명의 11일 노동과 직접 비교할 수 없다. 여러 에이전트가 동시에 작동했고 대규모 연산과 토큰이 투입됐다. Anthropic의 내부 연구 모델과 같은 환경을 일반 사용자가 동일한 비용으로 재현할 수 있는지도 아직 입증되지 않았다.
검증 뒤에는 인간의 검토와 유지보수가 남는다
코드가 Lean 검사를 통과했다는 사실과 Mathlib 같은 공동 라이브러리에 바로 편입할 수 있다는 판단은 별개다. 대규모 형식 증명에는 중복 제거, 정의와 이름의 정리, 구조 개선, 라이브러리 변경에 따른 수정, 다른 연구자가 재사용할 수 있는 형태로의 재구성이 필요하다.
페르마 정리 형식화 프로젝트를 이끌어 온 수학자 Kevin Buzzard는 직접 작성한 검토 기록 에서 1340만 줄이 넘는 코드베이스를 컴파일하고 비교 도구를 실행해 결과가 통과한다고 확인했다. 동시에 이 작업은 기존 문헌을 충실히 따르며 수학적으로 새로운 내용을 더하지 않았다고 선을 그었다.
Buzzard는 수학적 정의나 정리 증명이 아닌 코드도 따로 추려 살폈다. 그러나 이러한 점검이 코드의 간결성이나 교육적 가치, 장기 유지보수성까지 보증하지는 않는다. 동일한 정리를 증명하는 코드라도 사람이 이해하기 쉬운 구조와 공동 라이브러리에 적합한 품질은 별도의 심사를 받아야 한다.
현재 확인된 결론은 Claude 기반 시스템이 기존 페르마의 마지막 정리 논증을 대규모 Lean 코드로 형식화했고, Lean 검증과 외부 수학자의 재검사를 통과했다는 것이다. 다음 과제는 새로운 증명을 찾았는지가 아니라, 거대한 결과물을 독립적으로 계속 검토하고 사람이 탐색·재사용할 수 있는 수학 자산으로 정리할 수 있는지다.
함께 읽기:
뉴스레터 구독
최신 Web3, AI, 암호화폐 뉴스를 이메일로 받아보세요.