페르마의 마지막 정리 Lean 형식화: Claude 에이전트 1,000개와 30시간, 무엇이 확인됐나

페르마의 마지막 정리가 Lean으로 완전히 형식화되었습니다. Lean은 컴퓨터가 증명의 모든 단계를 확인하는 언어입니다. 최초의 완전한 형식화는 2026년 9월 4일 Anthropic이 발표했습니다. 공개되지 않은 연구용 모델이 8월에 11일 동안 이를 썼고, 연구자 한 명이 이따금 방향을 잡아 주었습니다. 코드는 공개되어 있으며, 이 정리를 사람이 형식화하는 프로젝트를 이끄는 임페리얼 칼리지 런던의 Kevin Buzzard가 이를 컴파일하고 "확인 결과 문제가 없다"고 보고했습니다.⁷ 2026년 11월 9일 Anthropic은 Claude Fable 5.2를 실행하는 에이전트 약 1,000개로 이루어진 팀이 "사람의 개입을 최소한으로 줄인 채 단 30시간 만에 정리를 완전히 형식화했다"고 말했습니다.¹ 기술 해설 글은 실행 시간을 28.7시간으로 적고, 이 실행을 "증명을 재현한" "토이 실험"이라고 부릅니다.² 정리 자체는 1994~95년 Andrew Wiles(앤드루 와일스)가 Richard Taylor와 함께 증명했습니다. 두 실행 모두 이미 알려진 그 증명을 기계로 확인한 것입니다.

30시간 실행에 대해 확립된 것은 훨씬 적습니다. 11월 12일 현재 그 Lean 코드는 공개되지 않았고, Anthropic 밖의 누군가가 이를 확인했다는 보고도 찾지 못했습니다. 시간, 토큰, 규모에 관한 수치와 Claude Opus 5.5와의 비교는 Anthropic 자신의 글에서, 그리고 모델마다 한 번씩 돌린 실행에서 나온 것입니다. 어느 실행이든 Lean 확인을 통과했다는 것은, 진술된 정리가 Lean의 공리에서 따라 나온다는 것을 보여 줍니다. 형식적 명제가 페르마가 주장한 내용을 말한다는 것을 보여 주지는 않으며, 증명을 읽을 수 있게 만들어 주지도 않습니다. 9월 증명에 대해서는 Buzzard와 별도의 확인 도구가 명제를 확인했습니다. 새 실행에 대해서는 그런 확인을 했는지 Anthropic이 밝히지 않았습니다.

아래에서는 무엇이 바뀌었는지, Lean 확인이 무엇을 다루는지, 무엇이 공개되어 있는지, 누가 무엇을 확인했는지, Buzzard가 무엇이라고 했는지, 관련 발표 두 가지, 그리고 짧은 역사를 정리합니다. 모든 출처는 2026년 11월 12일에 확인했습니다.

주요 용어#

• Lean: 증명 보조기(proof assistant)입니다. Lean의 **커널(kernel)**은 각 증명을 언어의 규칙에 비추어 확인하는 작은 프로그램입니다.
• Mathlib: 대부분의 Lean 프로젝트가 바탕으로 삼는, 커뮤니티가 만든 형식화된 수학 라이브러리입니다.
• sorry: 미완성 증명도 컴파일되게 해 주는 자리 표시자입니다. 완전한 형식화에는 하나도 없습니다.
• 공리(axioms): 증명이 출발점으로 삼을 수 있는 가정입니다. Mathlib은 propext, Classical.choice, Quot.sound 세 가지에 기댑니다.
• Comparator: Lean 프로젝트에서 만든 도구로, 따로 작성된 명제와 허용된 공리 목록에 비추어 증명을 확인한 뒤 커널에서 다시 실행합니다.¹⁶
• nanoda: Rust로 작성된 독립적인 Lean 커널로, 두 번째 검사기로 쓰입니다.

페르마의 마지막 정리는 Lean으로 형식화되었나요? 누가 했나요?#

이 정리는 n이 2보다 클 때 aⁿ + bⁿ = cⁿ을 만족하는 양의 정수 a, b, c는 없다고 말합니다. Anthropic의 공개 저장소는 이를 Lean으로 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이라고 진술합니다.⁵

