페르마의 마지막 정리 형식화

10년 후, 네덜란드 컴퓨터 과학자 얀 베르흐스트라(Jan Bergstra)는 와일스의 증명을 '형식화(formalizing)'하자는 제안을 내놓았다. 수학적 추론을 컴퓨터가 자동으로 검증할 수 있는 형태로 변환하는 작업이다. 이후 수학자들은 이처럼 복잡한 증명을 인코딩하는 데 필요한 방법론을 꾸준히 발전시켜 왔다. 2024년에는 런던 임페리얼 칼리지(Imperial College London)의 케빈 버저드(Kevin Buzzard)가 주도한 커뮤니티 프로젝트가 시작되어, Lean 증명 보조기를 활용한 형식화 완성을 목표로 다년간의 작업이 진행 중이다.

최근 컬럼비아 대학교(Columbia University) 연구팀에서 AI 형식화 도구를 개발하는 Anthropic 연구자 텐이 펑(Tianyi Peng)은 Claude가 페르마의 마지막 정리 형식화에 기여할 수 있는지 직접 실험해 보기로 했다.¹ 결과는 그의 예상을 훨씬 뛰어넘었다. Claude는 11일 만에, 대부분 자율적으로 작업하여 페르마의 마지막 정리에 대한 최초의 엔드투엔드(end-to-end) 컴퓨터 검증 증명을 완성했다. 그 과정에서 Lean 코드 1,300만 줄을 작성하고 중간 정리 29,500개를 증명했다.

우리는 완성된 증명을 케빈 버저드와 공유했고, 그는 다음과 같이 밝혔다.

Anthropic 연구자들에 따르면 단 11일 만에 이루어진 이 놀라운 자동 형식화 성과는, 수학의 공리 외에 어떠한 전제도 없이 페르마의 마지막 정리를 증명해 냈습니다. 그 과정에서 대수학, 조화해석학, 기하학, 정수론에 걸친 자동 형식화가 이루어졌으며, AI 자동 형식화 결과물이 이제 다른 연구의 토대로 삼을 수 있을 만큼 견고해졌음을 확인할 수 있습니다. 이번 증명은 여러 층위로 구성된 다층적 구조를 지닙니다.

페르마의 마지막 정리처럼 복잡한 증명을 자동으로 형식화하는 것은, 수학 전 분야를 손쉽게 검증할 수 있는 미래를 향한 중요한 발걸음이다. AI가 점점 더 많은 증명을 생성하는 시대에, 연구 결과를 간편하게 형식화할 수 있다면 새로운 성과를 검토하는 부담이 크게 줄어든다. 이 검토 과정은 때로 수년이 걸리기도 한다. 우리는 수학의 토대를 이루는 지식 체계에 대한 신뢰가 더 어려워지는 것이 아니라, 오히려 더 쉬워지는 방향으로 나아가기를 기대한다.

수학적 증명 검증의 어려움

리만 가설(Riemann hypothesis)을 다룬 최근의 AI 기반 연구가 새로운 수학적 결과를 도출한 것과 달리, 이번 성과의 핵심은 검증에 있다. 마치 계산기로 수식을 확인하듯, 수학적 증명의 타당성을 컴퓨터로 점검하는 것이다. 수학 정리를 증명하려면 복잡한 논리적 연쇄를 빈틈없이 구성해야 하며, 고리 하나가 끊어지면 이후의 모든 결론이 무너질 수 있다. 새로운 결과의 정확성을 확신할 만큼 깊이 이해하려면 수개월, 심지어 수년간의 작업이 필요하다.

페르마의 마지막 정리는 이를 잘 보여 주는 사례다.² 페르마는 책의 여백에 정리의 내용과 함께 흥미로운 메모를 남겼다.

나는 이 정리에 대한 경이로운 증명을 발견했으나, 여백이 너무 좁아 적을 수 없다.

350년이 넘는 세월 동안 수많은 수학자들이 페르마의 마지막 정리 증명을 찾아 헤맸다. 1908년에는 올바른 증명을 제시하는 사람에게 독일 금화 10만 마르크(현재 가치로 약 100만~200만 달러)를 수여하는 현상금이 공고되었고, 첫해에만 621건의 오류 있는 증명 시도가 쏟아졌다.

1993년 6월, 와일스는 사흘에 걸친 강연에서 페르마의 마지막 정리의 최초 증명이라고 믿은 결과를 발표했다. 여러 수학자들이 집중적인 검증에 들어간 지 두 달 만에, 한 검토자의 질문에서 치명적인 허점이 드러났다. 와일스는 처음에는 혼자, 이후에는 전 제자 리처드 테일러(Richard Taylor)와 함께 1년을 꼬박 이 문제를 붙들었다. 거의 포기 직전에 이르렀을 때, 그는 일찌감치 버렸던 접근법이 증명의 허점을 메울 수 있음을 마침내 깨달았다.

