AI가 페르마의 마지막 정리를 "풀었는가"? 11일 만에 완성된 1300만 줄의 증명이 바꾸는 수학

11일 만에 "증명 완료"된 350년의 난제

수학사에서 가장 유명한 난제 중 하나가 다시 세계의 주목을 받고 있다.

Anthropic은 2026년 9월, 자사의 AI "Claude"가 페르마의 마지막 정리에 대해 처음부터 끝까지 컴퓨터로 검증할 수 있는 완전한 형식 증명을 작성했다고 발표했다. 작업에 걸린 시간은 11일. 생성된 Lean 코드의 길이는 약 1300만 줄에 달하며, 작업 중 3만 300개의 정리가 증명되었고, 그 중 2만 9500개가 최종 증명에 사용되었다.

이 숫자만 보면, AI가 인류를 수세기 동안 괴롭혀 온 난제를 단 11일 만에 해결한 것처럼 보일 수 있다. 그러나 여기에는 중요한 구분이 있다. Claude가 한 일은 미지의 해결책을 발견한 것이 아니다. 앤드류 와일스와 리처드 테일러에 의해 1990년대에 완성되고 수학계에서 올바르다고 인정받은 증명을 컴퓨터가 하나씩 논리적으로 확인할 수 있는 언어로 번역하고, 부족한 방대한 중간 부분을 채운 것이다.

"새로운 증명의 발견"이 아닌 "기존 증명의 완전한 기계 검증". 이 차이를 이해하지 않으면 성과를 과대평가하게 된다. 한편, 형식화를 단순한 번역 작업으로 생각하면 그 어려움과 이번의 충격을 과소평가하게 된다.

페르마가 여백에 남긴 한 줄

페르마의 마지막 정리는 양의 정수 a, b, c와 2보다 큰 정수 n에 대해 "a의 n제곱＋b의 n제곱＝c의 n제곱"을 만족하는 조합은 존재하지 않는다는 주장이다.

피에르 드 페르마는 1637년경 고대 그리스의 수학서 『산술』의 여백에 이 주장을 적었고, 놀라운 증명을 발견했지만, 이 여백은 그것을 쓰기에는 너무 좁다고 하는 취지의 말을 남겼다. 그러나 그 증명은 발견되지 않았다.

이후 수세대에 걸쳐 수학자들이 도전했으나, 개별 지수에 대해서는 차례로 증명이 진행되었지만, 일반적인 경우는 350년 이상 해결되지 않은 채로 남아 있었다. 전환점은 1993년. 와일스가 오랜 비밀 연구를 거쳐 증명을 발표했으나, 검증 중 심각한 결함이 발견되었다. 와일스는 테일러와 함께 수정에 착수하여 1994년에 문제를 극복했다. 논문은 1995년에 발표되었다.

이 이야기는 수학에서 "증명 완료"가 누군가가 답을 쓴 순간에 성립되는 것이 아님을 보여준다. 증명은 다른 전문가들이 읽고, 전제나 인용된 정리를 포함하여 검토되고, 논리의 사슬이 끊어지지 않았음을 확인해야 한다. 와일스만큼의 수학자의 증명조차도 첫 발표 후에 결함이 발견된 사실은 그 어려움을 상징한다.

"인간에게는 명백한 것"이 컴퓨터에는 통하지 않는다

일반적인 수학 논문은 인간 전문가가 읽는 것을 전제로 작성된다. 저자는 상식적인 변형을 생략하고, 이미 알려진 결과를 참조하며, 문맥에서 이해할 수 있는 부분을 명시하지 않는다. 독자도 배경 지식을 사용하여 행간을 보충하면서 논리를 따라간다.

그러나 컴퓨터는 "여기는 명백할 것이다"라고 추측해주지 않는다. 정의, 전제, 타입, 사용할 정리, 거기서 도출되는 결론을 엄밀히 지정하고, 각 단계가 규칙에 따라 있음을 보여야 한다. 이 작업에 사용된 것이 정리 증명 지원 시스템 Lean이다.

Lean에서는 증명이 프로그램에 가까운 형식으로 기술된다. 입력된 증명이 논리 규칙에 따라 있는지를 작은 커널이 확인하고, 중간에 도약이 있으면 수용하지 않는다. 그 의미에서 형식 증명은 수학적 주장에 대한 매우 엄격한 자동 테스트에 가깝다.

어려운 점은 와일스의 논문만을 기계어로 바꾸면 끝나는 것이 아니라는 점이다. 인간을 위한 증명은 대수, 기하, 조화 해석, 수론 등의 거대한 지식 체계 위에 서 있다. 필요한 개념이나 보조 정리가 Lean의 공유 라이브러리에 존재하지 않으면, 그것들도 새로 정의하고 증명해야 한다. 이번의 1300만 줄이라는 규모는 이 "보이지 않는 토대"를 하나씩 쌓은 결과이기도 하다.

여러 AI가 거대한 증명을 분업했다