Anthropic의 첫 실행은 2026년 8월 7일, 컬럼비아 대학교 Tianyi Peng 그룹이 만든 협업 형식화 플랫폼 Prove2Me에서 시작되었고,¹⁵ 최종 정리는 8월 17일 저녁 증명된 것으로 표시되었습니다. 수십 개의 에이전트가 "Claude Fable 5.1과 대략 비슷한 범용 내부 연구 모델"을 실행했고, 출력 토큰 약 60억 개를 썼습니다. 글에 따르면 사람이 수학적으로 기여한 것은 "Tianyi가 이따금 내린 상위 수준의 지시에 그쳤다".³ 함께 공개된 타임라인 문서는 사람이 "목표 정리의 한 줄짜리 명제 말고는 수학도 Lean도 전혀 쓰지 않았다"고 덧붙입니다.⁴

결과물에는 정리 2만 9,511개와 Lean 코드 약 1,300만 줄이 들어 있습니다. 이 형식화는 Darmon, Diamond, Taylor가 1995년에 쓴 Wiles 논증 해설을 따르며, Mazur 정리와 Langlands–Tunnell 정리처럼 논증에 들어가는 깊은 결과들을 논증에 필요한 특수한 경우에 한해 증명합니다. 또 Buzzard의 임페리얼 프로젝트와, 정칙 소수(regular prime)에 대한 이 정리의 이전 형식화인 flt-regular에서 파일 106개를 출처를 밝혀 가져와 고쳐 썼습니다.⁴

페르마의 마지막 정리는 Freek Wiedijk의 100대 정리 목록에서 마지막까지 형식화되지 않은 항목이었습니다. Buzzard는 이 작업이 "20년 된 이 벤치마크를 마무리한다"고 썼고,⁷ 2026년 11월 1일에 마지막으로 수정된 Wiedijk의 페이지는 이제 100%로 표시되어 있으며 이 정리를 "Lean, Anthropic"의 것으로 적고 있습니다.¹³

30시간 실행은 9월과 비교해 무엇이 새로운가요?#

가장 자세한 설명은 Barry Zhang, Tianyi Peng, Elle Najt, Keller Scholl, Lance Martin이 Anthropic 개발자 블로그에 쓴 글입니다.² 목표는 이 결과를 "Prove2Me도, 작업을 지휘하는 연구자도 없이, 범용 도구로 만든 하네스(harness)를 써서" 다시 해내는 것이었습니다.

리드(lead) 에이전트 하나와 보조(helper) 에이전트 999개는 각자 네트워크에 접속할 수 없는 가상 머신, Lean과 Mathlib, Git 브랜치 하나, 그리고 공유 데이터베이스를 받았습니다. 출발 자료도 있었습니다. "우리는 에이전트들에게 명제 60개의 목록, 고전적 경로를 한 문장으로 요약한 개요, 그 명제들이 쓰는 정의, 그리고 이전 형식화에서 증명된 보조정리 47개를 주고, 리드와 보조 역할을 배정했다."

시작한 지 약 27분이 되었을 때 명제 3개가 이미 증명되어 있었습니다. 리드 에이전트는 보조 에이전트 대부분이 예산 안에서 해낼 수 없다고 판단한 명제 47개를 일단 제쳐 두고, 거의 모든 보조 에이전트를 나머지 10개에 배정했습니다. 이 10개는 약 70분 안에 증명되었습니다. 팀은 그 뒤 47개로 돌아갔습니다. 가장 어려운 조각은 Langlands–Tunnell 정리였고, 이 조각을 맡은 캡틴(captain) 에이전트는 "시간 안에 끝낼 가능성이 1% 미만"이라고 보았습니다. 팀은 이를 과제 2,418개로 이루어진 트리로 쪼갰고, 28.4시간째에 증명했습니다. 최종 정리는 28.7시간째에 뒤따랐고, 리드 에이전트는 이렇게 썼습니다. "모두 고맙습니다. 페르마의 마지막 정리가 main에 올라갔고, 공식 검사기로 커널 확인을 마쳤습니다."

기록된 개입은 두 가지입니다. 하네스는 리드 에이전트에게 남은 시간을 알리는 자동 알림을 19번 보냈고, 18시간째 무렵 Anthropic은 "마지막 저장 지점에서 실행을 다시 시작하고 에이전트들에게 12시간을 더 주었다".