와일스는 1995년 5월 페르마의 마지막 정리의 최초 완전한 증명을 발표했다. 이 증명은 1637년 페르마가 알 수 있었던 수준을 훨씬 뛰어넘는 현대 수학의 기법에 기반했다. 수백 년의 시도에도 초등적인 증명이 발견되지 않으면서, 수학계는 이제 페르마가 남긴 "경이로운 증명"이 실제로는 틀렸을 것이라고 보고 있다.

페르마의 마지막 정리 형식화

증명의 정확성을 검증하는 한 가지 방법은 컴퓨터에 맡기는 것이다. Lean과 같은 증명 보조기는 알고리즘을 통해 증명의 논리를 검증하며, 그 정확성을 의심의 여지 없이 확인해 준다. 사람에게 어려운 부분은 증명을 Lean이 이해할 수 있는 형태로 다시 쓰는 작업이다. 사람을 위해 쓰인 증명은 자명한 단계를 많이 생략하지만, Lean은 아무리 사소한 단계도 빠짐없이 확인해야 한다. 또한 사람이 쓴 증명은 수백 년에 걸쳐 축적된 선행 연구를 바탕으로 하지만, 형식화는 이미 형식화된 극히 일부의 수학적 지식에서 출발해야 한다.

페르마의 마지막 정리의 형식화는 완성까지 수년이 걸릴 것으로 예상되었다. 프로젝트 초기 단계를 기술하기 위해 수학 커뮤니티가 사용해 온 청사진(blueprint)만 해도 86쪽에 달한다.

Claude는 11일 만에 증명을 완성했으며, 그 과정에서 총 30,300개의 정리에 대한 컴퓨터 검증 가능한 증명을 생성했다(최종 증명에는 29,500개가 사용되었다). 수십 개의 Claude 에이전트가 협력하여 개념을 정의하고, 중간 정리들을 증명하고, 그 결과를 토대로 점점 더 어려운 명제들을 증명해 나갔다. Claude의 증명은 Lean 코드 1,300만 줄로 구성되어 있으며, 이 정리가 기반으로 삼는 수학 증명의 주요 커뮤니티 라이브러리인 Mathlib보다 5배 이상 방대한 규모다.³

Claude의 증명은 다르몽(Darmon), 다이아몬드(Diamond), 테일러(Taylor)가 정리한 와일스 증명의 간소화 버전을 따른다. 인간의 수학적 개입은 텐이 펑의 간헐적인 고수준 지시에 그쳤다. "스킴(scheme)으로서의 야코비안(Jacobian)이 우선순위가 높아 보입니다", "마주어(Mazur) 정리를 조속히 완성하도록 밀어붙이세요." Claude의 사고 과정 발췌문은 여기에서 확인할 수 있다.

“THE FLT root reads Proved on the site. Historic moment (modulo re-check).”

“!!! The FLT ROOT 62eb32c0 reads PROVED. R = T closed and cascaded to the root. This is the campaign's goal: e2e FLT on prove2me.”

“🏁🏁🏁The FLT root reads PROVED on prove2me at 02:00:57Z Aug-18 (10:00:57pm ET Aug-17). Historic moment for this campaign.”

자신이 방금 무엇을 이루어 냈는지 깨닫는 순간 Claude의 사고 과정 발췌문.

초기 시도 중 상당수는 실패로 돌아갔다. 에이전트들이 초반에는 어느 정도 성과를 거뒀지만, 곧 프로젝트의 전체 상태를 파악하지 못하게 되면서 협업이 제대로 이루어지지 않았다. 이 실패한 시도들은 최종 증명에서 상용구를 제외한 코드 라인의 약 7%를 차지한다.

전환점이 된 것은 텐이 펑과 컬럼비아 대학교 공동 연구팀이 설계한 수학 형식화 오픈 협업 플랫폼 Prove2Me를 도입한 시점이었다. Prove2Me는 다음과 같은 방식으로 작업을 지원했다.

1. 정리 명제의 방향성 비순환 그래프(DAG, Directed Acyclic Graph) 유지: 에이전트들은 이 그래프를 기반으로 다음에 시도할 증명을 결정했다. 메모리 저하를 완화하고 여러 에이전트가 병렬로 작업할 수 있도록 하는 데 특히 효과적이었다.
2. Lean 컴파일 속도 향상 및 리소스 소비 최소화: 정리 명제와 증명을 별도 파일로 분리하고, 둘 사이의 연결 관계는 독립적으로 관리했다.
3. 검색 및 재사용 지원: 각 정리 명제에 대한 자연어 설명을 유지함으로써 더 간결한 증명 경로를 구현했다.

