Anthropic은 2026년 9월 4일 Claude가 약 11일 동안 페르마의 마지막 정리의 기존 증명을 Lean으로 형식화하고 기계 검증을 마친 연구 결과를 공개했습니다. 9월 5일 새 보도가 나왔지만 연구 실행은 8월에 끝났습니다. 이번 뉴스는 결과 공개이지 AI가 오늘 미해결 문제를 갑자기 풀었다는 이야기가 아닙니다.
새로운 발견이 아니라 각 단계를 검증한다
페르마의 마지막 정리는 2보다 큰 정수 n에 대해 aⁿ+bⁿ=cⁿ을 만족하는 양의 정수 a, b, c가 없다는 명제입니다. Andrew Wiles의 증명은 1995년에 발표됐습니다. 이번 연구는 기존 수학적 논리를 Lean이 처리할 수 있는 형식 언어로 옮겼습니다.
수학 논문은 전문가에게 자명한 단계를 생략할 수 있지만 기계 검증에는 명시적인 정의와 추론이 필요합니다. 공개 저장소는 빌드 검사와 명제 비교 절차를 설명합니다. 실행 완료뿐 아니라 사용한 공리와 결론이 Mathlib의 해당 정리에 부합하는지도 확인합니다.
여러 AI는 어떻게 협업했나
Anthropic에 따르면 수십 개의 Agent가 약 1,300만 줄의 Lean 코드를 만들었습니다. Prove2Me는 정리 간 의존 관계를 정리하고 재사용할 결과를 검색하도록 지원합니다. 대화를 계속 늘리는 대신 대규모 협업의 진행 상태를 공유하는 방식입니다.
Imperial College London의 수학자 Kevin Buzzard도 직접 코드를 컴파일하고 비교 도구를 실행해 통과했다고 밝혔습니다. 다만 거대한 형식화 결과물과 다른 연구자가 읽고 유지·재사용하기 쉬운 수학 라이브러리는 다르며, 인간의 이해는 여전히 별도의 과제라고 지적했습니다.
Claude 구독만으로 재현하는 기능은 아니다
이번 실행에는 Claude Fable 5.1과 대략 비슷한 내부 연구 모델, 다중 Agent 실행 환경, 간헐적인 상위 수준의 인간 지시가 사용됐습니다. 공개된 수치는 약 60억 출력 tokens이지 실제 청구액이 아닙니다. 일반 계정의 무료 기능으로 소개하거나 공개 API 단가로 연구비를 확정해서는 안 됩니다.
코드는 공개됐지만 저장소는 유지보수하지 않고 기여도 받지 않는 연구 결과물이라고 명시합니다. 연구하고 검증할 자료이지 장기 지원 API나 임의의 문제를 채팅에 넣으면 정답을 보장하는 기능이 아닙니다.
중요한 것은 답을 검증할 수 있느냐는 점
일반 AI 사용자에게 중요한 교훈은 답을 만드는 일과 검사하는 일을 구분하는 것입니다. 유창한 설명은 정확성의 증거가 아닙니다. 이번에는 명확한 정리, 공개 코드, 형식 검증 도구가 있어 결과를 살펴볼 수 있습니다. 대규모 검증에 대한 AI의 기여를 보여주지만 모든 전문 분야에 같은 검사 조건이 갖춰졌다는 뜻은 아닙니다.