출시 발표 글은 이를 단순화합니다. 28.7시간을 30시간으로 적고, 기술 해설 글이 출력 토큰이라고 한 것을 "액션 토큰(action tokens)"이라고 부르며, 기술 해설 글이 Fable 5.2의 초기 버전이라고 한 모델을 Fable 5.2라고 부릅니다. 11월 9일에 보관된 첫 문구는 또 Fable 5.2가 "수학 참고 자료는 전혀 쓰지 않았고, 진행 상황을 채점하기 위한 중간 정리 명제 목록만 썼다"고 말했습니다.²³ 11월 11일 Anthropic은 그 구절을 지우고 위의 출발 자료를 인용하는 각주를 더했으며, 해당 단락을 "모델에 제공한 정보를 더 정확하게 기술하기 위해" 수정했다고 밝혔습니다.¹

	첫 형식화	30시간 실행
발표	2026년 9월 4일	2026년 11월 9일, 11월 11일 수정
모델(Anthropic의 보고)	"Claude Fable 5.1과 대략 비슷한" 내부 연구 모델	"Claude Fable 5.2의 초기 버전"
시간	11일, 8월 7일부터 17일까지	28.7시간, 18시간째 무렵 마지막 저장 지점에서 재시작
에이전트	수십 개	약 1,000개: 리드 1개, 보조 999개
사람의 관여(설명된 대로)	연구자 한 명이 이따금 내린 상위 수준의 지시. 한 줄짜리 목표 명제는 사람이 작성	방향을 잡는 연구자 없음. 첫 증명에서 가져온 명제, 개요, 정의, 보조정리 47개를 제공. 자동 알림 19번
조율	Prove2Me 플랫폼	Git, 공유 데이터베이스, 격리된 샌드박스
출력 토큰	약 60억 개	그 3분의 1. 수치는 밝히지 않음
증명 규모	정리 2만 9,511개, 약 1,300만 줄	길이는 7분의 1. 줄 수는 밝히지 않음
공개된 것	Lean 코드, 빌드·확인 스크립트, 둘러볼 수 있는 페이지, 17쪽 분량 타임라인	블로그 글 두 편과 그 그림

‘형식화했다’는 무슨 뜻이고, Lean 확인은 무엇을 입증하나요?#

증명을 형식화한다는 것은 Lean이 공리에서부터 모든 단계를 확인할 수 있도록 증명을 다시 쓰는 것입니다. 9월 저장소가 빌드되었다면, 커널이 그 안의 모든 선언을 받아들인 것입니다. 빌드는 또 fermat_last_theorem이 정확히 표준 공리 세 개에만 기대지 않으면 실패하도록 설정되어 있어, 그 아래 어디에도 sorry나 추가된 공리가 없음을 보장합니다.⁵

이것은 증명에 대해서는 강한 증거이지만, 명제에 대해서는 제한된 증거입니다. Buzzard의 11월 12일 글은 두 줄짜리 예를 듭니다. a, b, c가 양수라는 조건을 빠뜨린 페르마의 마지막 정리의 Lean 정의는 거짓인데, Lean의 자연수에는 0이 포함되기 때문입니다. 그는 "그렇다고 명제가 컴파일되지 않는 것은 아니다!"라고 씁니다. 컴파일되지 않는 것은 그 명제의 증명뿐입니다.⁸ 누군가는 명제를 읽고 그것이 올바른 명제인지 확인해야 합니다.

한계는 세 가지 더 있습니다. 저장소의 README는 "어떤 도구도 확인할 수 없는 것은 각 중간 정리가 그 이름이 암시하는 뜻을 갖는지다"라고 적습니다.⁵ Lean 증명은 아무것도 설명하지 않습니다. 같은 README는 소스가 "읽히기보다 확인되도록 쓰였다"고 말합니다. 그리고 커널을 신뢰해야 합니다. Buzzard는 발견된 지 네 시간 만에 고쳐진 Lean 커널의 건전성 버그(soundness bug)를 떠올리며, 서로 독립적인 여러 커널로 확인하면 그런 버그를 막을 수 있다고 주장합니다.⁸

그의 글은 AI가 생성한 Lean 코드에 던질 네 가지 질문을 제시합니다. 공개된 자료로 두 실행에 적용하면 다음과 같습니다.

Buzzard의 질문	첫 형식화	30시간 실행
Lean 명제가 비형식적 명제와 일치하는가?	Lean의 자연수와 Mathlib의 거듭제곱 함수를 씀. Buzzard는 이를 읽었다고 말함. comparator가 Mathlib만 가져오는(import) 파일과 대조해 일치를 확인	밝혀지지 않음. 에이전트들은 명제와 정의를 건네받았음
코드가 컴파일되는가?	그렇다. Anthropic이 처음부터 새로 한 빌드에서, 그리고 Anthropic이 빌려준 기계로 한 Buzzard의 빌드에서	리드 에이전트가 "공식 검사기로 커널 확인을 마쳤다"고 보고함. 외부에서 빌드할 수 없음
진술된 그대로의 정리를 증명하는가?	Comparator 통과. Anthropic과 Buzzard가 각각 실행	보고되지 않음
Lean 커널의 버그를 악용하는가?	Anthropic의 실행에서 nanoda가 모든 선언을 받아들임. Anthropic이 타입 규칙은 바꾸지 않는다고 말하는 작은 패치 네 개를 적용해 빌드	보고되지 않음