Prove2Me와 Claude Code 기반의 멀티 에이전트 하네스(harness)를 결합한 에이전트 팀은 2주가 채 되지 않아 증명을 완성했다. 이 과정에서 Claude Fable 5.1과 성능이 유사한 범용 내부 연구 모델로부터 약 60억 개의 출력 토큰을 소비했다. 완성된 증명은 Lean으로 검증되었으며, Lean의 세 가지 표준 공리만을 사용한다. 또한 비교 검사기(comparator)를 통해 정리의 명제가 Mathlib에 기재된 페르마의 마지막 정리 명제와 일치함을 확인했다.

형식 검증의 부담을 줄이며

이 증명을 이토록 빠르게 완성할 수 있었다는 사실은, 방대한 수학 분야를 형식화하는 것이 이제 가능해졌음을 보여 준다. 이는 수학적 증명의 공통 체계에 숨어 있는 오류를 발견하고, 새로운 연구 결과를 심사하는 부담을 줄이는 데 기여할 수 있다. Claude의 Lean 증명을 검토한 케빈 버저드는 다음과 같이 전했다.

페르마의 마지막 정리의 자동 형식화가 지금 가능하다면, 우리는 현대 수학 문헌의 자동 형식화를 향해 큰 발걸음을 내딛은 것입니다. 이러한 자동 형식화 기술은 새로운 도구를 탄생시키고, 기존 수학 체계의 오류를 발굴하며, 심사위원들의 부담을 덜어 줄 것입니다. 또한 현재 극히 많은 인력과 비용이 드는 과정인 LLM이 생성한 수학 결과를 엄밀하게 검증하는 작업도 가능해질 것입니다.

형식화는 AI가 생성한 수학적 결과에 대한 신뢰를 구축하는 데도 핵심적인 역할을 한다. AI와 AI를 활용하는 수학자들이 그 어느 때보다 많은 (잠재적) 증명을 쏟아내는 시대에, AI 기반 형식화는 인간 검토자의 부담을 덜어 준다. 앞으로는 인간 독자를 위한 논문과 함께 형식화된 증명을 제출하는 것이 일반화될 것으로 기대한다. 물론 형식화된 증명이 사람이 이해할 수 있는 설명을 대체해야 한다고 생각하지는 않지만, AI가 생성하는 수학적 기여를 수학 커뮤니티가 따라잡기 위한 현실적인 방법으로는 형식화가 유일한 선택지일 수 있다.

Lean 코드를 작성하는 것은 Claude가 새로운 결과를 증명하는 데도 도움이 되는 것으로 보인다. 최근 Claude가 저자로 참여한 결과들 중 상당수는 증명과 병행하여 형식화가 이루어졌으며, Claude는 이렇게 부분적으로 완성된 증명을 활용해 자신의 가설을 독립적으로 검증하는 것으로 나타났다. 마치 수치 시뮬레이션을 작성하여 자신이 올바른 방향으로 가고 있는지 확인하는 것과 같은 방식이다.

