아무도 읽지 않은 증명이 통과했습니다 : 수학에는 검사기가 있고 소프트웨어에는 없습니다

증명을 뜻하는 영어 proof의 뿌리는 라틴어 probare입니다. 시험한다, 검사한다는 뜻인데요. 증명이란 애초에 어떤 결론에 붙는 이름이 아니라, 그 결론을 통과시키는 절차의 이름이었던 셈입니다.

그러면 그 절차는 누가 밟을까요? 수학에서는 오랫동안 답이 하나였습니다. 사람이 읽습니다. 논문이 나오면 동료 수학자들이 몇 달, 길게는 몇 년에 걸쳐 한 줄씩 따라가며 빈틈이 없는지 확인하고, 그 과정을 견뎌야 비로소 정리로 인정받습니다. 페르마의 마지막 정리가 꼭 그랬습니다. 앤드루 와일스가 1993년 케임브리지 강연에서 내놓은 증명에는 실제로 빈틈이 하나 있었습니다. 그 자리를 리처드 테일러와 함께 메우고 나서야, 와일스의 109쪽짜리 본 논문과 두 사람이 함께 쓴 보조 논문이 1995년 같은 학술지에 나란히 실렸습니다. 빈틈을 찾아낸 쪽도 사람이었고요.

그런데 며칠 전, 사람이 한 번도 읽지 않았고 앞으로도 읽지 않을 1,300만 줄짜리 증명이 공개됐습니다.

현지 시각 9월 4일, 앤트로픽이 클로드 에이전트 수십 개를 붙여 페르마의 마지막 정리를 Lean으로 완전히 형식화했다고 발표했습니다. Lean은 수학 명제와 증명을 컴퓨터가 검사할 수 있는 언어로 적어 두는 정리 증명기(theorem prover)인데요. 최종적으로 성공한 실행에 걸린 시간이 11일, 그 사이 생성된 Lean 코드가 1,300만 줄 이상, 증명된 중간 정리가 3만 300개이고 그중 최종 증명에 실제로 쓰인 것이 2만 9,500개입니다. 투입된 에이전트의 정확한 대수는 공개되지 않았고, 쓰인 모델도 상용 제품이 아니라 앤트로픽 사내의 범용 리서치 모델이었습니다. 결과물 전체는 GitHub에 공개돼 있습니다.

먼저 오해를 하나 걷어내야겠습니다. AI가 페르마의 마지막 정리를 증명한 것이 아닙니다. 증명은 앞서 말한 대로 1995년에 끝났습니다. 이번 작업은 그 증명을 기계가 검사할 수 있는 형태로 옮겨 적은 형식화(formalization)이고, 발견보다는 번역에 가깝습니다. 임페리얼칼리지런던 수학과 교수인 케빈 버자드는 자기 블로그에 "수학적으로 이 작업은 우리에게 본질적으로 아무것도 알려주지 않는다"고 적었습니다. 자신은 이미 페르마의 증명이 맞다는 데 99.9% 확신하고 있었다는 것이죠. 그가 이렇게 말할 자격은 충분합니다. 2024년부터 영국 공학·물리과학연구위원회(EPSRC)의 5년 과제를 지원받아, 바로 그 형식화를 사람 손으로 진행해 온 프로젝트의 책임자거든요. 본인 표현으로는 5년에 100만 파운드짜리 과제입니다.

*출처: Wikimedia Commons*

그러면 이 사건에서 남는 것은 무엇일까요? 버자드가 같은 글에 이어 붙인 문장이 정확합니다. 이 작업이 알려주는 것은 자동 형식화 분야에서 무엇이 가능한지이며, 수천 쪽의 문헌을 AI 무리가 11일 만에 끝에서 끝까지 형식화할 수 있다면 앞으로는 최신 연구가 나오는 즉시 형식화되는 광경을 보게 되리라는 것입니다.

▸ 1,300만 줄을 통과시킨 것은 사람이 아니라 작은 커널이었습니다