Anthropic의 실험에서는 수십 개의 Claude 에이전트가 병행하여 작업했다. 어떤 에이전트가 개념을 정의하고, 다른 에이전트가 보조 정리를 증명하며, 또 다른 에이전트가 그것들을 결합하여 더 높은 정리로 나아간다. 인간이 공동 연구를 수행하는 것처럼 분업을 AI 그룹이 대규모로 실행한 모양이다.

하지만 처음부터 순조로웠던 것은 아니다. 초기 시도에서는 에이전트가 프로젝트 전체의 진척을 잃고, 서로의 성과를 잘 활용하지 못했다. 장기 작업에서는 개별 AI의 추론력뿐만 아니라, 어떤 과제가 끝났고 다음에 무엇을 증명해야 하는지를 관리하는 시스템이 결정적으로 중요했다.

그래서 사용된 것이 정리 간의 의존 관계를 유향 비순환 그래프로 관리하는 공동 형식화 기반 Prove2Me이다. 증명해야 할 항목을 지도처럼 배치하고, 각 에이전트가 미해결 작업을 선택하고, 완료된 결과를 다른 에이전트가 재사용할 수 있도록 했다. Lean의 컴파일 부하를 억제하고, 자연어에 의한 설명을 검색에 이용할 수 있는 설계도 대규모 분업을 지원했다.

최종적으로 AI 그룹은 약 60억의 출력 토큰을 소비하고, 11일이 채 안 되어 증명의 뿌리에 도달했다. Anthropic에 따르면 Lean에 의한 검사에 더해, 정리의 최종적인 기술이 기존 라이브러리 Mathlib의 페르마의 마지막 정리와 일치하는 것도 비교 도구로 확인했다. 즉, 비슷한 이름의 다른 문제를 증명하고 끝난 것이 아니라, 목표한 주장을 도달했음을 확인한 것이다.

인간의 5년 계획과 AI의 11일은 단순 비교할 수 없다

이번에 자주 대비되는 것은 임페리얼 칼리지 런던의 수학자 케빈 버저드가 이끄는 인간 중심의 형식화 프로젝트이다. 이 프로젝트는 2024년에 시작되어, 여러 해에 걸쳐 페르마의 마지막 정리를 Lean으로 형식화하는 것을 목표로 하고 있다.

"인간이 5년 걸리는 일을 AI가 11일 만에 끝냈다"는 설명은 강렬하지만, 양측의 목적은 완전히 동일하지 않다. Anthropic의 성과는 정리를 처음부터 끝까지 기계 검증 가능하게 하는 것을 최우선으로 했다. 한편, 버저드 등은 공유 라이브러리에 통합할 수 있는 기초 이론을 정비하고, 인간이 현대적인 증명을 탐구하면서 배울 수 있는 동적 문서를 만드는 것도 목표로 하고 있다.

단기간에 "통과"하는 거대한 코드를 만드는 것과, 수학자가 이해하고 재사용하며 다음 연구로 연결할 수 있는 형태로 정리하는 것은 다른 과제이다. Anthropic 자신도 인간의 프로젝트나 기존의 Mathlib이 쌓은 토대를 이용했다고 설명하고 있다. 이번 경쟁을 AI 대 수학자의 단순한 속도 경쟁으로 묘사하는 것은 정확하지 않다.

그럼에도 불구하고, 처음부터 끝까지의 형식화가 연 단위가 아닌 일 단위로 가능해진 사실은 무겁다. 버저드는 자신의 블로그에서 이 성과로부터 수학적으로 새로운 것은 거의 알 수 없다고 하면서도, 수천 페이지에 해당하는 문헌을 AI 그룹이 11일 만에 형식화할 수 있었던 것은 자동 형식화의 가능성을 보여준다고 평가했다. 기존에 99.9% 올바르다고 생각했던 증명에 대해 형식화 후에는 100% 확신한다고 말한 것도 이 성과의 상징으로 받아들여지고 있다.

SNS는 "경탄"과 "그것은 새로운 발견이 아니다"로 양분

발표 후, X, Reddit, Hacker News 등에서는 큰 반향이 일어났다. Lean 공식 계정은 최초의 완전한 컴퓨터 검증 완료 증명으로 성과를 소개했다. Hacker News에서는 관련 게시물에 수백 건의 댓글이 모였고, Reddit에서도 "몇 년 전에는 상상할 수 없었다", "1300만 줄이라는 규모에 압도된다", "2만 9000건 이상의 중간 정리가 필요한가"라는 놀라움의 목소리가 이어졌다.

한편, 가장 많이 반복된 것은 제목의 수용 방식에 대한 경고였다. "AI가 페르마의 마지막 정리를 풀었다"는 표현에 대해 "푼 것은 와일스와 테일러이며, Claude는 기존 증명을 Lean에 형식화했다", "새로운 수학적 발견이 아니다"라는 정정이 다수 게시되었다. 반응 중에는 형식화를 단순한 서식 변환으로 가볍게 보는 의견도 있었지만, 이에 대해서는 장대한 증명의 결핍된 토대를 보완하고 수만 건의 중간 정리를 기계 검증 가능하게 하는 것 자체가 큰 연구상의 성과라는 반론도 있었다.

