클로드, 페르마의 마지막 정리 11일 만에 증명 완성

앤트로픽(Anthropic)이 9월 4일 AI 클로드(Claude)가 페르마의 마지막 정리를 처음부터 끝까지 컴퓨터로 검증할 수 있는 증명을 완성했다고 발표했다. 클로드는 11일 동안 거의 자율적으로 작업하며 증명 지원 시스템 린 4(Lean 4)로 1,300만 줄가량 코드를 생성했다. 앤트로픽은 페르마의 마지막 정리에 대한 최초의 완전한 기계 검증 증명이라고 설명했다.

페르마의 마지막 정리는 n이 2보다 큰 정수일 때 aⁿ＋bⁿ＝cⁿ을 만족하는 양의 정수 a, b, c는 존재하지 않는다는 내용이다. 17세기 프랑스 수학자 피에르 드 페르마(Pierre de Fermat)가 기록을 남긴 이래 350년 넘게 미해결로 남아 있었지만 수학자 앤드루 와일스(Andrew Wiles) 등이 증명을 완성해 1995년 발표했다. 와일스 증명은 129쪽에 달했고 정확성을 확인하는 데 수개월이 걸렸다.

수학 증명은 논리 연결이 한 곳이라도 무너지면 그 뒤 결론까지 성립하지 않을 수 있다. 사람이 읽는 논문에서는 독자에게 자명한 절차가 생략되기도 하지만 컴퓨터에 증명을 확인시키려면 자명하다고 여겨지는 세부 절차까지 엄밀하게 기술해야 한다. 이미 알려진 수학 증명을 증명 지원 시스템이 확인할 수 있는 형태로 다시 쓰는 작업이 형식화다.

임피리얼칼리지런던 수학자 케빈 버자드(Kevin Buzzard)는 2024년부터 페르마의 마지막 정리를 린으로 형식화하는 공동 프로젝트를 이끌어 왔는데 초기 단계 작업 계획만으로도 86쪽에 이른다. 형식화에는 수년이 걸릴 것으로 예상됐다.

앤트로픽 연구자로 AI를 이용한 수학 형식화를 연구하는 톈이 펑(Tianyi Peng)이 클로드에 작업을 맡기자 클로드는 11일 만에 정리 3만 300건 가량을 기계 검증할 수 있는 형태로 증명했고 최종 증명에는 2만 9,500건가량을 썼다. 1,300만 줄가량이라는 규모는 린용 수학 라이브러리 매스립(Mathlib)의 5배가 넘는다. 클로드 에이전트 수십 개가 개념 정의와 중간 정리 증명을 나눠 맡아 더 어려운 명제 증명으로 차례차례 나아갔다.

다만 AI를 여러 개 돌리는 것만으로 작업이 진척된 건 아니다. 초기 시도에서는 각 에이전트가 거대한 프로젝트 진행 상황을 파악하지 못해 서로 성과를 제대로 활용하지 못하는 문제가 생겼다. 장기간에 걸친 복잡한 작업에서는 AI 자체 능력에 더해 어디까지 끝났는지, 다음에 뭘 증명해야 하는지를 관리하는 구조가 필요하다는 이야기다.

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

— Anthropic (@AnthropicAI) September 4, 2026

문제 해결에 쓰인 게 펑 등이 개발한 수학 형식화용 공동 작업 플랫폼 프루브2미(Prove2Me)다. 프루브2미는 정리 사이 의존 관계를 유향 비순환 그래프(DAG)라는 구조로 관리해 여러 클로드가 다음에 다뤄야 할 정리를 확인할 수 있게 했다. 또 정리 내용을 적은 부분과 증명을 별도 파일로 나눠 컴파일 속도를 높였고 각 정리에 자연어 설명을 붙여 이미 완성된 증명을 검색해 재사용하기 쉽게 했다.

완성된 증명은 린 검사를 통과했고 깃허브에 공개됐다. 증명은 린 표준 공리 3개에만 의존하며 증명하지 못한 부분을 일시적으로 통과시키는 sorry 같은 것도 들어 있지 않다. 매스립에 실린 페르마의 마지막 정리 기술과 증명 대상이 일치한다는 점도 비교 도구로 확인했다. 여기에 러스트(Rust)로 구현된 독립 린 커널 나노다(nanoda)에서도 선언 100만 건 이상을 오류 없이 검사할 수 있었다고 보고됐다.

AI가 수학 증명을 대량으로 만들어낼수록 사람만으로 정확성을 확인하는 부담도 커진다. 이에 앤트로픽은 앞으로 사람이 읽는 논문과 함께 컴퓨터로 검증할 수 있는 형식화된 증명을 만드는 게 일반적인 일이 될 것으로 내다봤다. 관련 내용은 이곳에서 확인할 수 있다.