Claude, 11일 만에 페르마의 마지막 정리 형식화했다고 발표

무엇을 완성했나

페르마의 마지막 정리는 3보다 큰 정수 n에 대해 양의 정수 a, b, c가 aⁿ+bⁿ=cⁿ을 만족할 수 없다는 명제입니다. 앤드루 와일스가 1990년대에 인간 수학자를 위한 증명을 완성했지만, 이를 컴퓨터가 모든 단계를 검사할 수 있는 형식으로 바꾸는 일은 별도의 대형 엔지니어링 과제입니다.

Anthropic에 따르면 Claude를 활용한 팀은 약 11일 만에 Lean 기반의 엔드투엔드 형식화를 완성했습니다. 이는 Claude가 새로운 증명을 발견했다는 뜻이 아닙니다. 인간 수학 논문에서 흔히 쓰이는 “자명하다” 또는 생략된 단계를 없애고, 정의와 타입, 보조정리, 의존관계를 모두 명시된 코드로 옮겼다는 의미입니다. Lean은 각 결론이 허용된 공리와 기존 정리에서 합법적으로 도출되는지 확인합니다.

프로젝트의 규모

공개된 설명에 따르면 약 1300만 줄의 Lean 코드와 3만 개 이상의 중간 정리가 만들어졌으며, 최종 증명에는 약 2만9500개의 결과가 사용됐습니다. 코드 규모는 Lean의 핵심 수학 라이브러리인 Mathlib의 5배를 넘는다고 합니다. 또한 최종 형식화가 Lean의 표준 공리 세 개에만 의존하고, 정리의 명제가 Mathlib에 있는 페르마의 마지막 정리와 일치하는지 프로그램으로 비교했다고 밝혔습니다. 다만 이 수치와 평가는 프로젝트 측 발표에 기반하며, AI가 새로운 수학 이론을 만들었다는 의미는 아닙니다.

멀티 에이전트보다 중요한 Harness

초기 멀티 에이전트 구성은 여러 부분에서 빠르게 결과를 냈지만, 프로젝트가 커지자 전체 상태와 의존관계를 추적하기 어려워졌습니다. 작업이 중복되고 부분 증명을 합치는 일도 복잡해졌습니다. 전환점은 Prove2Me와 Claude Code 기반의 멀티 에이전트 Harness를 도입한 것이었습니다.

이 시스템은 증명을 정리 노드로 구성된 방향성 비순환 그래프로 표현합니다. 어떤 정리가 완료됐는지, 어떤 선행 조건이 필요한지, 이미 만든 결과를 어디에서 재사용할 수 있는지를 관리합니다. 정리의 명제와 증명 코드를 분리하고 자연어 설명을 검색에 활용하며 Lean 컴파일도 빠르게 처리합니다. 에이전트들은 정의, 중간 보조정리, 상위 정리, 최종 통합을 나눠 맡았고, 인간은 주로 우선순위와 방향을 제시했습니다. 보고된 출력 토큰 사용량은 약 60억 개입니다.

의미와 한계

이 사례의 핵심은 AI가 수학 문제의 답만 제시한 것이 아니라, 작업을 분해하고 의존관계를 관리하며 컴파일 오류를 고치고 결과를 재사용하는 형식 수학의 전체 흐름에 참여했다는 점입니다. 이런 방식이 확장되면 기존 수학 문헌의 형식화 속도가 빨라질 가능성이 있습니다.

그러나 Lean이 보장하는 것은 주어진 기초와 형식화 안에서 추론이 맞다는 사실입니다. 모델링이 적절한지, 정리의 표현이 원래 의도와 맞는지까지 자동으로 판단하지는 않습니다. 앞으로의 수학 AI 경쟁에서는 모델의 추론 능력뿐 아니라 메모리, 의존성 그래프, 검증기, 협업 Harness의 안정성이 함께 중요해질 것입니다.

출처: 퀀텀비트