페르마 대정리, AI가 11일 만에 기계 검증을 끝냈다

effidev·2026년 9월 5일

수학계가 몇 년으로 잡아 놓은 일정이 있었다. 11일 만에 끝났다.

2026년 9월 4일 앤트로픽이 페르마의 마지막 정리(Fermat’s Last Theorem, 이하 FLT)의 첫 완전 기계 검증 증명을 공개했다. 클로드가 대체로 혼자서 11일 동안 작업해 린(Lean)이라는 언어로 증명을 써냈고, 그 코드가 컴퓨터 검사를 통과했다.

이 글은 이런 분을 위해 썼다. “AI가 페르마 대정리를 증명했다”는 문장을 보고 이게 정확히 무슨 뜻인지 궁금한 분, 그리고 에이전트 여러 개를 붙여 긴 작업을 시키려는데 실제로 어디서 무너지고 무엇으로 버텼는지 사례가 필요한 분이다. 수학 지식은 필요 없다. 대신 숫자와 절차는 발표문 원문에서 그대로 가져왔다.

먼저 용어 하나만 풀고 가자. **형식화(formalization)**는 사람이 읽는 증명을 컴퓨터가 한 줄씩 검사할 수 있는 코드로 옮기는 일이다. 새 증명을 만드는 게 아니다. 이미 맞다고 인정받은 증명을 기계가 따질 수 있는 형태로 다시 적는 작업이다. 이 차이가 이 사건의 거의 전부다.

11일이라는 숫자가 왜 걸리나

FLT는 1637년경 페르마가 디오판토스의 『산술』 여백에 적어 둔 주장이다. a^n + b^n = c^n을 만족하는 양의 정수 a, b, c는 n이 2보다 클 때 존재하지 않는다는 것. 페르마는 여기에 유명한 한 줄을 덧붙였다.

나는 이것의 참으로 놀라운 증명을 발견했으나, 이 여백은 그것을 담기에 너무 좁다.

350년 넘게 아무도 못 풀었다. 1908년에는 정확한 증명에 10만 독일 금마르크(앤트로픽 발표문 기준 오늘날 100~200만 달러)의 상금이 걸렸고, 첫 해에만 틀린 증명이 621건 쏟아졌다. 참고로 초등적인 증명은 수 세기가 지나도록 나오지 않았고, 그래서 수학계는 지금 페르마가 봤다는 그 “놀라운 증명”이 틀렸다고 본다.

앤드루 와일즈가 1995년 5월에 첫 정확한 증명을 발표하면서 문제 자체는 끝났다. 남은 건 형식화였다. 네덜란드 컴퓨터과학자 얀 베르흐스트라가 2000년대 중반에 제안했고, 2024년 임페리얼 칼리지 런던의 케빈 버자드가 린으로 완성하겠다며 커뮤니티 프로젝트를 띄웠다.

여기서 걸리는 대목이 이거다. 앤트로픽 발표문은 이렇게 적었다.

FLT의 경우, 형식화 과정은 몇 년이 걸릴 것으로 예상됐다. 커뮤니티가 프로젝트의 초기 단계를 설명하려고 써 온 설계도(blueprint)만 86쪽에 이른다.

초기 단계 설명서가 86쪽이다. 그 전체 일정이 11일에 끝났다.

옮겨 적기가 왜 그렇게 어려운가

사람이 읽는 증명은 “자명하므로 생략한다”를 마음껏 쓴다. 린은 그걸 못 봐준다. 아무리 사소해도 모든 단계를 봐야 한다. 게다가 사람의 증명은 수백 년치 출판물 위에 서 있는데, 형식화는 이미 형식화가 끝난 아주 작은 조각에서 출발해야 한다.

검증이 왜 필요한지는 와일즈 본인의 이력이 그대로 보여준다. 1993년 6월 사흘짜리 연속 강연에서 증명을 발표했는데, 여러 수학자가 두 달간 검토하던 중 한 명이 던진 질문에서 치명적인 구멍이 드러났다. 와일즈는 1년을 매달렸고, 처음엔 혼자, 나중엔 제자였던 리처드 테일러와 함께였다. 포기 직전에야 예전에 버렸던 접근이 구멍을 메운다는 걸 깨달았다. 그렇게 나온 최종본이 129쪽이다.

129쪽을 사람이 검토하는 데 수개월이 걸렸다. 기계가 검사하면 그 부담이 사라진다. 형식화의 값어치는 거기 있다.

리만 가설 때와는 다른 종류의 사건이다

최근에도 AI가 수학에서 성과를 냈다는 소식은 몇 번 있었다. 앤트로픽은 이번 건이 그것들과 다른 축에 있다고 발표문에서 선을 그었다.