새 Lean 코드는 공개되었나요? 누구나 다시 빌드할 수 있나요?#

아니요, 11월 12일 현재로는 아닙니다. 출시 발표 글도 기술 해설 글도 코드를 링크하지 않습니다. GitHub에 있는 Anthropic의 페르마 저장소는 9월 24일에 마지막으로 변경되었고, Lean 4.33.1과 Mathlib v4.33.0 기반의 9월 증명만 담고 있습니다.⁵ Anthropic의 다른 공개 Lean 저장소인 formal-math에는 관련 없는 프로젝트 세 개가 있습니다.¹⁷ 이 실행의 프롬프트, 로그, 채점기(grader), 하네스가 공개되었다는 것도 찾지 못했습니다.

이 실행의 최종 명제, Lean과 Mathlib 버전, 줄 수로 잰 규모, 그리고 여기에 comparator나 두 번째 커널을 돌렸는지는 모두 알려져 있지 않습니다.

9월 증명은 하드웨어가 충분하면 누구나 다시 빌드할 수 있습니다. Anthropic에서는 병렬 작업 96개로 빌드에 5시간 32분이 걸렸고 메모리 사용량은 최대 153GB였으며, README는 약 15시간 걸리는 comparator 확인에 300GB를 잡아 두라고 권합니다. Buzzard는 처음에 자기 컴퓨터로 시도했다가 "아주 빨리 메모리가 바닥났고", 그 뒤 Anthropic이 코어 96개짜리 기계를 임시로 쓸 수 있게 해 주었습니다.⁸ README는 이 저장소를 "연구 산출물. 유지 관리하지 않으며 기여를 받지 않는다"라고 부릅니다.⁵

무엇이 자체 보고이고, Anthropic 밖에서는 무엇을 확인했나요?#

30시간 실행에 관한 모든 것은 Anthropic에서 나왔습니다. 네 가지는 좀 더 자세히 볼 필요가 있습니다.

• 모델. 에이전트들은 Fable 5.2의 "초기 버전"을 실행했습니다.² 그것이 출시된 모델과 같은 방식으로 작동하는지는 밝혀져 있지 않습니다.
• Opus 5.5와의 비교. 출시 발표 글은 같은 설정에서 Opus 5.5가 "18시간 동안 형식화의 26%만 완료했고, 30시간이 지나도 진전이 거의 없었다"고 말합니다.¹ 이 그림은 완료율을 "증명된 명제의 가중 비율"로 재지만 가중치는 밝히지 않으며, 그림 설명에는 "모델마다 한 번씩 실행"했다고 적혀 있습니다. 한 번의 실행으로는 결과가 얼마나 달라지는지 보여 줄 수 없습니다.
• 토큰과 규모. 절대 수치는 나와 있지 않고, 두 글 모두 길이를 어떻게 쟀는지 말하지 않습니다. 이것이 중요한 이유는, Anthropic의 타임라인에 인용된 9월 증명에 대한 Claude 자신의 평가가 "증명 파일 전체 줄의 약 5분의 1은 트리의 다른 곳에 있는 선언을 그대로 복사한 것"이라고 보았기 때문입니다.⁴
• 출발점. 보조정리 47개와 정의들은 9월 4일부터 공개되어 있던 9월 형식화에서 왔습니다. Anthropic은 모델이 학습 과정에서 그 코드를 보았는지 밝히지 않습니다.

9월 증명에는 외부 독자가 있었습니다. Buzzard는 이를 컴파일하고 comparator를 돌렸으며, 한 댓글 작성자에게 한 말에 따르면 "코드베이스에서 (Claude에 따르면) 수학적 정의나 정리의 증명이 아닌 모든 줄을 직접 검사했다".⁷ 다른 댓글 작성자에게는 증명은 기계가 확인하지만, 명제는 누군가 읽어서 "그것이 올바른 정리에 대응하는지 확인해야 한다. 하지만 그건 내가 했다"고 설명했습니다. Anthropic은 그에게 "증명을 검토하고 의견을 준 데" 감사를 표합니다.³ 저장소 자체의 메타데이터에는 검토 상태가 여전히 "self-assessed"(자체 평가)로, 검토자 목록은 빈 채로 기록되어 있습니다.⁶