오십 년 전 케네스 아펠과 볼프강 하켄이 사색정리를 컴퓨터로 증명했을 때 수학계가 갈라진 지점이 여기였습니다. 1,936개의 경우를 기계가 하나씩 검사해 결론을 냈는데, 사람이 손으로 따라갈 수 없는 계산을 증명이라고 부를 수 있느냐는 것이었죠. 그때는 마땅한 답이 없었습니다. 이번에는 규모가 1,300만 줄로 커졌는데, 오히려 답이 준비돼 있습니다.

Lean으로 쓴 증명은 사람이 읽어서 승인하지 않습니다. Lean 커널이 검사합니다. 커널은 이 시스템에서 유일하게 믿어야 하는 부분이고, 그래서 아주 작게 유지됩니다. 논리 규칙 몇 가지를 기계적으로 적용하는 정도의 크기로 묶어 두는 것이 이 설계의 핵심이고요. 그 바깥이 아무리 커져도 최종 판정은 반드시 이 작은 조각을 통과해야만 나옵니다. 이번 산출물이 기대고 있는 공리는 Lean 표준 공리 세 개가 전부였습니다. 이 목록이 중요한 이유가 있는데요. 나중에 채우겠다며 비워 둔 자리가 한 군데라도 있었다면 바로 그 목록에 흔적이 남았을 것이기 때문입니다. 1,300만 줄 전체가 빈칸 없이 커널을 통과했다는 뜻이고요. 그래서 이 발표는 자기 발표인데도 검증 문제가 비교적 가볍습니다. 독립 재현의 상당 부분을 커널과 공개 저장소가 대신하기 때문입니다.

물론 커널이 대답해 준 것의 범위는 정확히 알아 둘 필요가 있습니다. 커널은 이 증명이 이 진술을 함의한다는 데까지만 보장합니다. 그 진술이 우리가 물으려던 바로 그 질문인지는 커널의 소관이 아닙니다. 그래서 앤트로픽은 별도의 대조 도구(comparator)를 돌려, 에이전트가 증명한 진술문이 Mathlib에 정의돼 있는 페르마의 마지막 정리 진술과 일치하는지 대조했습니다. 목표를 슬쩍 더 쉬운 명제로 바꿔치기하지 않았는지 확인한 것이죠. 넘어간 것은 증명을 쓰는 일이고, 넘어가지 않은 것은 무엇을 증명할지 적어 두는 일입니다. 소프트웨어의 형식 검증이 수십 년째 걸려 있는 자리도 정확히 같습니다. 명세가 틀렸으면 그 명세를 완벽히 만족하는 프로그램도 틀립니다.

▸ 첫 시도는 수학이 아니라 기억에서 무너졌습니다

이 프로젝트의 협업 구조를 설계한 사람은 앤트로픽 연구원이자 컬럼비아대 조교수인 톈이 펑입니다. 앤트로픽이 함께 공개한 실패 기록을 보면 초기 실행이 무너진 이유는 정리가 어려워서가 아니었습니다. 프로젝트 전체 상태를 각 에이전트의 컨텍스트 윈도우 안에 두었더니, 시간이 지나면서 무엇이 이미 증명됐는지에 대한 인식이 에이전트마다 갈라졌고 협업이 소음으로 바뀌었습니다.

해법은 더 좋은 모델이 아니었습니다. 프루브투미(Prove2Me)라는 플랫폼을 만들어, 아직 증명되지 않은 진술 전체를 유향 비순환 그래프(DAG)로 유지하고 지금 착수할 수 있는 노드를 표시했습니다. 에이전트는 열린 노드를 하나 집어 증명하고, 결과를 올리면 나머지가 그 위에 쌓습니다. 기능만 놓고 보면 공유 할 일 목록에 가깝습니다. 사내에서 멀티 에이전트를 붙여 보신 분이라면 익숙한 실패일 것입니다. (실은 이 대목을 보고 글을 쓰기로 마음먹었습니다.) 교훈은 한 줄로 정리됩니다. 규모가 커지면 기억은 프롬프트 안이 아니라 프롬프트 바깥의 구조에 있어야 합니다. 결승선을 넘긴 것은 모델 성능이 아니라 이 설계였습니다.

물론 이 11일을 사람의 오 년과 나란히 놓기는 어렵습니다. 앤트로픽은 아무것도 없는 데서 시작하지 않았습니다. 버자드가 이끄는 임페리얼칼리지 프로젝트가 여러 해에 걸쳐 쌓아 둔 Lean 조각들과 쿠머의 정규소수에 대한 기존 형식화를 가져다 확장한 것이고, 이번에 직접 다룬 범위는 17 이상의 소수 지수입니다. 효율이 좋았다고 하기도 어렵습니다. 소모한 출력 토큰이 약 60억이고, 앤트로픽 스스로 이 증명이 필요한 것보다 훨씬 길 가능성이 크다고 인정했습니다. 비용은 공개되지 않았고요.

▸ 남을 숫자는 1,300만이 아니라 리뷰 대기줄입니다

그리고 커널을 통과하는 것과 수학 공동체가 받아들이는 것은 다른 일입니다. Lean의 표준 수학 라이브러리인 Mathlib은 2026년 기준 190만 줄 규모로 알려져 있는데, 이번 산출물은 그 다섯 배가 넘습니다. 이것을 Mathlib에 넣으려면 결국 사람의 리뷰를 거쳐야 하는데요. 버자드가 같은 글에서 세어 본 바로는 Mathlib에 열려 있는 PR이 3,000건이고, 그중 600건 넘게 리뷰 큐에서 움직이고 있습니다. 버자드가 EPSRC에 약속한 나머지 두 가지도 정확히 그쪽 일입니다. Mathlib에 병합하는 것, 그리고 사람이 현대적 증명을 따라가며 탐색할 수 있는 문서를 만드는 것. 그의 연구비가 무의미해진 것이 아니라, 쓰는 쪽이 빨라지면서 읽는 쪽만 병목으로 남은 것입니다.

국내로 눈을 돌리면 대비가 선명해집니다. 지금 국내 모델의 수학 능력은 거의 전부 점수로 표현됩니다. SK텔레콤은 자사 모델 A.X K2가 2026년 국제수학올림피아드 문제에서 42점 만점에 29점을 받아 그해 금메달 기준선에 닿았다고 발표했고, 허깅페이스의 MathArena AIME 2026 리더보드에서는 97.1%로 공동 1위에 올랐습니다. 앞의 채점은 회사가 직접 한 것이고 뒤의 점수는 공개 리더보드가 매긴 것인데요. 어느 쪽이든 점수는 채점자와 정답지가 있어야 성립하고, 채점자를 믿지 못하면 그 점수도 믿을 수 없습니다. 반면 Lean 산출물은 채점자가 필요 없는 형태입니다. 맞으면 통과하고 틀리면 통과하지 못합니다. 국가가 돈을 대는 모델 사업의 평가 항목에 검증 가능한 산출물을 내놓는 능력이 들어 있는지 한 번쯤 물어볼 만합니다.

수학은 오십 년에 걸쳐 커널이라는 답을 마련해 두었고, 이번에 그 답이 1,300만 줄 규모에서도 버틴다는 것을 보여주었습니다. 소프트웨어에는 아직 그런 검사기가 없습니다. 앞으로도 AI가 만들어 낸 산출물을 누가 검토할 것인가라는 질문은 계속 나오겠죠. 그때 사람을 더 붙일지, 아니면 애초에 기계가 검사할 수 있는 형태로 적어 두는 쪽으로 옮겨갈지 고민이 필요합니다.

---

*커버 이미지: 디오판토스 『아리스메티카』 1670년판 여백에 실린 페르마의 주석 — Wikimedia Commons*