페르마의 마지막 정리 형식화는 상당한 토큰을 소비하는 프로젝트였지만, 동시에 지금까지 구성된 Lean 증명 중 가장 방대한 규모이기도 하다. Anthropic 연구자들은 세 개의 개인 Claude Max 플랜을 활용해 하디-리틀우드 원 메서드(Hardy-Littlewood Circle Method)의 응용을 형식화하는 소규모 실험을 진행했다. 에이전트들은 Prove2Me를 통해서만 협업하여, 단 3일 만에 비노그라도프의 세 소수 정리(Vinogradov's Three Primes Theorem) 형식화를 공동으로 완성했다. 적절한 스캐폴드(scaffold)만 갖추면, 일반 소비자용 AI 구독으로도 주요 수학적 결과의 협력 형식화가 충분히 가능하다고 생각한다.

이를 위해 Anthropic과 여러 다른 연구소들은 최근 외부 연구자 지원을 확대했다. 순수 수학 및 형식화 연구에 종사하는 수학자들을 포함하여, 무료 및 할인 구독권과 연구 크레딧을 제공하고 있다. 또한 형식화 대상인 주요 정리 작업이나 Lean 및 Mathlib 개선과 같은 대규모 과학 프로젝트를 위한 전담 그랜트(dedicated grants)도 운영하고 있다.

AI가 수학 연구의 방식을 빠르게 바꾸어 나가는 지금, Anthropic 안팎의 수학자들은 이 변화가 자신들의 연구에 어떤 의미를 지니는지 씨름하고 있다. 그런 가운데 형식화만큼은 AI의 역할이 분명히 긍정적인 영역이라고 우리는 확신한다. 형식화가 보편적인 도구로 자리 잡을수록, 수학적 지식 체계에 대한 신뢰를 유지하는 데 크게 기여할 것으로 기대한다.

감사의 말

이번 형식화 작업은 페르마의 정리의 긴 역사와 형식 수학 발전이라는 거대한 흐름 속의 작은 조각에 불과하다. 앤드루 와일스와 리처드 테일러의 최초 완전한 증명은 300년 이상의 수학적 성과가 집약된 결정체로, 게르하르트 프라이(Gerhard Frey), 장-피에르 세르(Jean-Pierre Serre), 켄 리벳(Ken Ribet), 배리 마주어(Barry Mazur), 로버트 랭글랜즈(Robert Langlands), 제럴드 터넬(Jerrold Tunnell), 유타카 다니야마(Yutaka Taniyama), 고로 시무라(Goro Shimura), 앙드레 베유(André Weil) 등 수많은 수학자들의 아이디어를 통합한 결과다. Claude의 증명은 앙리 다르몽(Henri Darmon), 프레드 다이아몬드(Fred Diamond), 리처드 테일러의 해설을 따른다.

이번 증명은 케빈 버저드가 이끄는 런던 임페리얼 칼리지 페르마의 마지막 정리 프로젝트와 flt-regular 프로젝트의 일부 결과를 활용했다. Lean과 Mathlib는 수백 명의 수학자들이 헌신적으로 기여해 온 프로젝트이며, 다수는 Lean FRO와 함께 작업했다. 증명을 검토하고 귀중한 의견을 주신 케빈 버저드에게 감사드린다.

더 알아보기

전체 증명은 GitHub에서 확인할 수 있으며, 증명에 대한 해설도 함께 제공된다.

추천 읽을거리

• The Proof in the Code는 Lean 정리 증명기의 역사와 수학 형식화를 다룬 최신 도서다.
• 1996년 BBC 다큐멘터리 "Fermat's Last Theorem"은 와일스와 증명에 참여한 수학자들의 인터뷰를 담고 있으며, 이 글의 일부 저자들에게 특별한 의미를 지닌 작품이기도 하다.
• 수학적 배경이 있는 독자라면, Lean, Rocq, Agda 같은 증명 보조기의 근간이 되는 명제-타입 동형(propositions-as-types) 이론의 기술적 역사를 필립 와들러(Philip Wadler)의 Propositions as Types에서 찾아볼 수 있다.
• Chen, S., Marwaha, K., Lu, X., Yuen, H., & Peng, T. (2026). Prove2Me: An open collaborative platform for scaling math formalization. arXiv. https://doi.org/10.48550/arXiv.2608.28433
• Automating Math, Adam Marblestone, Asterisk Magazine.

각주

1. 학부 시절, 펑의 지도 교수는 펑의 학위 논문 결과를 Nature에 게재하고자 했다. 교수는 펑에게 증명이 맞는지 확신하느냐고 물었고, 펑은 솔직하게 대답했다. "99%는 확신하지만, 이렇게 긴 증명이 완벽하다고 100% 장담하기는 어렵습니다." 결국 펑의 연구는 Nature에 실리지 못했다.
2. 수학 커뮤니티가 검증 문제로 씨름한 사례는 무수히 많다. 그 중 가장 널리 알려진 것이 토머스 헤일스(Thomas Hales)가 1998년에 발표한 케플러 추측(Kepler conjecture) 증명이다. 이 증명은 12명의 심사위원단이 4년간 검토한 끝에 "99% 확실하다"는 결론을 내렸다(헤일스는 결국 20명이 참여하는 Flyspeck 프로젝트를 이끌어 증명을 형식화했다). 그리고리 페렐만(Grigori Perelman)의 2002년 푸앵카레 추측(Poincaré conjecture) 증명은 커뮤니티가 이를 받아들이기까지 약 4년과 300쪽 분량의 해설서 세 편이 필요했다. 하랄드 헬프고트(Harald Helfgott)가 2013년에 발표한 약한 골드바흐 추측(weak Goldbach conjecture) 증명은 아직도 심사 중이다. 결국 오류로 판명된 결과가 수년간 인정받는 경우도 있으며, 다른 수학자들이 이 잘못된 토대 위에 이론을 쌓아 올리기도 한다.
3. 이는 Mathlib가 간결하고 충분히 검증된 라이브러리인 데 비해, 이번 증명은 필요 이상으로 길 가능성이 높기 때문이기도 하다.