30시간 실행에 대해서는 외부 확인을 찾지 못했습니다. Buzzard의 11월 12일 글은 9월 증명을 다루지만 새 실행은 다루지 않습니다.⁸ Xena 블로그의 Bluesky 계정은 2025년 12월 이후 게시물이 없고, Mathstodon의 Lean과 Fermat 해시태그 두 개에도 이에 관한 글은 없었으며, Lean 커뮤니티 채팅의 공개 아카이브는 2026년 2월 28일에 마지막으로 갱신되어 그곳의 논의는 읽을 수 없었습니다.²² 수학자들이 운영하는 사이트 Proofs and Prompts는 11월 10일 이 발표를 다루면서, Anthropic이 "Claude 에이전트 1,000개로 이루어진 팀이 단 30시간 만에 페르마의 마지막 정리의 증명을 형식화했다고 자랑하고 있다"고 묘사했습니다.¹⁸ 이 사이트는 Anthropic이 이 정리를 전에도 형식화했다는 점을 독자들에게 상기시켰고, 에이전트들이 답을 어디서 찾았을지에 관한 농담 하나를 사이트의 공식 견해가 아니라고 밝히며 덧붙였습니다.

Kevin Buzzard는 무엇이라고 했고, 사람이 하는 FLT(페르마의 마지막 정리) 프로젝트는 어떻게 되나요?#

Buzzard의 임페리얼 프로젝트는 Richard Taylor가 설계하고 Khare와 Wintenberger의 연구를 빌려 온, 이 정리에 이르는 현대적 경로를 따릅니다.¹¹ 영국 공학·자연과학연구위원회(EPSRC)가 2024년 10월부터 2029년 9월까지 연구비 EP/Y022904/1로 지원하며, 밝혀 둔 첫 목표는 이 정리를 1980년대 말까지 알려진 결과들로 환원하는 것입니다.¹²

그는 9월 4일 자 글 "FLT: Anthropic has beaten me to it"(FLT: Anthropic이 나보다 먼저 해냈다)에서 Anthropic을 축하하면서, 이 결과가 무엇을 뜻하는지 분명하게 말했습니다.⁷ 그는 "수학적으로 보면 anthropic의 이 작업은 본질적으로 아무것도 알려 주지 않는다는 점에 유의하라"고 썼습니다. 이미 증명이 옳다고 99.9% 확신하고 있었고, "형식화는 그 증명에 관한 초기 문헌을 충실히 따를 뿐 아무것도 더하지 않는다"는 것입니다. 그러나 "이 작업이 알려 주는 것은 자동 형식화(autoformalization) 분야에서 무엇이 가능한가이다". 그는 기계 확인이 "내 분야의 여러 중요한 결과의 증명에서 정확히 무엇이 가정되고 있는지"를 보여 주리라 기대합니다. 한 달 뒤 그는, 공개된 글 없이 전문가들만 아는 자기 분야의 논증들 때문에 호기심이 이끄는 연구를 떠나 형식화로 옮겨 왔다고 설명했습니다. "Lean은 속일 수 없다. 이것은 아주 일찍 배우게 된다."⁹

자신의 프로젝트에 대해서는 이렇게 씁니다. "위 소식에 대한 순진한 반응은 내게 이제 할 일이 없다는 것이다. 그렇지 않다." Anthropic의 증명은 그가 EPSRC에 약속한 것보다 더 나아갔습니다. 그러나 그는 Mathlib에 대한 기여도 약속했고, 이 기여는 계속되고 있습니다. 또 "사람이 현대적 증명을 탐색할 수 있게 해 주는 동적 문서"도 약속했는데, 그는 Anthropic이 이런 문서를 만들 것이라고 보지 않습니다. 그는 5년 동안 100만 파운드를 받았다고 적으며, Anthropic은 그보다 더 많이 썼을지 궁금해합니다.

10월에는 Jeremy Avigad, Buzzard, 그리고 다른 형식화 연구자 다섯 명이 그의 블로그에 쓴 기고 글이 이를 더 날카롭게 표현했습니다. "성과는 인상적이지만, AI가 생성한 이 코드는 아마 지속적인 가치가 거의 없을 것이다."¹⁰ 이들이 우려하는 것은 재사용이며, Anthropic 자신의 타임라인도 그 증명이 "아직 Mathlib이 받아들일 형태가 아니다"라고 말합니다.⁴ 임페리얼 저장소는 여전히 활발하며, main 브랜치에는 10월 22일까지 Mathlib 업데이트가 올라왔습니다.¹¹

