AI 개발 기업인 Anthropic은 2026년 9월 4일, AI 'Claude'가 페르마의 마지막 정리에 대해 처음부터 끝까지 컴퓨터로 검증할 수 있는 증명을 완성했다고 발표했습니다. Claude는 11일 동안 거의 자율적으로 작업하여 증명 보조 시스템 'Lean 4'로 약 1,300만 행의 코드를 생성했습니다. Anthropic은 페르마의 마지막 정리에 대해 최초의 완전한 기계 검증 증명이라고 설명하고 있습니다.Formalizing Fermat's Last Theorem \ Anthropichttps://www.anthropic.com/research/formalizing-fermats-last-theorem
Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants like Lean can verify—can help.Last month, Claude completed the first formalized proof of Fermat’s Last Theorem, one of…pic.twitter.com/pdT8zwlV4A
페르마의 마지막 정리는 "n이 2보다 큰 정수인 경우, aⁿ＋bⁿ＝cⁿ을 만족하는 양의 정수 a, b, c는 존재하지 않는다"라는 것입니다. 17세기 프랑스의 수학자 피エール 드 페르마가 남긴 이래 350년 이상 미해결로 남아 있었으나, 수학자 앤드루 와일스 등이 증명을 완성하여 1995년에 발표했습니다. 와일스의 증명은 129페이지에 달하며, 정당성을 확인하는 작업에는 수개월이 걸렸습니다.
수학의 증명에서는 논리의 연결이 한 곳이라도 무너지면 그 뒤의 결론까지 성립하지 않게 될 가능성이 있습니다. 사람을 대상으로 한 논문에서는 독자에게 명백한 단계가 생략되기도 하지만, 컴퓨터가 증명을 확인하게 하려면 '명백하다'고 여겨지는 세부적인 단계까지 엄격하게 기술해야 합니다. 알려진 수학적 증명을 증명 보조 시스템이 확인할 수 있는 형태로 다시 쓰는 작업이 '형식화'입니다. 임페리얼 칼리지 런던의 수학자 케빈 버저드 씨는 2024년부터 페르마의 마지막 정리를 Lean으로 형식화하는 공동 프로젝트를 이끌고 있으며, 초기 단계의 작업 계획만 해도 86페이지에 달합니다. 형식화에는 수년이 걸릴 것으로 예상되었습니다. Anthropic의 연구원이자 AI를 통한 수학 형식화를 연구하는 텐이 펑 씨가 Claude에게 작업을 시킨 결과, Claude는 11일 만에 약 3만 300개의 정리를 기계 검증 가능한 형태로 증명했으며, 최종 증명에서는 약 2만 9500개를 사용했습니다. 약 1,300만 행이라는 규모는 Lean용 수학 라이브러리 'Mathlib'의 5배 이상이라고 합니다. 수십 개의 Claude 에이전트가 개념 정의와 중간 정리 증명을 분담하여, 더 어려운 명제의 증명으로 순차적으로 나아갔습니다.
하지만 단순히 여러 AI를 가동하는 것만으로 작업이 진행된 것은 아니며, 초기 시도에서는 각 에이전트가 거대한 프로젝트의 진행 상황을 파악하지 못해 서로의 성과를 제대로 활용하지 못하는 등의 문제가 발생했습니다. 장기간에 걸친 복잡한 작업에서는 AI 자체의 능력에 더해 '어디까지 끝났는지', '다음으로 무엇을 증명해야 하는지'를 관리하는 시스템이 필요해진다는 것입니다. 문제 해결에 사용된 것은 펜 씨 등이 개발한 수학 형식화용 협업 플랫폼 'Prove2Me'입니다. Prove2Me는 정리 간의 의존 관계를 방향성 비순환 그래프(DAG)라고 불리는 구조로 관리하여, 여러 Claude가 다음에 작업해야 할 정리를 확인할 수 있도록 했습니다. 또한 정리의 내용을 기술한 부분과 증명을 별도의 파일로 분리하여 컴파일 속도를 향상시키고, 각 정리마다 자연어로 된 설명을 첨부함으로써 이미 완성된 증명을 검색해 재사용하기 쉽게 만들었습니다.
완성된 증명은 Lean의 검증을 통과했으며, GitHub에 공개되어 있습니다. 증명은 Lean의 표준적인 3가지 공리에만 의존하고 있으며, 미증명 부분을 임시로 통과시키는 'sorry' 등도 포함되어 있지 않습니다. Mathlib에 수록된 페르마의 마지막 정리 기술과 증명 대상이 일치한다는 점도 비교 도구를 통해 확인되었습니다. 나아가 Rust로 구현된 독립적인 Lean 커널 'nanoda'에서도 100만 건 이상의 선언을 에러 없이 검사할 수 있었다고 보고되었습니다. GitHub - anthropics/fermats-last-theorem · GitHubhttps://github.com/anthropics/fermats-last-theorem AI가 수학 증명을 대량으로 생성할 수 있게 될수록, 인간만으로 정당성을 확인하는 부담도 커집니다. 이에 따라 Anthropic은 향후 인간을 위한 논문과 함께 컴퓨터로 검증할 수 있는 형식화된 증명을 작성하는 것이 일반화될 것으로 예상한다고 밝혔습니다.
원문 보기 | 출처: Gigazine