새 수학을 만들어낸 리만 가설 관련 최근 AI 작업과 달리, 여기서 새로운 것은 검증이다. 수학적 증명을 계산기로 계산을 확인하듯 검사하는 일 말이다.

같은 “AI가 수학을 했다”는 헤드라인 아래 두 가지가 섞여 있다는 뜻이다. 하나는 없던 결과를 만드는 것, 다른 하나는 있는 결과가 진짜 맞는지 기계가 따지게 만드는 것. 이번 건은 후자다. 그래서 뒤에 나올 검증자의 냉정한 평가와도 모순되지 않는다.

1,300만 줄이 어느 정도인가

앤트로픽이 밝힌 규모는 이렇다.

• 린 코드 1,300만 줄
• 중간 정리 3만 300개를 증명, 그중 2만 9,500개를 최종 증명에 사용
• 출력 토큰 약 60억 개
• 모델은 “클로드 페이블 5.1에 대략 견줄 만한” 사내 범용 연구 모델

1,300만 줄이 감이 안 잡히면 두 가지로 바꿔 보면 된다. 첫째, 이 증명이 딛고 선 매스립(Mathlib)—커뮤니티가 쌓아 온 수학 라이브러리—보다 5배 이상 크다. 둘째, 사람이 하루에 500줄씩 쉬지 않고 써도 약 71년치다(1,300만 ÷ 500 = 2만 6천 일).

코드를 직접 받아 돌려 본 버자드의 실측은 숫자가 조금 다르고, 더 아프다.

거대한 증명이다(1,340만 줄이 넘는다). 96코어 머신에서 린의 수학 라이브러리보다 컴파일에 거의 20배가 걸린다.

램 500GB짜리 머신에서도 파일 사이를 오갈 때 린이 굼떴다고 적었다. 그 머신도 앤트로픽이 내줬다.

첫 시도는 무너졌다 — 이유가 익숙하다

여기가 에이전트를 굴려 본 사람에게 가장 쓸모 있는 대목이다. 앤트로픽은 실패를 그대로 적었다.

클로드의 초기 시도 여럿이 실패했다. 에이전트들이 초반에는 성과를 냈지만, 곧 프로젝트의 상태를 놓쳤고 서로 협업하기를 멈췄다. 그 실패한 작업물이 최종 증명에서 보일러플레이트를 뺀 줄 수의 약 **7%**를 차지한다.

에이전트를 여러 개 붙여 본 적 있다면 낯익은 실패다. 처음엔 잘 돌다가, 맥락이 길어지면 각자 무슨 작업이 끝났는지를 잊고 같은 일을 다시 하거나 남의 결과를 무시한다. 이 문제는 이전에 다룬 여러 에이전트가 서로 반박하며 난제를 푼 사례, 그리고 에이전트들이 자기들끼리 쪽지판을 만들어 버린 사건과 같은 뿌리에서 나온다. 모델이 약해서가 아니라 상태를 어디에 두느냐의 문제다.

버틴 것은 모델이 아니라 게시판이었다

성공은 **프루브투미(Prove2Me)**로 갈아탄 뒤에 나왔다. 컬럼비아대의 톈이 펑(Tianyi Peng)과 동료들이 만든, 수학 형식화용 공개 협업 플랫폼이다. 발표문이 꼽은 역할이 셋이다.

1. 정리 명제의 방향성 비순환 그래프(DAG)를 유지한다. 에이전트가 “다음에 뭘 증명할지”를 이 그래프를 보고 정한다. 기억이 흐려지는 문제를 줄이고 여러 에이전트가 동시에 일하게 하는 데 특히 효과가 있었다.
2. 명제와 증명을 다른 파일로 갈라 놓는다. 둘 사이 연결은 따로 관리한다. 린 컴파일이 빨라지고 자원 소모가 준다.
3. 정리마다 자연어 설명을 붙여 둔다. 검색과 재사용이 되니 증명 경로가 단순해진다.

정리하자면 공유 작업 목록을 코드 바깥에 두고, 컴파일 단위를 잘게 쪼개고, 검색 가능한 설명을 붙인 것이다. 셋 다 에이전트를 여럿 굴릴 때 그대로 옮겨 쓸 수 있는 설계다.

발표문에는 클로드가 따라간 프루브투미 계획의 주요 이정표 그래프도 실려 있다. 색으로 구분된 세 구간이 최종 목표로 가는 길에 반드시 통과해야 했던 세 개의 핵심 하위 정리이고, 그 그래프는 와일즈의 원래 증명을 가깝게 따라간다. 사람이 짠 증명의 뼈대를 그대로 작업 분해 구조로 쓴 셈이다.

린을 쓰는 게 모델 자신에게도 도움이 된다는 관찰