11월 12일 현재 30시간 실행에 대한 Buzzard의 공개 논평은 찾지 못했습니다. 그의 가장 최근 글은 이렇게 끝납니다. "‘Lean으로 확인했으니 참이다’라는 말은 의미가 통하게 만들 수 있다. 하지만 그러려면 ‘Lean 코드가 컴파일된다’ 이상의 일을 해야 한다."⁸

Axiom은 Stacks Project에서 무엇을 형식화했나요?#

수학을 위한 AI를 만드는 스타트업 Axiom은 발표 날짜를 2026년 11월 4일로 적었습니다.¹⁹ Proofs and Prompts는 11월 7일에 이를 목록에 올렸습니다.¹⁸ Stacks Project는 컬럼비아 대학교의 Johan de Jong이 2005년에 시작한, 대수기하학에 관한 오픈소스 참고 자료입니다. Axiom은 "약 1,600만 줄의 코드"로 "Stacks Project 전체"를 형식화했다고 말하며, 그 결과를 "지금까지 만들어진 것 가운데 가장 큰, 통합되고 재사용 가능한 형식화된 수학 라이브러리"라고 부릅니다. 이것은 Axiom 자신의 설명입니다.

저장소의 README는 sorry도 native_decide도 없고, 증명은 표준 공리 세 개만 쓰며, 라이브러리에 Lean 모듈이 약 6만 3,000개 있다고 밝힙니다.²⁰ 라이브러리는 두 층으로 나뉩니다. 사람이 Stacks Project와 대조해 확인한 코드인 StacksCore와, "AI 에이전트가 작성한" 코드로 README의 말로는 "검토가 가장 필요한" StacksFrontier입니다. Axiom은 명제의 충실성이 "다중 에이전트 감사(multi-agent auditing)를 통해 대규모로 자동 보장"되고 다른 교차 확인으로도 보장된다고 말하며,¹⁹ 에이전트들이 원 자료에서 국소적으로 다듬어야 할 명제 수십 개를 찾았다고 말합니다. 외부 검토는 아직 찾지 못했습니다.

이것은 새 증명에 가져다 쓰도록 만든 라이브러리이며, Axiom의 베유 추측(Weil conjectures) 형식화가 이미 이것을 바탕으로 합니다. Axiom은 de Jong이 10월 21일, 당분간 AI가 생성한 댓글과 풀 리퀘스트를 원래의 Stacks Project에 보내지 말아 달라고 요청했다고 적습니다.¹⁹ 9월에 Buzzard는 한 독자에게 Stacks 형식화가 "아마 지금도 가능하겠지만 오늘날에는 비용이 크다"고, 그것을 Mathlib에 넣는 일은 "또 다른 이야기"라고 말한 바 있습니다.⁷ Axiom의 유한 단순군 분류 형식화는 앞서 유한 단순군 분류 정리의 Lean 형식화에서 다뤘습니다.

임페리얼의 Langlands Lab은 무엇인가요?#

임페리얼 칼리지 런던은 2026년 10월 27일 Langlands Lab을 발표했습니다.²¹ Proofs and Prompts는 11월 4일에 이를 목록에 올렸습니다.¹⁸ 이 연구실은 XTX Markets가 낸 500만 파운드의 지원금으로 운영되며 Buzzard가 이끕니다. 연구의 초점은 랭글랜즈 프로그램(Langlands program)으로, 임페리얼은 이를 여러 분야, 특히 정수론과 해석학 사이의 연결을 밝히려는 노력이라고 설명합니다. 목표는 Lean으로 검증된 새로운 결과, 그 결과를 이해하기 쉽게 풀어 쓴 논문, 그리고 증명을 따라가며 공부할 수 있는 무료 대화형 도구를 내놓는 것입니다.

지원금은 2027년부터 4년 동안 박사과정 학생 5명과 박사후연구원 3명을 지원합니다. 학생들은 "자신이 연구하는 수학을 깊이 이해해야 하며, 연구 결과물에 책임을 지기 전에 AI의 도움 없이 자신의 결과를 설명하고 방어해야 한다". Buzzard의 말도 인용되어 있습니다. "AI는 수학 연구를 한다는 것의 의미를 바꾸고 있으며, 우리는 다음 세대 수학자를 어떻게 길러 낼지 다시 생각해야 합니다."

검증하기 어려운 AI 생성 증명에 이것이 왜 중요한가요?#

Anthropic이 직접 이유를 듭니다. 형식화는 수학자들이 결과에 확신을 갖는 데 도움이 되며, "AI 모델이 사람이 검증하기 어려운 결과를 만들어 낼 때 이것은 더욱 중요하다".¹ 페르마의 마지막 정리가 깔끔한 시험대가 되는 것은 아무도 이 정리를 의심하지 않았기 때문입니다. 올바른 명제는 짧고 잘 알려져 있으므로, 틀린 명제라면 쉽게 알아챌 것입니다.

AI가 생성한 새로운 결과는 더 어렵습니다. Buzzard는 Lean 코드가 딸린 OpenAI 정리 290개 가운데 "약 38개는 Lean 코드가 논문의 주 정리를 증명하기는커녕 진술하지도 않는다"고 보고합니다.⁸ Axiom의 유한 단순군 분류의 경우 명제가 AI가 작성한 라이브러리 속 약 5,600줄의 정의에 기대고 있으며, 그는 산재군(sporadic group)의 정의를 꼼꼼히 확인했다고 말하는 사람을 만나 본 적이 없다고 합니다. 같은 질문을 애런슨-앰바이니스 추측(Aaronson-Ambainis)을 AI가 증명했을까와 OpenAI의 양-밀스 증명에서도 살펴봤습니다.

형식화가 빨라지면 형식 증명이 붙은 채 도착하는 AI 생성 주장도 늘어납니다. 그 뒤에 따라야 할 확인에는 여전히 사람이, 그리고 이 정도 규모라면 큰 기계가 필요합니다.

짧은 역사: Wiles에서 Wiedijk 목록의 마지막 정리까지#

날짜	사건
1637년경	페르마가 자신이 가진 디오판토스의 『아리스메티카(Arithmetica)』 여백에 이 주장을 적음3
1993년 6월	Wiles가 뉴턴 연구소(Newton Institute)에서 강연 세 번에 걸쳐 증명을 발표. 확인 작업 두 달째에 빈틈이 발견됨
1993~94년	Wiles가 약 1년 동안, 처음에는 혼자, 나중에는 Richard Taylor와 함께 빈틈을 메움
1995년 5월	Wiles의 논문과 Taylor–Wiles 논문이 Annals of Mathematics 141권에 실림14
1999년	Wiedijk가 형식화 여부를 추적하는 "100대(top 100)" 정리 목록이 만들어진 해13
2023년 11월	Buzzard가 GitHub에 임페리얼 FLT 저장소를 엶11
2024년 10월	그의 EPSRC 연구비 지원이 시작됨. 2029년 9월까지12
2026년 8월 7~17일	Prove2Me에서 Anthropic의 첫 실행
2026년 9월 4일	Anthropic이 첫 완전한 형식화를 발표. Buzzard: "Anthropic이 나보다 먼저 해냈다"
2026년 10월 27일	임페리얼이 Langlands Lab을 발표
2026년 11월 4일	Axiom이 Stacks Project 형식화를 공개
2026년 11월 9일	Anthropic이 에이전트 1,000개, 30시간 실행을 보고

연구 기록에 주는 의미#

AI가 쓴 형식 증명을 믿기 전에 독자에게는 다음 정보가 필요합니다. 누가 형식적 명제를 썼고 누가 그것을 비형식적 명제와 대조해 확인했는지, 팀이 보고하는 바로는 어떤 모델을 썼고 사람이 그 모델에 무엇을 제공했는지, 코드의 어느 버전을 어떤 Lean과 Mathlib 버전에서 확인했는지, 그리고 어떤 확인을 언제 누가 실행했는지입니다. 9월 증명에 대해서는 Anthropic의 저장소와 글이 이 가운데 대부분에 답합니다. 30시간 실행에 대해서는 대부분이 아직 열려 있습니다.

AI의 도움을 받은 결과를 발표하는 연구자도 같은 정보를 날짜와 서명을 붙여, 코드 링크와 함께 적어 둘 수 있습니다. Papex에서는 AI 앱이 그런 초안을 준비할 수 있고, 연구자가 이를 검토하고 서명합니다(AI 앱이 Papex와 함께 작동하는 방식(영어)). 그런 기록은 수학이 옳은지에 대해서는 아무것도 말하지 않습니다. 그 판단은 Lean과 명제를 읽는 사람들의 몫으로 남습니다.

열린 쟁점을 해소할 수 있는 것은 30시간 실행 코드의 공개, 그 코드에 대한 comparator와 두 번째 커널 실행, Anthropic 밖의 누군가가 하는 명제 확인, 그리고 완료율 수치 뒤에 있는 가중치입니다.

이해관계에 관해 밝힙니다. 이 글은 Anthropic의 Claude 모델에 관해 다루며, Claude로 초안을 작성했습니다. 독자는 이 점을 염두에 두고 이 글을 판단하고, 아래 출처를 확인하시기 바랍니다.

출처#

1. Introducing Claude Fable 5.2 and Claude Mythos 5.2 (Anthropic, 2026년 11월 9일, 11월 11일 수정), 2026년 11월 12일 확인 ↩ a b c d
2. Barry Zhang, Tianyi Peng, Elle Najt, Keller Scholl, Lance Martin, Safely scaling multi-agent teams with Claude Fable 5.2 (claude.dev, 2026년 11월 9일), 2026년 11월 12일 확인 ↩ a b c
3. Formalizing Fermat's Last Theorem (Anthropic, 2026년 9월 4일), 2026년 11월 12일 확인 ↩ a b c
4. Formalizing Fermat's Last Theorem in Lean: a timeline and selected excerpts from Claude's reasoning (Anthropic, 17쪽), 2026년 11월 12일 확인 ↩ a b c d
5. anthropics/fermats-last-theorem: README, FinalCheck.lean, 커밋 aa2d8b34 (GitHub, 2026년 9월 24일 마지막 변경), 2026년 11월 12일 확인 ↩ a b c d e
6. anthropics/fermats-last-theorem, formalization.yaml (GitHub), 2026년 11월 12일 확인 ↩
7. Kevin Buzzard, FLT: Anthropic has beaten me to it, 댓글 포함 (Xena, 2026년 9월 4일), 2026년 11월 12일 확인 ↩ a b c d e
8. Kevin Buzzard, "…and the proof is checked in Lean" (Xena, 2026년 11월 12일), 2026년 11월 12일 확인 ↩ a b c d e f
9. Kevin Buzzard, To grieve, or not to grieve? (Xena, 2026년 10월 1일), 2026년 11월 12일 확인 ↩
10. Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash, Adam Topaz, How to Formalize All of Mathematics (Xena, 2026년 10월 16일), 2026년 11월 12일 확인 ↩
11. ImperialCollegeLondon/FLT: README와 커밋 이력 (GitHub), 2026년 11월 12일 확인 ↩ a b c
12. ImperialCollegeLondon/FLT, GENERAL.md (GitHub), 2026년 11월 12일 확인 ↩ a b
13. Freek Wiedijk, Formalizing 100 Theorems (라드바우드 대학교, 2026년 11월 1일 마지막 수정), 2026년 11월 12일 확인 ↩ a b
14. Andrew Wiles, Modular elliptic curves and Fermat's Last Theorem, Annals of Mathematics 141 (1995), 3호, 2026년 11월 12일 확인 ↩
15. Shuze Chen 외 공저자 4명, Prove2Me: An Open Collaborative Platform for Scaling Math Formalization, arXiv:2608.28433, 2026년 11월 12일 확인 ↩
16. leanprover/comparator: README (GitHub), 2026년 11월 12일 확인 ↩
17. anthropics/formal-math: README (GitHub), 2026년 11월 12일 확인 ↩
18. Newsfeed, 2026년 11월 4일, 7일, 10일 항목 (Proofs and Prompts), 2026년 11월 12일 확인 ↩ a b c
19. The Stacks Project, formalized in Lean (Axiom, 2026년 11월 4일), 2026년 11월 12일 확인 ↩ a b c
20. AxiomMath/Stacks: README (GitHub), 2026년 11월 12일 확인 ↩
21. £5 million grant to establish new laboratory for AI-assisted mathematics at Imperial (임페리얼 칼리지 런던, 2026년 10월 27일), 2026년 11월 12일 확인 ↩
22. Lean 커뮤니티 Zulip 아카이브, 색인 (2026년 2월 28일 마지막 갱신), 2026년 11월 12일 확인 ↩
23. Introducing Claude Fable 5.2 and Claude Mythos 5.2, 처음 게시된 버전 (인터넷 아카이브 사본, 2026년 11월 9일 18:57 UTC), 2026년 11월 12일 확인 ↩