더 나아가 논의는 연구자의 역할이나 자금 배분에도 미쳤다. 거액의 보조금과 수년의 계획으로 진행해 온 작업에 AI가 단기간에 도달한 것을 연구 생산성의 도약으로 환영하는 목소리가 있다. 그 한편으로는 젊은 연구자의 주제가 AI에 선점될 가능성이나 수학을 손으로 생각하는 동기가 사라질 것이라는 불안도 표명되었다. 버저드의 블로그의 댓글란에서도 "수학의 슬픈 종말"로 보는 의견과 "수학적 내용은 변하지 않았고, 검증 수단이 발전한 것이다"라는 응답이 오갔다.

이들은 무작위 추출된 여론 조사라기보다는 각 SNS 상에서 확인된 게시물의 경향에 불과하다. 그럼에도 불구하고, 이번 성과가 왜 오해받기 쉬우며 동시에 강한 감정을 불러일으키는지를 잘 보여준다. 사람들이 반응하는 것은 하나의 정리뿐만 아니라, "지적 노동의 어디까지가 자동화될 것인가"라는 더 큰 질문이기 때문이다.

올바른 증명과 유용한 증명은 동일하지 않다

이번 성과에는 명확한 약점도 있다. 1300만 줄이라는 규모는 주요 수학 라이브러리 Mathlib 전체의 5배를 넘는다. 기계가 정확성을 확인할 수 있어도, 인간이 전체를 파악하고 필요한 부분을 찾아내어 다른 증명에 재사용하는 것은 쉽지 않다.

수학의 발전에는 올바른 결론뿐만 아니라, 왜 그렇게 되는지를 이해할 수 있는 설명, 개념을 정리하는 적절한 추상화, 다른 분야에서도 사용할 수 있는 보조 정리가 필요하다. 같은 기초 이론을 매번 거대한 전용 코드로 다시 만들면, 형식 증명은 늘어나도 지식 체계는 자라기 어렵다. 검증 가능한 증명이 대량 생산되는 한편, 각각이 호환성이 부족한 고립된 섬이 될 가능성이 있다.

따라서 다음 과제는 AI가 만든 코드를 짧게 정리하고 Mathlib에 환원하며, 인간이 읽을 수 있는 해설과 대응시키는 것일 것이다. AI가 거칠게 길을 열고, 인간과 AI가 그 길을 지도에 하는 것이다. 이번 성과는 목표라기보다는 이 새로운 분업의 출발점으로 보는 것이 좋다.

심사의 한계를 보완하는 "지치지 않는 두 번째 독자"

가장 큰 의의는 유명한 정리를 다시 증명한 것이 아니라, 그동안 비용과 시간 때문에 현실적이지 않았던 기계 검증을 대규모로 실행할 수 있는 가능성을 보여준 점에 있다.

수학 논문의 검증에는 전문가의 긴 시간이 필요하다. 특히 새로운 이론이 수백 페이지에 이르고, 다수의 선행 연구에 의존하는 경우, 심사자가 모든 것을 재구성하는 것은 어렵다. AI가 형식화를 보조할 수 있다면, 인간을 위한 논문과 함께 Lean 등으로 검사할 수 있는 증명서를 제출하는 습관이 확산될지도 모른다.

이는 AI가 수학적 성과를 대량으로 만들어내기 시작한 시대에는 더욱 중요해진다. 인간이 읽는 속도를 초과하여 AI가 논문 후보를 생성하면, 기존의 심사만으로는 따라잡을 수 없다. 생성하는 AI와 형식화하는 AI, 최종적으로 작은 검증 커널이 논리를 확인하는 시스템을 결합함으로써, 적어도 "논리적으로 결론이 도출되었는가"를 효율적으로 확인할 수 있다.

물론, 형식 증명은 논문의 가치를 모두 판단하는 것은 아니다. 정의가 현실의 문제를 적절히 표현하고 있는지, 연구 과제가 중요한지, 증명이 새로운 통찰을 제공하는지, 설명이 교육적인지 등의 판단은 남는다. 또한, 검증 소프트웨어나 기반 라이브러리에 대한 신뢰, 거대 코드의 감사, 계산 자원의 편재와 같은 문제도 피할 수 없다.

그럼에도 불구하고, 지치지 않고 권위에 주저하지 않으며 논리의 빈틈을 놓치지 않는 "두 번째 독자"를 수학이 갖게 되는 의미는 크다.

AI는 수학자를 대체하는가

이번 사건은 AI가 수학자의 일을 일괄적으로 대체했다는 이야기가 아니다. 증명의 원형을 만든 인간, 수십 년 동안 이론을 정비한 연구자, Mathlib과 Lean을 키운 커뮤니티, 증명을 분할하는 기반을 설계한 개발자가 있어야만 Claude의 11일이 성립했다.

그러나 "그래서 AI는 단순한 도구다"라고 정리하는 것도 이르다. 여러 에이전트가 실패에서 재건하고, 의존 관계를 추적하면서 수만 개