발표문 뒤쪽에 지나가듯 적힌 문단이 하나 있는데, 형식화 얘기보다 개발 쪽에 더 쓸모 있다.

린을 쓰는 것이 클로드가 새로운 결과를 증명하는 데도 도움이 되는 듯하다. 최근 클로드가 저자로 참여한 결과들 중 다수가 증명과 나란히 형식화됐고, 클로드는 그 부분 증명들을 이용해 자기 가설을 독립적으로 점검하는 것으로 보인다. 방향이 맞는지 확인하려고 수치 시뮬레이션을 짜는 것과 비슷하다.

익숙한 패턴이다. 코드를 짜게 시킬 때 테스트를 함께 쓰게 하면 결과가 나아지는 것과 같은 구조다. 자기 주장에 대해 스스로 돌려 볼 수 있는 검사기를 옆에 두는 것 — 그게 수학에서는 린이고, 우리 쪽에서는 타입 검사기와 테스트다.

사람이 넣은 말은 이 정도가 전부였다

수학적 입력은 톈이가 가끔 던진 고수준 지시로 제한됐다고 발표문은 적는다. 실제로 인용된 문장이 이렇다.

“스킴으로서의 야코비안이 우선순위 높아 보인다” “마주르 정리를 빨리 끝내는 쪽으로 밀어라”

작업 지시지 수학 풀이가 아니다. 증명이 뿌리까지 통과한 순간 클로드가 남긴 기록도 공개됐다.

“FLT 루트가 프루브투미에서 PROVED로 읽힌다. 2026년 8월 18일 02:00:57Z. 이 캠페인의 역사적 순간.”

발표는 9월 4일이지만 증명이 닫힌 건 8월 18일이다. 그 사이에 검증과 정리 작업이 있었다는 뜻이다.

검증한 수학자의 답은 “수학적으로는 없다”였다

버자드는 축하부터 했다. 코드베이스를 컴파일하고 비교기(comparator)를 돌려 **“확인된다(it checks out)”**고 적었다. 이건 독립 검증이라 무게가 다르다.

그런데 같은 글에서 그는 이렇게 못박는다.

수학적으로 앤트로픽의 이 작업은 우리에게 사실상 아무것도 알려주지 않는다. 나는 FLT의 증명이 맞다고 99.9% 확신한다고 공개적으로 말해 왔고, 정수론 커뮤니티 대다수는 100% 확신한다.

새 수학이 나온 게 아니라는 뜻이다. 그럼 뭐가 남나. 바로 다음 문단이 답이다.

다만 이 작업이 알려주는 것은 자동형식화(autoformalization) 분야에서 지금 무엇이 가능한가이다. 수천 쪽의 문헌을 어떤 AI 스웜이 11일 만에 끝에서 끝까지 형식화할 수 있다면, 앞으로는 현대 연구가 그때그때 형식화되는 광경을 보게 될 것이다.

“AI가 페르마 대정리를 풀었다”가 아니라 **“수천 쪽짜리 문헌을 기계가 검사 가능한 형태로 옮기는 일이 이제 2주 안에 된다”**가 이 사건의 문장이다.

20년 묵은 목록의 마지막 칸이 채워졌다

버자드가 짚은 부수 효과 하나가 상징적이다. FLT는 프리크 비데이크(Freek Wiedijk)의 100대 형식화 과제 목록에서 마지막으로 남아 있던 정리였다. 이번 건으로 20년 된 벤치마크가 끝났다.

어디까지가 맞는 말인가

과장 없이 범위를 그으면 이렇다.

• 새 수학이 아니다. 이미 인정된 와일즈의 증명을 옮겨 적은 것이다.
• 현대적 증명이 아니다. 버자드 본인이 형식화 중인 노선(카레·테일러 등)이 아니라 1995년 다르몽–다이아몬드–테일러 해설판을 따른다. 랑글랜즈–튜널 정리와 리벳의 레벨 낮추기 정리를 거치는 경로다.
• 커버 범위에 이음매가 있다. 앤트로픽 저장소는 폰테인 이론과 마주르의 아이젠슈타인 아이디얼을 전개해 프레이 곡선 쪽을 막는다. 버자드는 남는 구간을 두고 **홀수 정규 소수는 베스트–버크벡–브라스카–로드리게스가 이미 형식화해 뒀고, 가장 작은 비정규 소수가 37이라 “다 괜찮다”**고 정리했다.
• 사람이 읽을 문서는 아니다. 버자드가 EPSRC 지원으로 하던 일—매스립에 현대 정수론 기본 객체를 넣는 PR, 그리고 사람이 현대적 증명을 탐색할 수 있는 동적 문서—은 그대로 남았다. 그는 앤트로픽이 그걸 할 것 같지는 않다고 적었다.
• 검사 기준은 명시돼 있다. 완성된 증명은 린이 검사했고, 린의 표준 공리 3개만 쓴다. 별도 비교기가 정리의 명제가 매스립의 FLT 명제와 일치하는지 확인했다.

