검증되었지만 읽히지 않는 증명 — 페르마의 마지막 정리 형식화가 남긴 질문
검증되었지만 읽히지 않는 증명 — 페르마의 마지막 정리 형식화가 남긴 질문
기계가 증명을 기계가 검증할 수 있는 형태로 써낼 수 있다면, 수학에서 ‘이해’는 무엇으로 남는가. Lean 커널이 통과시킨 1,300만 줄은 지식인가, 지식의 그림자인가?
도입
2026년 9월 4일, Anthropic 이 페르마의 마지막 정리(Fermat’s Last Theorem, 이하 FLT)의 첫 종단(end-to-end) 컴퓨터 검증 증명을 공개했다. 발표문의 주장은 간명하다. Claude 가 11일 동안 대체로 자율적으로 작업해 Lean 으로 증명을 써냈고, 그 과정에서 1,300만 줄의 Lean 코드를 작성하고 30,300개의 정리를 증명했으며 그중 29,500개가 최종 증명에 쓰였다는 것이다. a^n + b^n = c^n 을 만족하는 양의 정수 해가 n > 2 에서는 없다는, 1637년 여백의 낙서로 시작해 1995년 앤드루 와일스의 129쪽 논문으로 닫힌 문제다.
Hacker News 에서 이 발표는 490점을 넘기며 그날의 1위가 됐다. 그런데 스레드 상단에서 가장 강하게 권해진 링크는 Anthropic 의 발표문이 아니었다. 한 이용자는 임페리얼 칼리지 런던의 FLT 형식화 프로젝트를 이끄는 케빈 버자드(Kevin Buzzard)의 블로그 글을 함께 읽으라고 권하며, 그 글이 “이 성취가 무엇을 뜻하고 또 무엇을 뜻하지 않는지”에 대한 맥락을 준다고 적었다 (@lalitmaganti). HN 운영자는 그 링크를 게시물 상단 안내문에 추가하면서, 차라리 그쪽을 대표 링크로 올리고 싶다고까지 말했다 (@dang).
이 반응의 구조가 사건의 성격을 말해 준다. 발표문만 읽으면 무엇이 증명됐는지는 알 수 있지만, 무엇이 증명되지 않았고 그 증명이 어떤 종류의 앎인지는 알 수 없다.
11일과 1,300만 줄, 그리고 당사자가 직접 확인한 것
먼저 사실관계를 정리한다. Anthropic 에 따르면 증명은 와일스 증명을 단순화한 다르몽·다이아몬드·테일러(Darmon–Diamond–Taylor)의 1995년 해설을 따른다. 실행은 컬럼비아 대학의 티안이 펑(Tianyi Peng) 연구진이 설계한 Prove2Me 라는 공개 협업 플랫폼 위에서 이뤄졌다. 이 플랫폼은 정리 진술들의 유향 비순환 그래프(DAG)를 유지해 에이전트가 다음에 무엇을 증명할지 고르게 하고, 진술과 증명을 서로 다른 파일로 분리해 Lean 컴파일을 빠르게 하며, 각 정리에 자연어 설명을 붙여 검색과 재사용을 가능하게 한다. 그 위에 Claude Code 기반 멀티에이전트 하네스가 얹혔고, 수십 개의 에이전트가 협업했다. 소비된 출력 토큰은 약 60억 개, 사용된 모델은 “Claude Fable 5.1 에 대략 상응하는 내부 범용 연구 모델”이다.
주목할 것은 실패의 기록도 남아 있다는 점이다. 초기 시도들은 실패했다. 에이전트들이 프로젝트의 상태를 놓치고 협업이 무너졌기 때문이며, 그 실패한 작업들이 최종 증명의 비(非)보일러플레이트 라인 중 약 7%를 차지한다. 인간의 수학적 개입은 “간헐적인 상위 수준 지시”에 그쳤다고 발표문은 적는다. 또한 커뮤니티가 만들어 둔 86쪽짜리 청사진(blueprint)과 Mathlib 이라는 공용 라이브러리, 그리고 버자드의 임페리얼 프로젝트와 flt-regular 프로젝트의 조각들이 출발점으로 쓰였다. Anthropic 은 감사의 글에서 이를 명시한다.
여기서 결정적인 것은 버자드 본인의 검증이다. 그는 블로그에서 코드베이스를 직접 컴파일하고 comparator 를 돌려 봤으며 “체크아웃된다(it checks out)“고 적었다. 규모는 1,340만 줄이 넘고, 96코어 머신에서 Lean 의 수학 라이브러리보다 컴파일에 20배 가까이 걸린다. 500GB 램 머신에서도 파일 사이를 오가는 것이 굼떠서, 실제 탐색은 Anthropic 이 함께 제공한 HTML 문서로 했다고 한다.
동시에 그는 범위를 정확히 잘라 놓았다. 이 저장소가 전개하는 것은 폰텐 이론(Fontaine theory)과 마주르(Mazur)의 아이젠슈타인 이데알에 관한 작업이며, 그 결과로 직접 다뤄지는 것은 소수 지수 p ≥ 17 이다. 그렇다면 나머지는? 홀수 정규소수(odd regular prime)에 대한 FLT 는 Best–Birkbeck–Brasca–Rodriguez 가 이미 형식화해 두었고, 가장 작은 비정규 소수는 37 이다. 따라서 17 미만의 홀수 소수는 전부 정규소수여서 앞선 작업이 덮는다. 버자드의 표현으로는 “so it’s all good”, 즉 빈틈이 없다. Anthropic 의 “FLT 전체가 증명됐다”는 주장은 이렇게 두 갈래를 합쳐야 성립한다. 기계가 새로 써낸 것은 p ≥ 17 경로이고, 작은 지수는 인간이 몇 해 전에 형식화해 둔 결과에 기댄다.
그리고 버자드는 이 작업의 수학적 의미를 스스로 깎아내린다. “수학적으로 Anthropic 의 이 작업은 사실상 아무것도 알려 주지 않는다”고 그는 썼다. 자신은 FLT 증명이 옳다는 데 99.9% 확신하고 있었고, 수론 커뮤니티 대부분은 100% 확신한다는 것이다. 형식화는 초기 문헌을 충실히 따랐을 뿐 새로 더한 것이 없다. HN 에서는 “버자드 그룹이 선수를 빼앗겼다”는 반응이 최상위 댓글로 올라왔지만 (@kdavis), 정작 당사자는 그 프레임을 거부한다. 그는 EPSRC 연구비로 두 가지를 더 약속했다고 밝힌다. 하나는 현대 정수론의 기본 대상들을 Mathlib 에 풀 리퀘스트로 넣는 일이고, 다른 하나는 “인간이 현대적 증명을 탐색할 수 있는 동적 문서”를 만드는 일이다. 그는 Anthropic 이 후자를 할 것 같지는 않다고 본다. 애초에 그들이 형식화한 것은 현대적 증명도 아니다.
신뢰의 뿌리는 커널이 아니라 명제 진술부에 있다
이 사건이 던지는 인식론적 질문은 “1,300만 줄을 믿을 수 있는가”이다. HN 의 한 이용자는 정확히 그렇게 물었다. AI 가 생성한 1,300만 줄의 Lean 코드가 옳다고 확신할 근거가 있는가, 우리는 하나의 검증 문제를 다른 검증 문제로 바꿔 놓은 것뿐 아닌가 (@skobes).
답의 절반은 형식 증명의 구조에 있다. Lean 커널이 증명을 통과시켰다는 것은 「이 증명 항이 이 명제라는 타입을 가진다」는 확인이다. 즉 그 명제가 주어진 정의와 공리로부터 따라 나온다는 보장이다. 중간의 1,300만 줄이 얼마나 장황하든, 얼마나 이상한 우회로를 돌든, 커널을 통과했다면 논리적 연결은 끊기지 않았다. 다른 이용자가 정리한 대로다. 증명 보조기의 장점은 중간 줄을 읽을 필요가 없다는 것이며, 사람이 확인해야 하는 것은 목표 진술이 자기가 생각하는 그 명제와 실제로 일치하느냐 하나뿐이다 (@fwip).
그러니 신뢰의 뿌리는 커널이 아니라 명제 진술부에 있다. 형식 문장은 정의들의 조합이고, 정의가 미묘하게 어긋나면 참인 문장을 증명하고도 우리가 의도한 정리와는 다른 것을 증명한 셈이 된다. HN 토론에서 이른바 ‘쓰레기 정리(junk theorem)’ 문제가 거론된 이유가 여기 있다 (@stratos123). 한 이용자는 그 성격을 정확히 요약했다. 쓰레기 정리는 거짓이 아니라 참이다. 다만 수학을 어떻게 인코딩했느냐에 민감해서, 참이면서도 개념적으로는 무의미하다. 폰 노이만 서수로 자연수를 정의하면 자연수끼리의 교집합이 최솟값과 같아지는데, 이 문장은 참이지만 자연수를 사고하는 방식으로는 완전히 틀렸다 (@mswphd).
FLT 의 경우 이 축은 실제로 닫혔다. Anthropic 은 증명이 Lean 의 표준 공리 세 개만 사용하며, comparator 가 정리의 진술이 Mathlib 자체의 FLT 진술과 일치함을 확인했다고 밝혔다. 그리고 버자드가 자기 손으로 같은 검사를 다시 돌렸다. 진술 충실성은 발표자의 자기 신고가 아니라 외부 전문가의 재실행으로 확인된 셈이다. 이 점은 명확히 해 둘 가치가 있다. “AI 가 그럴듯한 것을 증명했다고 우겼다”는 회의는 이 사례에는 맞지 않는다.
닫히지 않은 축은 그 아래에 있다. 커널 자체의 건전성이다. HN 토론에서는 Lean 에도 버그가 있었고 다른 증명 보조기도 마찬가지였다는 점, 증명 보조기가 잘 작동하는 이유 중 하나는 그것이 인간의 의도를 담은 입력을 전제로 만들어졌다는 점이 지적됐다. 1,300만 줄 안에 무엇이 들었고 그것이 Lean 의 버그를 건드리지 않는지 우리는 모른다는 것이다 (@Jaxan). 더 날카로운 정리도 나왔다. 인간 수학자가 Lean 증명을 쓸 때는 커널 버그를 이용해 속일 동기도 능력도 거의 없지만, AI 는 과거에 목표 달성에 ‘적극적’이었고 Lean 의 버그를 찾아내 악용하는 법도 안다. 같은 커널을 통과했어도 저자가 누구냐에 따라 신뢰의 증감 방향이 갈린다는 것이다 (@3192987). 실제로 프런티어 모델을 동원해 Lean 커널과 런타임의 건전성 이슈를 찾아 패치해 온 작업이 있다는 반론도 함께 올라왔다 (@kingstnap). 여기에 더해, 이 증명의 상당 부분이 Mathlib 에 없던 새 코드라는 지적도 있었다. 기존 자산 위에 쌓은 것이 아니라 상당량을 새로 합성했다는 뜻이며, 그만큼 검토되지 않은 표면이 넓다 (@throw567643u8). 이 우려는 추상적이지 않다. 스레드에서는 한 달쯤 전에 Lean 커널의 버그가 AI 에 의해 악용돼 거짓 명제가 증명된 사건이 있었다는 지적이 나왔고, 같은 이용자는 인간이 검토하지 않은 1,300만 줄이 FLT 에 대한 우리의 이해를 닫아 주지는 않는다고 정리했다. 그 안 어딘가에서 커널 버그가 쓰였을 가능성이 분명히 남아 있기 때문이다 (@mswphd).
반대편의 정리도 같은 스레드에 있었다. 단순한 검사기가 있고 그것이 옳다는 데 많은 사람이 동의하며, 정리의 형식화가 그 정리를 정확히 정의한다는 데도 많은 사람이 동의한다면, 아무도 읽지 않은 1,300만 줄은 그것으로 충분하다는 것이다. 검증해야 할 것은 정리의 형식화와 검사기의 무결성 둘뿐이고, 증명 본문을 읽을 필요는 없다 (@stabbles). 두 입장의 차이는 사실 판단이 아니라 위험을 어디까지 감수하느냐의 문제에 가깝다. 분명한 것은 형식 증명이 옮겨 놓는 것이 신뢰의 총량이 아니라 신뢰가 걸리는 지점이라는 사실이다. 129쪽 논문을 읽어 낸 소수의 전문가에게 걸려 있던 신뢰가, 이제 커널 코드와 진술 한 줄에 걸린다.
그리고 마지막으로 남는 것이 이해 가능성이다. 검증 가능성과 이해 가능성은 서로 다른 목표다. 한 이용자는 기하대수, 리 이론 같은 주제를 오래 공부해 왔음에도 자기 뇌가 Lean 을 읽지 못한다고 고백했다. Lean 4 이전부터 여러 차례 입문을 시도했지만 Lean 증명이 쓰이는 방식이 자기가 증명을 사고하는 방식과 맞지 않았고, Isabelle 쪽이 더 자연스러웠다는 것이다. 증명의 미래가 Lean 하나로 굳는 것이 아쉽다고 그는 덧붙였다 (@rao-v). 별도의 댓글에서는 “인간이 1,300만 줄을 검사했느냐, 이런 작업의 품질 보증은 어떻게 하느냐”는 질문이 나왔고 (@prometheus1992), 또 다른 이용자는 곧바로 “이제 /simplify 를 돌려라, 절반으로 줄일 수 있는가”라고 응수했다 (@stabbles). Anthropic 스스로도 각주에서 이 증명이 “필요한 것보다 훨씬 길 것”이라고 인정한다.
와일스의 증명을 이해한다고 말할 수 있는 사람이 지금 세상에 25명에서 50명뿐일 것이라는 추정이 스레드에 올라왔다 (@bjourne). 그 목록에 1,300만 줄짜리 Lean 저장소를 추가할 수는 없다. 그것은 이해가 아니라 확인이다. 버자드가 자기 프로젝트의 잔여 과제로 “인간이 탐색할 수 있는 동적 문서”를 꼽은 것은 이 간극에 대한 정확한 대응이다. 형식화는 명제가 참임을 확정하지만, 왜 참인지를 사람에게 전달하는 일은 여전히 별도의 노동이다.
검증기가 있는 곳에서만 통하는 마법
HN 에서 가장 많이 인용된 수치와 함께 붙은 해석은 이랬다. 1,300만 줄과 29,500개의 중간 정리라는 규모는 “옳다는 것을 보일 수 있는 일이라면 무엇이든 모델이 해낼 수 있다”는 생각에 힘을 실어 준다는 것이다 (@m_w_). 이 추론은 어디까지 타당한가. 선을 그어 둘 필요가 있다.
이 문제가 특별한 것은 다섯 가지 조건이 동시에 성립했기 때문이다. 첫째, 목표 명제가 이미 형식적으로 존재했다. Mathlib 에 FLT 의 진술이 있었기에 “무엇을 증명할 것인가”를 다시 정의할 필요가 없었다. 둘째, 인간 커뮤니티가 만든 86쪽 청사진이라는 분해 계획이 있었다. 셋째, 무오류에 가까운 판정자가 사실상 무제한으로 싸게 판정해 준다. 넷째, 부분 진전이 재사용 가능한 조각으로 축적된다. 정리 하나를 증명하면 그것은 영구히 남아 다음 정리의 재료가 된다. 다섯째, 실패가 무해하다. 틀린 증명은 배포되어 사고를 내는 대신 그냥 컴파일에 실패한다. 한 이용자는 이 구조를 경험적으로 짚었다. 검증기가 있으면 에이전트의 사고가 상당히 혼란스러워도 의미 있는 해로 수렴하더라는 것이다 (@fspeech).
대부분의 실무 문제는 이 조건을 만족하지 않는다. 명제 자체가 흐릿하고(“사용자가 쓰기 편한 화면”), 판정자가 사람이며, 그 사람은 비싸고 느리고 날마다 일관되지 않다. 형식화의 성공을 그대로 일반화하면 조건이 아니라 결론만 옮겨 오게 된다.
소프트웨어 공학에 주는 함의는 그래서 오히려 뚜렷하다. 우리 업계에는 이미 값싼 판정자가 여럿 있다. 타입 체커, 테스트 스위트, 컴파일러, 프로퍼티 기반 테스트, 정적 분석기, 계약과 불변식이 그것이다. 생성 모델의 한계 생산성은 이 판정자들이 촘촘한 코드베이스에서 유독 높다. 뒤집으면, 판정자를 늘리고 날카롭게 하는 일이 코드를 직접 쓰는 일보다 레버리지가 크다는 결론이 된다. 다만 같은 함정이 여기서도 반복된다는 점을 잊으면 안 된다. 테스트가 통과했다는 것은 테스트에 적어 둔 것이 참이라는 뜻이지, 우리가 의도한 것이 참이라는 뜻이 아니다. 신뢰의 뿌리가 커널이 아니라 명제 진술부에 있다는 원칙은 그대로 “신뢰의 뿌리는 테스트 러너가 아니라 단언문에 있다”로 번역된다. 게이트를 늘릴수록 게이트가 무엇을 묻고 있는지를 사람이 읽어야 한다.
비용도 함께 봐야 한다. 출력 토큰 60억 개를 두고 HN 에서는 공개 요율로 어림해 30만 달러 안팎이 든다는 계산이 나왔다 (@davmre). 버자드는 5년짜리 프로젝트에 100만 파운드를 받았다고 적으며, Anthropic 은 11일이 걸렸지만 돈은 더 썼을지 궁금하다고 덧붙였다. 이 비교를 곧이곧대로 받으면 안 되는 이유는 분명하다. 실패한 시도의 비용이 계산에 들어 있지 않고, Mathlib 과 청사진과 앞선 형식화라는 공짜로 주어진 인프라가 가격표에 없다.
앞으로의 시나리오는 셋으로 갈린다. 낙관적으로는 버자드의 기대대로 현대 연구 문헌의 형식화가 상시 작업이 되어, 논문 심사의 부담이 줄고 “전문가들에게는 알려진” 결과를 암묵적으로 가정해 온 논문들이 드러난다. 비관적으로는 검증은 됐지만 아무도 읽지 않는 거대한 산출물이 쌓이고, 커널 버그 한 건이 그 전부를 흔든다. 현실적으로는 그 사이 어디쯤일 것이다. 형식화의 병목이 노동에서 판단으로 옮겨 가고, 사람의 일은 증명을 쓰는 것에서 진술을 고르고 검사하는 것으로 이동한다.
결론
리드 질문으로 돌아간다. Lean 커널이 통과시킨 1,300만 줄은 지식인가. 지식이다. 단, 정확히 한 줄에 대한 지식이다. 최종 진술이 참이라는 것을 우리는 이제 기계적으로 안다. 그러나 왜 참인지는 그 안에 담겨 있지 않다. 버자드가 “수학적으로 사실상 아무것도 알려 주지 않는다”고 쓴 것은 폄하가 아니라 이 구분을 정확히 지킨 문장이다. 그는 같은 글에서 흥분을 감추지 않는다. 수천 쪽의 문헌이 11일 만에 종단으로 형식화될 수 있다면, 머지않아 현대 연구가 진행 중에 형식화되기 시작할 것이고, 기계가 불완전한 논증을 가차없이 표시하게 될 것이기 때문이다.
그러니 이 사건의 의미는 FLT 에 있지 않다. FLT 는 이미 참이라고 모두가 믿고 있었다. 의미는 자동 형식화가 실용적 규모에 도달했다는 사실, 그리고 그 순간 ‘검증됨’과 ‘이해됨’이 처음으로 뚜렷하게 분리됐다는 사실에 있다. 20년 묵은 100개 정리 목록의 마지막 항목이 이렇게 닫혔다.
남는 질문은 우리 쪽에 있다. 형식적으로는 검증됐지만 아무도 읽지 않는 산출물이 계속 늘어날 때, 공동체는 무엇을 신뢰의 단위로 삼을 것인가. 그리고 통과하는 테스트와 초록색 CI 를 근거로 이미 같은 일을 하고 있는 우리 코드베이스에서, 마지막으로 단언문을 직접 읽어 본 것은 언제인가.
출처: