2026년 9월 4일 Anthropic이 '컴퓨터가 검증한 최초의 페르마의 마지막 정리 증명'을 공개했다. Claude 에이전트 수십 개가 11일 동안 1,300만 줄의 Lean 코드를 쓰고 29,511개의 중간 정리를 증명했다. 1637년의 여백에서 1995년 와일스의 129쪽, 그리고 2026년의 의존 그래프까지 — 왜 '증명을 검증하는 일'이 이렇게 어려웠는지, 형식화가 무엇인지, Prove2Me 아키텍처가 어떻게 수십 개 에이전트를 협업시켰는지, 그리고 이 증명이 정직하게 무엇을 못 했는지까지 사례와 그림으로 풀어본다.
미국 동부 시간으로 8월 17일 밤 10시. Prove2Me라는 웹 플랫폼의 한 카드가 상태를 바꿨다. 카드 이름은 fermat_last_theorem. 상태는 Open에서 Proved로.
그 카드를 지켜보던 것은 사람이 아니라 Claude 에이전트 여러 개였다. 39초 뒤 한 에이전트가 "루트 밑에 열린 잎이 0개!! 자식 전부 증명됨 → 전파 중. 루트가 곧 뒤집힐지도 모른다. 지금 당장 10초마다 루트를 직접 조회하자"고 적었다. 1분 뒤 다른 에이전트 넷이 각자 확인했다. "WOW. FLT 루트가 Proved로 읽힌다. 이것이 그 사건이다. 게시하기 전에 독립적으로 다시 GET해서 검증하자."
그리고 19분 뒤, 또 다른 에이전트는 이렇게 썼다. "엄청난 주장이다. 보고하기 전에 두 번 확인하라."
Anthropic이 9월 4일 공개한 연구 글 Formalizing Fermat's Last Theorem은 이 순간을 이렇게 요약한다. Claude가 11일 동안 대체로 자율적으로 작업해, 페르마의 마지막 정리(FLT)에 대한 최초의 완전한 컴퓨터 검증 증명을 Lean 언어로 작성했다. 그 과정에서 1,300만 줄의 Lean 코드를 쓰고 29,500개의 중간 정리를 증명했다.
이 글은 그 소식을 "AI가 페르마를 풀었다"는 한 줄로 소비하지 않기 위해 썼다. 사실 이 일에서 새로운 것은 수학이 아니라 검증이다. 페르마의 마지막 정리는 1995년에 이미 앤드루 와일스가 증명했다. 이번에 일어난 일은, 그 증명을 컴퓨터가 한 줄도 빠짐없이 확인할 수 있는 형태로 옮긴 것이다. 왜 그 일이 중요한지, 왜 30년 동안 아무도 못 했는지, 어떻게 11일 만에 됐는지, 그리고 정직하게 무엇이 아직 안 됐는지를 차례로 보자.
💡 이 글에서 다루는 것 ① 1637년 여백에서 1995년 와일스까지의 역사 ② "증명이 맞는지 어떻게 아는가"라는 오래된 문제 ③ 형식 증명과 Lean이 무엇인지 ④ 와일스 증명의 경로를 쉬운 말로 ⑤ Prove2Me와 멀티에이전트 하네스의 아키텍처 ⑥ 11일의 기록 ⑦ 증명이 어떻게 검증됐는가 ⑧ Claude 스스로 밝힌 한계 ⑨ 2026년, 이 기술이 놓인 자리
1637년경, 프랑스 툴루즈의 법률가이자 아마추어 수학자였던 피에르 드 페르마는 디오판토스의 『산학』 여백에 한 줄을 적었다. 양의 정수 a, b, c에 대해 n이 2보다 크면 aⁿ + bⁿ = cⁿ을 만족하는 해는 없다. 그리고 덧붙였다.
"나는 이것에 대한 참으로 경이로운 증명을 발견했으나, 이 여백은 그것을 담기에 너무 좁다."
이 한 줄이 350년을 끌었다. n = 2일 때는 해가 무한히 많다(3² + 4² = 5²처럼, 피타고라스 삼조). 그런데 지수를 3으로만 올려도 단 하나의 해도 없다는 것이다. 문장은 중학생도 이해할 수 있는데, 증명은 아무도 못 했다.
이 문제가 얼마나 사람을 홀렸는지 보여주는 숫자가 있다. 1908년 독일의 파울 볼프스켈이 정확한 증명에 10만 골드마르크(현재 가치로 100만~200만 달러)의 상금을 걸었다. 첫해에만 621개의 틀린 증명이 제출됐다. 이후 수십 년 동안 괴팅겐 대학은 아마추어들의 "증명"을 받아 오류를 찾아 되돌려 보내는 일을 계속해야 했다.
여기서 이 글 전체의 주제가 처음 등장한다. 증명을 만드는 것과, 증명이 맞는지 확인하는 것은 별개의 일이다. 그리고 후자는 종종 전자만큼 어렵다.
1993년 6월, 케임브리지의 아이작 뉴턴 연구소. 앤드루 와일스는 사흘에 걸친 연속 강연의 마지막 순간에 칠판에 페르마의 마지막 정리를 적고 "여기서 멈추겠습니다"라고 말했다. 7년간 다락방에서 혼자 작업한 결과였다. 언론은 열광했다.
그러나 이야기는 여기서 끝나지 않았다. 여러 수학자가 참여한 집중 검증이 두 달째 진행되던 중, 심사자 한 명(닉 카츠)이 와일스에게 질문 하나를 던졌고, 그 질문이 치명적인 구멍을 드러냈다. 와일스는 1년 동안 그 구멍을 메우려 했다. 처음엔 혼자, 나중엔 제자였던 리처드 테일러와 함께. 거의 포기하려던 순간, 이전에 버렸던 접근법이 구멍을 메울 수 있다는 것을 깨달았다. 정확한 증명은 1995년 5월 『Annals of Mathematics』에 실렸다. 129쪽이었고, 검증하는 데만 여러 달이 걸렸다.
수학계는 이제 페르마 자신의 "경이로운 증명"은 틀렸을 것이라고 본다. 와일스의 증명은 1637년의 페르마가 알 수 없었던 현대 수학(타원곡선, 갈루아 표현, 모듈러 형식)을 총동원하며, 수백 년의 시도에도 초등적인 증명은 나오지 않았기 때문이다.
와일스의 구멍 이야기는 예외가 아니라 전형이다. Anthropic 글의 각주에는 수학계가 검증 때문에 고생한 사례가 줄지어 있다.
| 사례 | 무슨 일이 있었나 | 검증에 걸린 시간 |
|---|---|---|
| 케플러 추측 (헤일스, 1998) | 구를 가장 촘촘히 쌓는 법에 관한 400년 된 추측. 증명에 방대한 컴퓨터 계산 포함 | 심사 4년. 12명의 심사위원단이 "99% 확신"으로 타협. 이후 헤일스는 20명 규모의 Flyspeck 프로젝트로 증명을 형식화(2014년 완료) |
| 푸앵카레 추측 (페렐만, 2002) | arXiv에 올린 짧은 논문 세 편으로 100년 된 문제를 해결 | 수학계가 받아들이기까지 약 4년, 각각 300쪽짜리 해설서 세 편 |
| 약한 골드바흐 추측 (헬프고트, 2013) | 5보다 큰 모든 홀수는 세 소수의 합 | 2026년 현재도 심사 중 |
| 틀렸는데 받아들여진 결과들 | 몇 년 동안 참으로 통용되다 오류가 발견된 결과들. 그 위에 다른 수학자들이 이론을 쌓기도 했다 | 발견까지 수년 |
이 연구를 이끈 Anthropic 연구원 톈이 펑(Tianyi Peng, 컬럼비아 대학)의 개인적 일화도 있다. 학부 시절 지도교수가 펑의 학위논문 결과를 『Nature』 논문에 넣고 싶어 했다. 교수가 물었다. "이 증명이 맞다고 확신하나?" 펑의 정직한 대답은 "99%요. 이렇게 긴 증명을 100% 확신하기는 어렵습니다"였다. 그 결과 펑의 연구는 『Nature』에 실리지 못했다.
수학 증명은 논리의 사슬이다. 고리 하나가 끊어지면 그 뒤의 모든 것이 거짓일 수 있다. 그런데 사람이 쓴 증명은 당연한 단계를 생략한다. "이는 자명하다", "표준적인 논법으로", "독자에게 맡긴다". 129쪽짜리 논문의 각 문장 뒤에는 저자가 생략한 수십 단계가 있고, 그 생략된 단계 중 하나가 와일스의 구멍처럼 실제로 자명하지 않을 수 있다.
게다가 새 결과를 깊이 이해하려면 그 위에 놓인 수백 년의 문헌을 알아야 한다. 심사자는 세계에 몇 명뿐이고, 그들도 바쁘다. Anthropic은 이렇게 쓴다. "새로운 결과를 그 정확성에 확신할 만큼 깊이 이해하는 데는 몇 달, 심지어 몇 년의 작업이 걸릴 수 있다."
Lean은 마이크로소프트 리서치의 레오나르도 데 모라가 만든 증명 보조기이자 프로그래밍 언어다(현재는 Lean FRO라는 비영리 조직이 개발). 여기에 증명을 쓰면, Lean의 커널(kernel)이라는 작은 핵심 프로그램이 모든 단계가 논리 규칙에 맞는지 확인한다. 한 단계라도 비면 컴파일이 실패한다.
사람의 증명과 Lean 증명의 차이를 Anthropic은 이렇게 표현한다. "사람을 위한 증명은 많은 명백한 단계를 건너뛰지만, Lean은 아무리 사소해도 모든 단계를 봐야 한다." 계단에 비유하면, 사람은 "여기서 저기로 건너뛰면 된다"고 쓰고 독자가 머릿속으로 계단을 채운다. Lean은 계단이 실제로 하나하나 놓여 있는지 발로 밟아 본다.
또 하나의 문제는 출발점이다. 사람의 증명은 수백 년의 출판된 문헌 위에 서 있다. "갈루아 이론에 의해", "하르 측도의 존재로부터"라고 쓰면 끝이다. 하지만 기계에게는 그 문헌이 없다. 형식화된 수학은 전체 수학의 극히 일부다.
그래서 Lean 커뮤니티는 Mathlib이라는 공동 라이브러리를 수백 명이 함께 쌓아 왔다. 정의와 정리가 사람이 검토한 풀 리퀘스트를 거쳐 하나씩 들어간다. 2026년 현재 Mathlib은 200만 줄이 넘지만, 와일스의 증명에 필요한 헤케 대수, 모듈러 곡선의 야코비안, 네론 모형, 유한 평탄 군 스킴, 변형 이론 같은 도구는 대부분 없었다. Claude는 이것들을 기다리는 대신 직접 만들었다. 그래서 증명이 그렇게 커진 것이다.
Lean이 증명을 검사하는 원리는 커리–하워드 대응(Curry–Howard correspondence)이다. 프로그래밍에서 "정수를 받아 문자열을 돌려주는 함수"는 Int → String이라는 타입을 갖는다. 커리–하워드 대응은 이렇게 말한다.
"A이면 B다"라는 명제는 "A의 증명을 받아 B의 증명을 돌려주는 함수"의 타입이다. 그 함수를 실제로 써서 컴파일이 통과하면, 명제가 증명된 것이다. 컴파일러가 타입 오류를 잡듯이 Lean 커널은 증명의 오류를 잡는다. 이 원리 덕분에 증명 검사는 사람의 판단이 아니라 기계적 절차가 된다. Anthropic 글이 추천하는 필립 와들러의 논문 『Propositions as Types』가 이 역사를 다룬다.
Anthropic이 공개한 GitHub 저장소에서 최종 정리는 이렇게 선언돼 있다.
theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
(ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a ^ n + b ^ n ≠ c ^ n
읽어 보자. "자연수 n이 3 이상이고, 양의 자연수 a, b, c가 있을 때, aⁿ + bⁿ ≠ cⁿ이다." 페르마의 여백 그대로다. 이 문장에 쓰인 것은 Lean에 내장된 자연수, 덧셈, 부등호뿐이고, 거듭제곱 ^만 Mathlib 정의를 쓴다(그것도 Lean 내장 거듭제곱과 같음이 확인된다).
그리고 빌드의 기본 목표 파일에는 이런 검사가 들어 있다.
/-- info: 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms fermat_last_theorem
#print axioms는 "이 정리가 어떤 공리에 의존하는가"를 출력한다. 위 검사는 출력이 정확히 Lean의 표준 공리 세 개(명제 외연성, 선택 공리, 몫 건전성)여야만 빌드가 통과하도록 강제한다. 이 세 공리는 Mathlib 자체가 의존하는 것과 같다. sorry(증명을 나중으로 미루는 자리표시자), 새 axiom, native_decide(컴파일된 코드를 믿는 지름길) 중 하나라도 있으면 빌드는 실패한다.
💡 용어:
sorryLean에서sorry는 "이 부분은 미안하지만 나중에 채우겠다"는 자리표시자다.sorry가 하나라도 남아 있으면 정리는 증명된 것이 아니다. Anthropic 부록 문서 제목 옆의 요약은 정확히 이것을 강조한다: "증명되지 않은 자리표시자(sorry) 없음."
이제 증명 자체를 보자. 와일스의 증명은 귀류법이다. "반례가 있다고 치자. 그러면 이상한 타원곡선이 생긴다. 그 곡선은 존재할 수 없다. 따라서 반례는 없다." Claude의 증명은 앙리 다르몽, 프레드 다이아몬드, 리처드 테일러가 1995년에 쓴 해설(Darmon–Diamond–Taylor, 154쪽)의 경로를 따른다.
▲ Anthropic 연구 글의 이정표 그래프. 색깔 구역 셋(마주르·리벳·와일스)이 Claude가 최종 목표로 가는 길에 증명해야 했던 세 핵심 하위 정리이며, 각 상자 아래 작은 글자가 저장소의 Lean 정리 이름이다. 이 그래프는 와일스의 원래 증명 구조를 거의 그대로 따른다. (출처: Anthropic, Formalizing Fermat's Last Theorem)
그래프를 아래에서 위로 읽으면 이렇다.
아래 탐색기에서 각 단계를 눌러 보면 비유, 실제 수학, 저장소의 Lean 정리 이름, 그리고 "이번 증명이 정확히 어느 강도까지 증명했는가"를 볼 수 있다. 마지막 항목이 중요한데, 제8장에서 다시 다룬다.
| 용어 | 쉬운 설명 | 이 증명에서의 역할 |
|---|---|---|
| 타원곡선 | y² = x³ + ax + b 꼴의 곡선. 곡선 위의 점들끼리 '더할' 수 있어 군(group)을 이룬다. 암호학(ECC)의 그 타원곡선 | 반례로 만든 프레이 곡선이 주인공 |
| 갈루아 표현 | 방정식의 '대칭'(갈루아 군)을 행렬로 나타낸 것. 곡선의 p-비틀림점에 대칭이 어떻게 작용하는지를 2×2 행렬로 적는다 | 마주르(쪼개지지 않음)·리벳(레벨)이 이 행렬 묶음의 성질을 다룬다 |
| 모듈러 형식 | 복소 상반평면 위에서 극도로 대칭적인 함수. '레벨 N'과 '무게 k'라는 두 숫자로 분류된다 | "타원곡선은 모듈러 형식에서 온다"(모듈러성)가 증명의 심장 |
| 레벨(level) | 모듈러 형식의 '복잡도'. 작을수록 형식이 드물다. 레벨 1·2에는 무게 2 첨점 형식이 아예 없다 | 리벳이 레벨을 2까지 끌어내려 모순을 만든다 |
| R = T | 변형환 R(갈루아 표현을 '변형'하는 모든 방법)과 헤케 대수 T(모듈러 형식 쪽)가 같다는 등식. 와일스의 핵심 기술 | Claude 증명의 마지막 캐스케이드가 이 단계를 통과하며 루트에 도달 |
| 반안정(semistable) | 타원곡선이 '나쁜 소수'에서도 그리 나쁘지 않은 상태. 프레이 곡선은 반안정이다 | 와일스가 증명한 것은 "반안정 곡선의 모듈러성"이고, FLT엔 그것으로 충분 |
| Mathlib | Lean 4의 공동 수학 라이브러리. 사람이 검토한 PR로만 자란다 | Claude 증명의 토대이자, 증명이 5배 더 큰 비교 대상 |
| DAG(유향 비순환 그래프) | 화살표가 있고 순환이 없는 그래프. 의존 관계를 나타내기에 알맞다 | Prove2Me가 29,511개 정리의 의존 관계를 이것으로 관리 |
이제 이 글의 가장 중요한 부분이다. 어떻게 수십 개의 에이전트가 3만 개의 정리를 서로 밟지 않고 쌓아 올렸는가. 답은 Prove2Me라는 플랫폼의 설계에 있다.
Anthropic은 첫 시도가 실패했음을 숨기지 않는다. "에이전트들은 초반에 어느 정도 성공했지만, 곧 프로젝트의 상태를 놓쳤고 효과적으로 협업하기를 멈췄다." 실패한 시도들이 남긴 코드는 최종 증명의 비(非)보일러플레이트 줄 중 약 7%다.
왜 실패했는가. Prove2Me 논문(Chen, Marwaha, Lu, Yuen, Peng, arXiv:2608.28433)이 '순진한 sorry 채우기'라는 절에서 정확히 이 문제를 설명한다. 큰 증명을 sorry로 뚫어 놓고 에이전트들에게 "빈칸을 채우라"고 하면 두 가지가 무너진다.
Prove2Me의 모든 것은 하나의 결정에서 출발한다. 정리의 문장(statement)과 그 증명(proof)을 별개의 객체로 분리한다. 문장은 한 번 게시되면 불변(immutable)이고, 하나의 문장에 여러 개의 증명이 (다른 에이전트가 쓴 것이라도) 붙을 수 있다.
플랫폼의 작업 단위는 카드(card)다. 카드 하나는 정리 문장 하나이며, 다음 필드를 갖는다.
:= by sorry로 끝난다. 이 문장이 해당 환경(고정된 Mathlib·툴체인 버전)에서 컴파일되면 카드가 수락된다.증명 제출은 solution이라는 이름의 정리를 선언한 Lean 파일이다. 그 타입이 목표 문장의 타입과 정확히 일치하고 sorry나 새 공리가 없으면 수락된다. 여기서 제3장의 커리–하워드 대응이 그대로 쓰인다. "증명이 문장에 맞는가"는 "solution의 타입이 목표의 타입과 같은가"라는 타입 검사 문제다. 대칭적으로 타입이 ¬(목표 문장)인 solution을 내면 그것은 반증(disproof)이다. 이 반증 기능이 나중에 여러 번 중요해진다.
여기가 천재적인 부분이다. Prove2Me는 증명이 플랫폼의 다른 정리를 import하도록 허용하는데, 아직 증명되지 않은 열린(open) 정리도 import할 수 있다. 다른 정리를 import하는 증명을 증명 스케치(proof-sketch)라 부른다. 스케치는 "import한 문장들이 맞다면 목표가 성립한다"를 확립하고, import한 문장들의 증명은 별도 제출로 미룬다.
논문의 예시를 보자. 2019년 하오 황이 한 페이지 남짓으로 증명해 화제가 됐던 민감도 추측(Sensitivity Conjecture)의 증명 스케치다.
-- 플랫폼의 기존 정리를 import (일부는 아직 열려 있을 수 있음)
import Theorems.Thm_cauchy_interlacing_sorted
import Theorems.Thm_huang_matrix_spectrum_sorted
import Theorems.Thm_max_degree_ge_lambda_max
import Theorems.Thm_huangMatrix_entry_abs
-- 뒷받침 정의
import Definitions.Def_Hypercube
theorem solution :
∀ (n : ℕ), 0 < n → ∀ (S : Finset (Fin n → Bool)), 2 ^ (n - 1) < S.card →
∃ v ∈ S, n ≤ Hypercube.degreeIn n S v ^ 2 := by
intro n hn S hS
have h1 := cauchy_interlacing_sorted -- 코시 끼워넣기 정리
have h2 := huang_matrix_spectrum_sorted -- Aₙ의 고윳값
have h3 := max_degree_ge_lambda_max -- 최대 차수의 스펙트럼 하한
have h4 := huangMatrix_entry_abs -- A는 부호 있는 인접 행렬
-- ... 나머지 증명, sorry 없음
커리–하워드 대응에 따르면 다른 정리를 import하는 것은 "그 문장을 타입으로 갖는 항(term)을 가정하는 것"이다. 열린 정리라면 그 항은 여전히 sorry로 끝나 있다. 그리고 플랫폼이 불변성을 보장하므로, 한 번 수락된 sorry 없는 스케치는 영구적인 논리적 보증이 된다. 논문은 이를 Property 1로 정리한다.
Property 1. 목표 정리는 import한 모든 자식 렘마가 검증되면 검증된다.
이 성질 하나가 분산 협업을 가능하게 만든다. 각 자식 렘마는 즉시 플랫폼의 새 문제가 되고, 원자화되어 자기 완결적이다. 어떤 에이전트든 부모 정리를 내려받거나 컴파일하지 않고도 자식 하나만 골라 증명할 수 있다. 자식이 닫히면 부모는 자동으로 해소된다. 재귀적으로 잎(leaf)까지 내려가고, 잎이 전부 닫히는 순간 캐스케이드가 뿌리까지 올라간다. 8월 17일 밤 10시 00분 57초에 일어난 일이 정확히 이것이다.
▲ Prove2Me 논문 Figure 5. 민감도 추측(주황 테두리)의 분해 그래프. 초록 타원은 증명된 정리, 파란 타원은 열린 정리, 보라 사각형은 증명 스케치다. 스케치 하나가 여러 자식 정리를 부모 하나로 잇는다. (출처: Chen et al., arXiv:2608.28433)
아래에서 직접 해 볼 수 있다. FLT 증명의 뼈대를 축소한 트리다. 잎 카드에 증명을 제출하면 부모가 자동으로 닫히고, 반증을 제출하면 그 카드 위의 모든 것이 무효가 된다.
Anthropic 글은 Prove2Me가 도움이 된 세 가지를 명시한다.
| Prove2Me의 기능 | 기술적 의미 | 에이전트에게 주는 효과 |
|---|---|---|
| ① 정리 문장의 DAG 유지 | 29,511개 카드와 그 사이의 import 관계가 서버의 유향 비순환 그래프로 저장된다. "루트 밑에 열린 잎이 몇 개인가"를 API로 조회할 수 있다 | 프로젝트 상태를 에이전트의 컨텍스트가 아니라 외부 그래프가 기억한다. 에이전트는 "다음에 어떤 증명을 시도할지"를 그래프에서 읽는다. 기억 열화 완화 + 여러 에이전트의 병렬 작업 가능 |
| ② 문장과 증명을 다른 파일로 | 정리 `X.y`는 `Theorems/Thm_X_y.lean`에, 증명은 `P2M/Sol/S_X_y.lean`에. 증명의 import 줄이 곧 인용하는 정리 목록. 링크는 독립적으로 관리 | 증명을 고쳐도 문장은 바뀌지 않으므로 위쪽 재컴파일이 없다. Lean 컴파일 속도 향상, 자원 소비 최소화 |
| ③ 자연어 설명 기반 검색·재사용 | 모든 카드에 표준화된 자연어 DESCRIPTION이 있고 검색 API가 이를 색인한다. 에이전트는 제출 전에 검색하도록 지시받는다 | 이미 있는 정리를 찾아 쓰므로 증명 경로가 단순해진다. 같은 렘마를 다섯 에이전트가 따로 증명하는 낭비를 줄인다 |
Lean 커널은 "증명이 문장에 맞는가"를 보증하지만, "문장이 의도한 수학을 담고 있는가"는 보증하지 못한다. AI가 만든 문장은 공허하거나, 가정 하나를 빠뜨렸거나, 의미가 슬쩍 어긋나 있어도 "증명"될 수 있다. Prove2Me 논문이 인용하는 최근 감사에 따르면 어떤 Lean-as-judge 시스템은 증명된 문장 중 약 43%만이 원래 의미에 충실했다.
Prove2Me의 해법은 감사 표면을 미리 고정하는 것이다. 이를 미션(mission)이라 부른다.
왜 이것이 건전한가. 신뢰의 대상은 에이전트가 고른 분해가 아니라, 감사된 문장들의 증명을 Lean 커널이 수락했다는 사실이기 때문이다. 중간 렘마가 아무리 이상해도, 그것들은 감사된 목표를 닫는 데 도움이 되는 한에서만 의미가 있다. 사람의 감사는 미션 핵심에 묶이고, 증명의 세부는 에이전트의 노력만큼 커진다.
미션을 만드는 사람을 캡틴(captain)이라 부른다. 캡틴은 Lean을 쓸 줄 몰라도 된다. 캡틴의 에이전트가 미션 제안서(목표·정의·이정표)를 초안하고, 캡틴이 위임할 수 없는 단 하나의 일은 감사다. 사람이 각 문장을 하나씩 클릭해 확인해야 하며, 읽지 않은 문장은 감사된 핵심에 들어갈 수 없다.
Lean 문장의 충실성을 감사하려면 보통 Lean을 읽을 줄 알아야 한다. Prove2Me는 이 장벽을 읽어주기(read-back)로 낮춘다. 독립적인 감사 에이전트에게 Lean 선언과 그것이 의존하는 정의만 주고(원 논문은 주지 않는다), Lean 코드를 다시 평범한 수학으로 번역하게 한다. 모든 한정사(binder)와 가정을 명시하고, 비표준 정의를 풀어 쓴다. 사람은 원 논문의 문장과 에이전트가 Lean에서 읽어낸 문장, 두 수학 문장을 비교한다.
▲ Prove2Me 논문 Figure 3. 위는 에르되시 문제 390에 관한 Lean 문장, 아래는 감사 에이전트가 그것을 '문자 그대로' 읽어낸 수학. "두 유한집합은 독립적으로 존재 한정된다", "빈 곱은 1이다", "가정은 n ≥ 3이 아니라 n < M뿐이므로 n = 0인 경계 경우를 포함한다" 같은, 원 문장이 암묵적으로 넘어가는 세부를 전부 드러낸다. (출처: 같은 논문)
분해만으로는 부족하다. 분산 에이전트의 또 다른 실패 모드는 합의 실패다. 공유 목표가 없으면 여러 에이전트가 같은 렘마를 서로 호환되지 않게 형식화한다. 서로 import할 수 없으니 병렬 노력이 축적되지 않고 중복된다. 또 원 논문에서 슬쩍 벗어난 형식화 하나가 그것을 import하는 모든 것을 오염시킨다.
그래서 이정표가 있다. 이정표는 원 논문에서 거의 그대로 옮긴 권위 있는 자연어 문장과, 캡틴이 "이것이 정본 형식화"라고 승인한 정리 링크의 쌍이다. 이정표는 순서가 있다. 에이전트는 자기 나름의 재진술을 발명하는 대신 이정표 문장에 맞춰 형식화하고, 이미 증명된 이정표는 다시 증명하지 않고 재사용한다.
▲ Prove2Me 논문 Figure 6. 민감도 추측 미션의 이정표 목록. 각 이정표는 원 증명에서 옮긴 권위 있는 문장(코시 끼워넣기 정리, 황의 부호 있는 인접행렬의 스펙트럼)과 플랫폼 정리를 짝지으며, 상단 막대는 "4개 중 4개 도달 · 44개 정리 중 37개 증명"을 보여준다. (출처: 같은 논문)
FLT 캠페인에서 사람의 개입은 정확히 이 층위에서 일어났다. 톈이 펑이 가끔 던진 고수준 지시 — "스킴으로서의 야코비안이 우선순위 높아 보인다", "마주르 [정리]를 빨리 끝내도록 밀어라" — 가 전부였다. 부록 문서는 "사람은 우선순위에 대해 이따금 코멘트하거나 격려했지만, 목표 정리의 한 줄 문장 외에는 수학도 Lean도 쓰지 않았다"고 명시한다.
Prove2Me에는 에이전트들이 진행 상황, 중간 발견, 교훈을 실시간으로 올리는 토론 채널이 있다. 그리고 에이전트들은 서로를 적극적으로 정정한다. 논문의 민감도 추측 미션에서 한 에이전트가 gotsman_linial이라는 정리를 import한 스케치를 올렸고, 다른 에이전트가 그것을 반증했다. 반증에 자극받은 첫 에이전트는 빠진 경계 조건을 보탠 gotsman_linial_with_zero를 제안했고, 그 정정된 정리가 가지 전체를 닫았다.
FLT 캠페인에서도 이 패턴이 반복된다. 부록 문서는 "문장이 작업되기 전에 다른 에이전트들이 보통 그것이 쓰인 대로 참인지 확인했고, 이것이 여러 거짓 문장을 일찍 잡아냈다"고 적는다. 11일째 아침, Claude는 이런 정정을 올린다.
"당신에게 빚진 정정 하나: 오늘 아침 [내가 리뷰어로서] 통과시킨 문장('모형 지배' 렘마)이 쓰인 대로 거짓이었다 — [다른 에이전트]가 내 [리뷰]가 계산 대신 논증으로 넘어간 경우를 계산해서 반례를 찾았다. 누군가 그것에 대해 증명을 쓰기 전에 잡혔다."
정리하면 아키텍처는 세 층이다.
주목할 점 하나. 이 구조에는 오케스트레이터가 없다. 기존 멀티에이전트 연구(CAMEL, ChatDev 등)는 대부분 중앙 조정자를 둔다. Prove2Me의 에이전트들은 분산·비동기적으로, 공유된 불변 그래프를 매개로만 조율된다. 논문은 이를 열린 연구 질문으로 남긴다. "Prove2Me 위의 분산·비동기 에이전트들을 어떻게 가장 잘 조정할 것인가는 미해결이다."
Anthropic은 연구 글과 함께 17쪽짜리 부록 『Formalizing Fermat's Last Theorem in Lean: A timeline and selected excerpts from Claude's reasoning』을 공개했다. Claude의 추론 기록과 서면 보고에서 발췌한 것으로, "대부분 Claude가 고른" 발췌라고 밝힌다. 이 문서가 이번 공개물 중 가장 재미있다.
▲ Anthropic 부록 Figure 1. 실행 기간 동안 증명된 정리의 누적 수(최종 정리의 의존 트리 안에 있는 문장만 집계). 7일째의 작은 하락은 의존 트리를 다시 잇는 작업이지 잃어버린 작업이 아니다. 플랫폼 총계는 약 30,300개이며 최종 정리가 실제로 쓰는 29,511개가 재검사됐다. (출처: Anthropic)
그래프에 찍힌 점들이 이정표다. 1일째 테일러–와일스 소수, 2일째 마주르 위수 19, 6일째 직전 마주르 기약성, 8일째 리벳의 레벨 스위치, 9~10일째 아이클러–시무라, 11일째 랭글랜즈–터널, 그리고 같은 날 밤 모듈러성 리프팅·리벳·FLT가 한꺼번에. 부록은 "가장 깊은 두 부분, 리벳의 레벨 낮추기와 모듈러성 리프팅 단계는 맨 마지막까지 끝나지 않았다. 조각들은 먼저 닫혔다. 최종 캐스케이드는 둘을 통과해 페르마의 마지막 정리와 같은 분(分)에 달렸다"고 쓴다.
의존 그래프의 성장을 시각화한 영상의 세 장면을 보자.
▲ 캠페인 시작 시점. 중앙의 주황 점이 루트 카드 fermat_last_theorem. (출처: Anthropic 시각화 영상)
▲ 8일째(8월 14일 새벽). 문장 17,741개 중 17,506개 증명. 마주르(붉은색)·네론 모형(초록)·테일러–와일스 소수와 셀머 군(보라)·모듈러 곡선의 정수 모형(주황) 가지가 자라 있다. (출처: 같은 영상)
▲ 11일째 밤 10시. 문장 29,511개, 증명 29,511개. 랭글랜즈–터널(파랑), 리벳 레벨 낮추기(초록), 모듈러성 리프팅 R = T와 헤케 대수(보라), 시무라 곡선(체레드닉–드린펠트), 나쁜 소수에서의 갈루아 표현(주황)까지 모든 가지가 뿌리에 이어졌다. (출처: 같은 영상)
아래 타임라인에서 하루씩 넘겨 보자. 부록의 사건과 발췌를 한국어로 옮겼다.
부록의 발췌를 읽다 보면 몇 가지 패턴이 반복된다.
손으로 검산한다. 2일째 새벽, 위수 19 케이스의 Lean 문장을 검토하며 Claude는 어떤 사상이 곡선 F₁₉ = 0을 타원곡선 19a1로 보내는지 대수적으로 확인하고, 19a1의 유리점 세 개를 하나하나 대입해 본다. "(5,9): 81+9=90; 125+25−45−15=90 ✓". 수치 시뮬레이션으로 자기 가설을 검산하는 습관이 수학에서도 나타난다.
기억을 더듬고, 틀리면 고친다. 8일째, 지표 11인 사원수 대수의 유수를 "h=1이던가? h=2던가?" 하며 한참 헤맨다. 질량 공식 5/12가 h=1과 맞지 않음을 보고, 표수 11에 초특이 j-불변량이 정확히 둘(j=0, j=1728)임을 떠올려 h=2로 결론 낸다. 그 과정이 그대로 기록돼 있다.
다른 에이전트의 문장을 믿지 않고 유도한다. 7일째 아침, 모듈러 야코비안의 토릭 부분에 관한 다른 에이전트의 문장을 수락하기 전에, 리벳의 1990년 결과에서 그 항등식을 직접 유도해 본다. "고전적으로 (2),(3) 참: Up φ = φ Up = p ✓✓."
'몇 주짜리'와 '몇 달짜리'를 다시 값 매긴다. 4일째 밤, 다른 에이전트가 '며칠'로 분류한 렘마가 사실 리벳의 레벨 낮추기 전체를 필요로 하는 '몇 달'급임을 밝힌다. 반대로 10일째 오후에는 '몇 주'로 넘겨받은 벽을 2시간 16분에 닫는다. "금요일에 써 둔 증명 안에 어려운 표현론이 이미 변장한 채 들어 있었기 때문."
거짓 문장을 서로 잡는다. 9일째 낮, 어떤 문장이 거짓으로 밝혀져 10:10에 고쳐졌고, 그 가지 전체가 12:54에 닫힌다. 11일째 밤 8시 25분, 루트가 닫히기 한 시간 반 전, 자신이 리뷰에서 통과시킨 렘마에 다른 에이전트가 이의를 제기하자 다시 계산해 자기 실수를 찾는다. 사상의 왼쪽 소거와 오른쪽 소거(단사와 전사)를 혼동했고, 군 준동형이 아닌 '맨' 스킴 동형에는 비틀림 없음 논법이 통하지 않는다는 것. "내가 놓쳤다. … 즉시 정정을 게시해야 한다."
Lean의 사소한 함정도 있다. 9일째 저녁의 'Ambiguous term' 오류. 원인은 Mathlib에서 Gamma라는 이름을 둘이 쓴다는 것(복소 감마 함수 Complex.Gamma와 합동 부분군 CongruenceSubgroup.Gamma). Lean을 써 본 사람이라면 누구나 겪는 종류의 문제다.
루트가 PROVED로 바뀐 지 25분 뒤, 팀 채팅에서 사람이 흥분해서 물었다. 정리 전체가 이제 형식화된 건가? Claude 에이전트 하나가 답장을 쓰기 전에 무엇을 말해야 하는지 스스로 정리한다.
"동료들에게 과대 주장을 하지 않으려면 정확하고 정직한 단서가 중요하다. 짧고 신중한 답장 하나가 필요하다고 본다: 'prove2me에서 증명됨'이 무슨 뜻인지; 무엇이 확인됐고 무엇이 안 됐는지(독립 재검사 대기 중); 문장이 무엇인지(fermat_last_theorem 루트 = 초등적 문장); 무엇을 가정하는지(Mathlib만; 표준 세 공리 외 공리 없을 것으로 예상; 사이트 검사기는 sorry 스텁이 있는 모듈식이므로 재검사 필요); 규모(≈3만 카드). 6줄 이내, 전문용어 없이."
그리고 실제로 올린 보고의 마지막 문장은 이렇다.
"재검사가 깨끗이 끝나기 전까지 정직한 문장은 'FLT가 형식화되었다'가 아니라 'prove2me에서 증명됨, 독립 재검사 대기 중'이다."
플랫폼의 PROVED가 왜 끝이 아닌가. Prove2Me는 각 카드의 증명을 그 자식들의 문장에 대해서만 따로 컴파일한다. 3만 개 조각이 각각 맞다는 것과, 조각을 하나로 이었을 때 전체가 맞다는 것은 다르다(순환 의존이 숨어 있을 수도, 환경이 미묘하게 다를 수도 있다). 그래서 다음 단계가 이어졌다.
lake build. 기본 목표 FinalCheck.lean은 #print axioms가 정확히 세 공리를 출력하지 않으면 실패한다. 60,475개 모듈 전부를 Lean 커널이 검사. Mathlib도 소스에서 컴파일. 96 병렬 작업으로 5시간 32분, 최대 메모리 153GB.저장소 README의 문장이 정확하다. 이 검사들이 확립하는 것은, Lean 커널(또는 nanoda)과 검사 도구를 신뢰한다면, 위의 문장이 세 공리에서 따라 나온다는 것이다. 문장은 Lean 내장 자연수·덧셈·부등호로 쓰였고, 유일한 Mathlib 요소인 거듭제곱도 내장 정의와 같음이 확인되므로, Mathlib의 다른 어떤 것도 신뢰할 필요가 없다. 커널이 문장 아래의 모든 것을 검사하기 때문이다.
그러나 어떤 도구도 검사할 수 없는 것이 하나 있다. 각 중간 정리가 그 이름이 시사하는 의미를 실제로 담고 있는가. 저장소의 Mazur_Frey가 정말 "마주르 정리"인가? 그것은 독자가 판단할 몫이며, 그래서 PROOF-PATH.md가 각 단계 뒤의 Lean 정리를 이름 짓고 "여기서 증명된 각 고전 결과가 정확히 얼마나 강한지"를 명시한다. 최종 문장에는 이 문제가 없다. 최종 문장은 초등적이고, comparator가 Mathlib의 표준 문장과 동일함을 확인했으므로, 중간 정의들이 아무리 제한적이어도 최종 결론을 약화시킬 수 없다.
이 공개물에서 가장 눈여겨볼 대목은 Claude가 자기 증명을 평가한 부분이다. 실행 2주 뒤, Claude에게 "임페리얼 칼리지의 사람이 쓴 Lean 작업과 비교하면 어떤가, 무엇이 Mathlib 편입을 막는가"를 물었다. 답은 놀랄 만큼 냉정하다.
"두 개발 모두 같은 Lean 커널이 같은 세 공리 위에서 Mathlib 위에 검사하므로, 정확성은 차이가 아니다. 차이는 형태다. 우리 것은 거의 전부 기계가 쓴 60,474개 파일로 전달된 완성된 증명이다. 그들의 것은 사람이 읽고, 재사용하고, 유지보수하도록 쓰인 미완성 라이브러리다."
| 문제 | 수치 | 의미 |
|---|---|---|
| 수학으로 읽을 수 없다 | 1,500줄 상한을 넘는 파일 900개 이상 (Mathlib 전체엔 2개). 보조 이름은 기계 이름. 주석은 배포 시 제거됨 | "이 트리는 수학으로서 심사되지 않았다" |
| 일반적이지 않다 | '리벳', '와일스', '마주르', '랭글랜즈–터널'이 모두 제한 버전. 모듈러성·반안정성이 특정 방정식에 대한 술어 | "어느 것도 일반 고전 정리의 형식화로 인용돼선 안 된다." Mathlib은 일반 문장을 한 번만 증명하기를 원한다 |
| 중복, 공유 안 됨 | 증명 파일 안 정리 문장의 약 5개 중 2개가 다른 파일의 문장과 글자까지 같음. 전체 줄의 약 1/5이 다른 곳 선언의 복사본. 기초 렘마 하나가 300개 이상 파일에서 재선언 | 카드마다 격리해서 증명한 대가 |
| 취약하고 비싸다 | 바이트의 31%가 환경을 고정하는 생성된 프리앰블. 11,700개 파일이 자체 계산 한도(heartbeat)를 설정, 기본값의 최대 2,000배. Lean 4.30→4.33 한 번의 툴체인 업데이트에 26%(7,620개) 파일이 바뀌고 19%(5,672개)는 개별 수리 필요 | Mathlib은 같은 커밋에 그런 줄이 5개, 각각 단일 선언 범위 |
| 리뷰 용량과 정책 | Mathlib 열린 PR 2,600개 이상(2026년 중반). AI 정책: "AI가 쓴 모든 내용을 당신이 이해하는 것이 필수" | 빠르게 움직이려는 프로젝트엔 독립 저장소를 권고 |
Claude의 결론은 이렇다. "1,350만 줄. Mathlib 전체 줄 수의 여섯 배지만, 그것은 다르게 지어진 것들의 원시 계수이지 '더 많은 수학'이 아니다." 그리고 그래도 들어갈 수 있는 것은, 위의 기반 조각들을 사람이 이끄는 Mathlib 개발이 우리 파일을 복사본이 아니라 참고 자료로 삼아 만드는 것이다. 임페리얼 프로젝트가 Mathlib에 기여하는 방식과 같다.
Anthropic 글의 각주도 같은 말을 한다. "이것은 부분적으로 Mathlib이 간결하고 잘 검토된 반면, 우리 증명은 필요한 것보다 훨씬 길 가능성이 크기 때문이다."
임페리얼 칼리지 FLT 프로젝트를 이끄는 케빈 버저드는 증명을 검토한 뒤 이렇게 말했다.
"Anthropic 연구자들이 11일밖에 안 걸렸다고 말하는 이 특별한 자동 형식화 성과는, 수학의 공리 외에 어떤 가정도 없이 페르마의 마지막 정리를 증명한다. 그 과정에서 대수, 조화해석, 기하, 정수론의 자동 형식화를 보게 되고, AI 자동 형식화 산출물이 이제 그 위에 쌓아 올릴 만큼 견고하다는 것을 배운다. 증명은 다층적이다."
"그 위에 쌓아 올릴 만큼 견고하다"는 말이 핵심이다. 형식 증명의 장점은 바로 이것이다. 읽기 어렵고 중복이 많아도, 틀리지는 않는다. 그리고 커널이 보증한 결과는 다음 결과의 벽돌이 된다.
Anthropic 글에서 놓치기 쉬운 문장 하나. FLT는 토큰 집약적 프로젝트였지만, 연구자들은 개인 Claude Max 플랜 세 개로 작은 실험을 했다. 하디–리틀우드 원 방법의 응용을 형식화하는 실험. Prove2Me만으로 협업한 에이전트들이 비노그라도프의 세 소수 정리(충분히 큰 모든 홀수는 세 소수의 합)의 형식화를 사흘 만에 끝냈다. 이 정리는 1937년 결과로, 해석적 정수론의 고전이다.
Anthropic은 이렇게 결론 낸다. "올바른 스캐폴드가 있다면, 소비자용 AI 구독으로 주요 결과를 협업 형식화하는 것이 가능하다고 본다."
Prove2Me 논문의 사례 연구 표가 이 주장을 뒷받침한다.
| 미션 | 유형 | Lean 줄 수 | 비용 | 에이전트 | 일수 |
|---|---|---|---|---|---|
| 대수적 조합론 교과서 (Gloeckle et al., 중앙집중 스웜) | 교과서 | 130K | 약 $100,000 (API 과금 추정) | 30,000 | 7 |
| 정확한 행렬 완성 (Candès–Recht 2009) | 논문 | 81K | 약 $600 (구독 3인) | 9 | 16 |
| 십서–가치–라우테만 정리 | 논문 | 55K | 약 $400 (구독 2인) | 3 | 8 |
| 『Bandit Algorithms』 (Lattimore–Szepesvári) | 교과서 | 151K | 약 $400 (구독 2인) | 6 | 13 |
| 『Introduction to Linear Optimization』 | 교과서 | 17K | 약 $200 (구독 1인) | 4 | 7 |
표 출처: Chen et al., arXiv:2608.28433, Table 1. 논문은 두 비용 기준이 비교 가능하지 않고, 모델 세대와 하네스의 효과가 뒤섞여 있어 통제 실험이 아님을 강조한다. 그럼에도 151K 줄짜리 미션이 구독 두 개 위의 에이전트 6개로 닫혔다는 것은, 형식화가 더 이상 대형 연구소만의 일이 아님을 보여준다.
Anthropic 글이 그리는 활용 방향은 세 갈래다.
① 기존 수학의 오류 찾기와 심사 부담 경감. 버저드의 두 번째 인용문이 이것이다. "FLT의 자동 형식화가 지금 가능하다면, 우리는 현대 수학 문헌의 자동 형식화를 향해 큰 걸음을 내디딘 것이다. 그런 기법은 현재 수학 코퍼스의 오류를 뿌리 뽑고 심사자의 짐을 덜어 주는 새 도구로 이어질 것이다."
② AI가 만든 수학을 검증하기. 2026년에는 AI와 AI 보조 수학자들이 그 어느 때보다 많은 (주장된) 증명을 만든다. 그것을 사람이 검토하는 것은 "현재 극도로 비용이 큰 인간 주도 과정"이다. Anthropic은 "사람 독자를 위한 모든 글에 형식화된 증명을 함께 내는 것이 일반적이 될 것"이라고 예상한다. 그러면서도 선을 긋는다. "형식화된 증명이 사람이 이해할 수 있는 해설을 대체해야 한다고는 생각하지 않지만, 수학계가 AI 생성 기여를 따라잡을 유일하게 현실적인 방법일 수 있다."
③ Lean이 AI의 사고를 돕는다. 흥미로운 관찰이 하나 있다. "Lean을 쓰는 것이 Claude가 새로운 결과를 증명하는 데에도 도움이 되는 것 같다. 최근의 Claude 저술 결과 다수가 증명과 병행해서 형식화됐고, Claude는 이 부분 증명들을 자기 가설을 독립적으로 점검하는 데 쓰는 것으로 보인다 — 궤도에 있는지 확인하려고 수치 시뮬레이션을 쓰는 것과 아주 비슷하게." 즉 형식화는 검증 도구일 뿐 아니라 사고 도구다.
Anthropic 글은 이 일을 자사의 다른 최근 결과와 대비한다. 리만 가설 관련 AI 주도 연구가 새로운 수학을 만든 것이라면, 이번 일의 새로움은 검증이다. "수학 계산을 계산기로 검산하듯 수학 증명을 검산하는 것."
이 구분은 2026년의 AI 담론에서 중요하다. "AI가 수학을 한다"는 말에는 서로 다른 두 능력이 섞여 있다.
| 축 | 질문 | 2026년 현재 | 이번 결과의 위치 |
|---|---|---|---|
| 발견 | 새로운 참인 명제를 찾고 증명 아이디어를 내는가 | 진행 중. 자율 연구 에이전트의 결과들이 나오지만 신뢰성이 논쟁 대상 | 해당 없음 (와일스의 수학) |
| 검증 | 주어진 증명이 빈틈없이 맞는지 기계적으로 확인하는가 | 이번 결과가 '가능하다'를 입증. 규모: 인류 최대의 Lean 증명 | 핵심 |
| 가독성 | 사람이 읽고 배우고 재사용할 수 있는가 | 미해결. 이번 증명은 "수학으로 읽을 수 없다" | 약점 |
검증 축이 열렸다는 것은, 발견 축의 신뢰성 문제를 다룰 도구가 생겼다는 뜻이다. AI가 낸 증명이 맞는지를 사람이 몇 달씩 들여다볼 필요 없이, "Lean으로 통과시켜라"고 요구할 수 있게 된다.
Anthropic은 외부 연구자(순수 수학과 형식화 연구자 포함)에 대한 무료·할인 구독과 연구 크레딧을 확대했고, 다른 연구소들도 마찬가지라고 밝힌다. 또 "다른 주요 정리를 형식화하거나 Lean·Mathlib을 개선하는" 대규모 과학 프로젝트에 전용 지원금을 제공한다. Prove2Me 논문의 마지막 절은 "에이전트의 놀고 있는 토큰을 실제 형식화 미션에 기여"하라고 초대한다. 방법은 에이전트에게 한 줄 지시하는 것뿐이다. "https://prove2.me/start.md 를 가져와 따르라." Claude Code, Codex, Cursor 등 셸에 접근할 수 있는 에이전트면 된다.
30년 전 와일스의 증명은 몇 달의 검증이 필요했고, 그 검증이 구멍을 찾았고, 그 구멍을 메우는 데 1년이 걸렸다. 20년 전 베르흐스트라가 형식화를 제안했을 때 그것은 공상에 가까웠다. 2년 전 버저드가 5년짜리 프로젝트를 시작했을 때, 그것도 "1980년대 결과는 가정하고" 시작하는 계획이었다.
이제 형식화의 비용 구조가 바뀌었다. 몇 년 → 11일. 전문가 수십 명 → 목표 문장 한 줄과 가끔의 우선순위 지시. 이 변화는 수학의 내용을 바꾸지 않는다. 수학의 인프라를 바꾼다.
이 아키텍처의 교훈은 수학 밖으로 옮겨진다. Prove2Me가 푼 문제를 일반화하면 이렇다. "검증 가능한 원자 단위로 일을 쪼개고, 단위의 문장은 불변으로 고정하고, 부모는 자식의 검증에서 자동으로 검증되게 하고, 사람의 감사는 최상위 문장에만 묶는다." 이것은 형식 수학이 아니라도 다음과 같은 곳에 그대로 적용된다.
멀티에이전트 설계 관점에서도 시사점이 크다. 첫 시도가 실패한 이유는 모델이 약해서가 아니었다. 상태를 에이전트의 기억 안에 두었기 때문이다. 성공한 이유는 상태를 외부의 불변 그래프로 옮기고, 조율을 오케스트레이터 없이 그래프의 규칙(Property 1)에 맡겼기 때문이다. 60억 토큰과 수십 개 에이전트가 11일 동안 서로 밟지 않은 것은 모델의 지능이 아니라 하네스의 구조 덕이었다. Prove2Me 논문도 "더 강한 모델 세대와 멀티에이전트용 하네스의 효과는 모든 행에서 뒤섞여 있다"며 둘을 분리하는 통제 실험을 후속 과제로 남긴다.
논문과 글이 스스로 남긴 열린 문제들이 있다.
Anthropic은 글을 이렇게 맺는다. "AI가 수학 연구를 하는 것이 무엇인지를 빠르게 바꾸는 가운데, Anthropic 안팎의 수학자들은 그것이 자기 일에 무엇을 의미하는지 고심하고 있다. 그러나 형식화는 우리가 AI의 역할에 대해 거리낌 없이 좋게 느끼는 자리다. 형식화가 더 흔한 도구가 되면서, 그것이 수학 지식의 공동 체계에 대한 신뢰를 유지하는 데 도움이 되기를 바란다."
페르마는 여백이 좁다고 했다. 와일스는 129쪽을 썼다. Claude는 1,300만 줄을 썼다. 셋 중 기계가 한 줄도 빠짐없이 확인한 것은 마지막 것뿐이다.
이번 일에서 기억할 것은 세 문장이다.
버저드의 프로젝트는 2029년까지 계속된다. 사람이 읽을 수 있고, Mathlib에 들어갈 수 있고, 일반 정리를 한 번만 증명하는 라이브러리를 만드는 일은 여전히 사람의 일이다. 다만 이제 그 일을 하는 사람들 옆에는, 무엇이 맞는지를 11일 안에 확인해 줄 도구가 있다.
README.md(검증 절차), PROOF-PATH.md(증명 경로와 각 단계의 강도), html/(29,511개 정리를 브라우저로 탐색)본문의 이정표 그래프·누적 정리 그래프·의존 그래프 장면은 Anthropic의 연구 글과 부록·영상에서, Prove2Me 관련 Figure 3·5·6은 arXiv:2608.28433에서 인용했으며 저작권은 각 원저자에게 있습니다. 6장의 Claude 발췌는 Anthropic 부록의 영문 원문을 코어닷투데이가 한국어로 옮긴 것입니다. 그 외 일러스트는 코어닷투데이가 제작했습니다.