이 일을 개인이 흉내 낼 수 있나 — 3일짜리 실험이 있다

토큰 60억 개짜리 프로젝트를 개인이 따라 할 수는 없다. 그런데 발표문 뒤쪽에 규모를 확 줄인 실험이 붙어 있다.

앤트로픽 연구자들이 개인 클로드 맥스 플랜 3개로 하디–리틀우드 원 방법의 응용을 형식화하는 작은 실험을 했다. 전적으로 프루브투미를 통해 협업하면서, 에이전트들이 비노그라도프의 세 소수 정리 형식화를 단 3일 만에 함께 끝냈다.

발표문은 여기에 “적절한 스캐폴드만 있으면 소비자용 AI 구독으로도 주요 결과의 협업 형식화가 가능하다고 본다”는 결론을 붙였다. 핵심은 구독 등급이 아니라 스캐폴드, 곧 작업 그래프·컴파일 분할·검색 가능한 설명이라는 그 세 장치다.

숫자만 따로 모으면

지금 직접 열어 볼 수 있는 것

말로만 듣고 넘기기엔 아까운 사건이라, 확인 경로를 적어 둔다.

1. 증명 저장소를 본다. github.com/anthropics/fermats-last-theorem이다. 언어는 린, 라이선스는 아파치 2.0, 저장소 생성일은 2026년 9월 4일이다. 다만 앞에서 본 대로 전체 컴파일은 개인 장비로 감당할 규모가 아니다. 버자드는 앤트로픽이 함께 준 HTML 문서를 클론해서 브라우저로 여는 쪽이 실무적으로 편했다고 적었다.
2. 발표문의 사고 기록 발췌를 읽는다. 에이전트가 목표에 도달했음을 깨닫는 순간의 로그가 그대로 실려 있다. 멀티 에이전트 하네스를 설계 중이라면 실패 서술(7% 문단)과 짝지어 읽는 게 좋다.
3. 자기 프로젝트에 스캐폴드 셋을 대본다. 공유 작업 그래프가 코드 바깥에 있는가, 컴파일·검증 단위가 잘게 쪼개져 있는가, 산출물마다 검색 가능한 자연어 설명이 붙는가. 이 셋이 없으면 에이전트 수를 늘려도 7% 실패분만 늘어난다.
4. 연구자라면 지원 창구를 본다. 발표문은 앤트로픽을 비롯한 여러 곳이 순수수학·형식화 연구자에게 무료·할인 구독과 연구 크레딧을 넓혔고, 다른 주요 정리의 형식화나 린·매스립 개선처럼 더 큰 과학 프로젝트에는 전용 그랜트가 있다고 적었다.

한 가지 더. 앤트로픽은 형식화된 증명이 사람이 읽을 설명을 대체해야 한다고는 보지 않는다고 못박았다. 다만 AI가 쏟아내는 기여를 수학 커뮤니티가 따라잡을 유일하게 실행 가능한 방법일 수는 있다고 적었다. 사람이 읽는 글과 기계가 읽는 코드를 함께 낸다는 뜻이다.

남는 질문 하나

이번 건에서 사람이 한 일은 우선순위 몇 줄을 던진 것, 그리고 결과를 받아 컴파일해서 맞는지 확인한 것이었다. 버자드가 “확인된다”고 쓰지 않았다면 이 발표의 무게는 지금과 달랐을 것이다.

기계가 만든 증명이 늘어날수록 검사도 기계가 한다. 그럼 사람의 자리는 어디로 가나. 버자드의 답은 글 안에 있다. 그는 자동형식화가 “우리를 정직하게 붙들어 둘 것”이라고 적었다. 논문 중에는 “전문가들에게는 알려진” 결과를 슬쩍 가정하고 넘어가는 것들이 있는데, 기계가 그걸 가차 없이 짚어낼 거라는 얘기다. 그는 자기 전공인 랑글랜즈 프로그램의 현재 상태를 두고 품어 온 의심이 정당한지도 기계가 논증을 훑으며 불완전한 대목을 무자비하게 표시하면서 판가름 날 거라고 덧붙였다.

덧붙이면, 이 소식이 세상에 처음 샌 경로도 사람 쪽이었다. 버자드의 기록에 따르면 이즐링턴의 한 커피숍이 인스타그램에 먼저 올렸고, 공식 발표는 그로부터 한 시간 뒤였다.

11일과 1,300만 줄보다 오래 갈 문장은 아마 그쪽이다.