클로드가 11일 만에 페르마의 마지막 정리를 기계에 넘겼습니다 — 1,300만 줄과 29,500개의 정리

1637년, 피에르 드 페르마는 읽던 책의 여백에 한 줄을 적었습니다. 증명을 찾았는데 여백이 좁아 옮기지 못하겠다는 말이었습니다. 그 한 줄이 358년을 버텼습니다.

1994년 앤드루 와일즈가 마침내 증명했습니다. 다만 그 증명은 사람이 쓰고 사람이 읽고 사람이 검토한 것이었습니다. 100쪽이 넘는 논문을 이해할 수 있는 사람은 세계에 많지 않았고, 그래서 검증은 늘 신뢰의 문제였습니다.

2026년 9월 4일, 앤트로픽이 그 증명을 기계가 한 줄씩 검사할 수 있는 형태로 옮겼다고 발표했습니다. 클로드가 11일 동안 대체로 혼자 일했고, 1,300만 줄의 코드가 나왔습니다. 수학자들이 수 년은 걸릴 거라고 보던 작업입니다.

11일 만에 끝난 358년

앤트로픽이 공개한 것은 새로운 수학이 아닙니다. 와일즈가 이미 증명한 정리를 기계가 검증할 수 있는 언어로 옮긴 것입니다. 수학에서는 이 작업을 형식화라고 부릅니다.

옮기는 일이라고 하면 단순 번역처럼 들리지만 그렇지 않습니다. 사람이 쓴 증명에는 생략된 단계가 아주 많습니다. 사람끼리는 그 생략을 알아서 채워 읽지만, 기계는 채워 주지 않습니다. 생략된 자리를 전부 명시적으로 메워야 합니다.

그래서 형식화는 원래 증명보다 훨씬 길어집니다. 이번에 나온 1,300만 줄이라는 숫자가 그 팽창의 크기입니다.

페르마가 여백에 적은 한 줄

페르마의 마지막 정리는 문장만 보면 간단합니다. n이 2보다 큰 자연수일 때, 세 자연수의 n제곱 사이에 덧셈이 성립하는 경우는 없다는 이야기입니다.

중학교 수준의 표현으로 적을 수 있는 문장인데, 증명에는 358년이 걸렸습니다. 수학에서 문장의 길이와 증명의 난이도가 따로 논다는 것을 보여 주는 대표 사례입니다.

페르마 본인이 정말 증명을 갖고 있었는지는 지금도 아무도 모릅니다. 와일즈가 쓴 도구들은 20세기에야 만들어진 것이라, 17세기의 페르마가 같은 길을 갔을 리는 없습니다.

와일즈의 1994년 증명, 그리고 남은 숙제

와일즈는 페르마의 정리를 직접 공격하지 않았습니다. 타원곡선과 모듈러 형식이라는 전혀 다른 두 영역을 잇는 다리를 세웠고, 그 다리가 서면 페르마의 정리가 따라 나온다는 구조를 이용했습니다.

이 방식 덕분에 증명은 성공했지만, 대신 증명이 현대 정수론의 아주 깊은 곳까지 내려가게 됐습니다. 논문을 처음부터 끝까지 읽고 검증할 수 있는 사람은 극소수였습니다.

수학계는 이 증명을 받아들였습니다. 다만 그 수용은 소수의 전문가가 오랜 시간에 걸쳐 검토했다는 사실에 기대고 있었습니다. 기계가 검사한 것은 아니었습니다.

형식화란 무엇인가 — 사람이 읽는 증명과 기계가 검사하는 증명

형식화는 수학 증명을 컴퓨터가 이해하고 검사할 수 있는 형식 언어로 다시 쓰는 작업입니다. 결과물은 사람이 읽기엔 지독하게 장황하지만, 기계는 한 줄도 봐주지 않고 전부 검사합니다.

한 줄이라도 논리가 어긋나면 검사기가 통과시키지 않습니다. 그래서 형식화가 끝난 증명은 사람의 판단이 아니라 기계의 검사로 뒷받침됩니다.

신뢰의 성격이 바뀝니다. 그전에는 이 사람이 검토했으니 맞을 것이라는 신뢰였다면, 형식화 이후에는 검사기가 통과시켰으니 논리적으로 빈 곳이 없다는 신뢰가 됩니다.

Lean 4는 어떤 도구인가

이번 작업에 쓰인 도구는 Lean 4입니다. 증명 보조기라고 부르는 소프트웨어로, 수학 명제와 그 증명을 프로그램처럼 적으면 타당한지 검사해 줍니다.

Lean에는 Mathlib이라는 공용 수학 라이브러리가 있습니다. 전 세계 자원자들이 여러 해에 걸쳐 기본 정리들을 형식화해 쌓아 온 결과물입니다. 새 증명은 이 라이브러리 위에 올라갑니다.

Lean 커뮤니티는 취미 프로젝트가 아닙니다. 대학 연구자와 학생, 산업계 개발자가 함께 붙어 있고, 형식화된 수학의 표준 인프라 자리를 놓고 실질적으로 앞서 있습니다.

수학자들이 수 년이라고 봤던 작업

와일즈 증명의 형식화가 언젠가 가능하리라는 데는 대체로 합의가 있었습니다. 문제는 시간이었습니다.

임페리얼칼리지런던의 케빈 버자드가 이끄는 프로젝트는 2024년에 시작해 2029년까지 지원을 받고 있었습니다. 5년 규모의 일정입니다. 이 숫자가 수학계가 잡고 있던 감각을 보여 줍니다.

그 일정표 위에 11일이라는 숫자가 얹혔습니다. 감각의 차이가 두 자릿수를 넘습니다.

앤트로픽이 공개한 것 — 1,300만 줄

앤트로픽은 결과물과 함께 기술 보고서를 냈습니다. 핵심 수치는 Lean 코드 약 1,300만 줄입니다.

줄 수가 곧 품질은 아닙니다. 형식화 코드는 반복이 많고 기계적으로 생성되는 부분도 많아서, 사람이 손으로 쓴 코드와 같은 잣대로 비교하기 어렵습니다.

그래도 규모 자체는 의미가 있습니다. 사람이 이만큼을 손으로 채우려면 몇 명이 몇 해를 붙어야 하는지 계산해 보면, 왜 5년 일정이었는지가 이해됩니다.

30,300개의 정리, 그중 29,500개

작업 과정에서 증명된 정리는 30,300개입니다. 이 가운데 29,500개가 최종 증명에 실제로 쓰였습니다.

두 숫자의 차이인 800개가량은 중간에 만들었다가 결국 경로에서 빠진 것들입니다. 사람이 증명을 쓸 때 버려지는 초안과 같은 성격입니다.

거꾸로 보면 만든 것의 97퍼센트가 최종본에 남았다는 뜻이기도 합니다. 무작정 쏟아 내고 나중에 고른 것이 아니라, 경로를 잡아 가며 채웠다는 정황입니다.

60억 개의 출력 토큰이 뜻하는 것

이 작업에 들어간 출력 토큰은 약 60억 개로 보고됐습니다. 모델이 생성한 글자 수의 규모를 재는 단위입니다.

60억 토큰은 개인이 다룰 수 있는 규모가 아닙니다. 대규모 추론 자원을 11일간 쉬지 않고 돌려야 나오는 숫자입니다.

이 지점이 이번 성과의 성격을 정합니다. 새 알고리즘의 승리라기보다, 검증 가능한 문제에 대량의 계산을 쏟아부었을 때 어디까지 가는지를 보여 준 사례에 가깝습니다.

Mathlib의 다섯 배라는 규모 감각

앤트로픽은 이번 결과물이 Lean의 주 라이브러리보다 다섯 배 크다고 밝혔습니다. Mathlib은 수많은 사람이 여러 해 동안 쌓아 온 공용 자산입니다.

한 문제를 푸는 데 만든 코드가 공용 라이브러리 전체의 다섯 배라는 것은, 형식화 코드가 얼마나 부풀어 오르는지를 보여 줍니다.

동시에 재사용성 문제도 남깁니다. 공용 라이브러리는 다른 사람이 계속 쓰라고 다듬어 놓은 것이고, 한 증명을 위해 생성된 방대한 코드는 그만큼 정돈돼 있지 않을 가능성이 큽니다.

첫 시도는 실패했습니다

앤트로픽은 처음부터 성공한 것이 아닙니다. 와일즈 증명을 형식화하려던 초기 시도는 실패했다고 스스로 밝혔습니다.

이 대목이 오히려 정보가 많습니다. 모델의 능력만으로 뚫린 것이 아니라, 작업을 담을 구조가 있어야 했다는 뜻이기 때문입니다.

실패를 공개한 기술 보고서는 성공만 적은 보도자료보다 읽을 가치가 큽니다. 어디서 막혔고 무엇을 바꿨는지가 다음 사람에게 실제로 쓸모 있는 정보입니다.

Prove2Me가 바꾼 것

돌파구는 Prove2Me라는 오픈소스 도구에 접근권을 주면서 열렸습니다. 컬럼비아대학의 톈이 펑과 협력자들이 만든 협업 형식화 플랫폼입니다.

이 플랫폼은 큰 형식화 작업을 잘게 쪼개고, 조각들을 나눠 맡기고, 결과를 다시 합치는 일을 돕습니다. 사람 여럿이 협업하라고 만든 구조인데, 그 구조가 모델 여럿에게도 맞았습니다.

주목할 점은 이 도구가 앤트로픽 것이 아니라는 사실입니다. 외부 연구 커뮤니티가 만들어 둔 공용 인프라가 결정적인 자리를 차지했습니다.

수십 개 에이전트가 나눠 맡는 방식

이번 작업은 클로드 한 개가 처음부터 끝까지 쓴 것이 아닙니다. 수십 개의 에이전트가 Prove2Me 위에서 조각을 나눠 맡았습니다.

형식화는 이 방식과 잘 맞습니다. 각 조각의 정답 여부를 검사기가 즉시 판정해 주기 때문입니다. 맞으면 통과, 틀리면 반려라는 신호가 자동으로 돌아옵니다.

채점자가 붙어 있는 문제에서 병렬 시도가 강하다는 것은 새로운 발견이 아닙니다. 다만 그 원리가 현대 정수론의 최상단까지 올라갔다는 것이 이번 사건입니다.

대체로 자율적이라는 표현의 무게

앤트로픽은 클로드가 대체로 자율적으로 일했다고 표현했습니다. 완전히 자율적이라고는 하지 않았습니다.

이 표현의 여백이 넓습니다. 사람이 어느 지점에서 얼마나 개입했는지, 막혔을 때 방향을 잡아 준 것이 누구인지에 따라 성과의 성격이 달라집니다.

기술 보고서를 읽는 사람들이 가장 먼저 확인하는 부분도 여기입니다. 보도자료의 한 문장보다 보고서의 개입 기록이 훨씬 많은 것을 말해 줍니다.

케빈 버자드와 임페리얼칼리지 FLT 프로젝트

이 분야에서 가장 오래 붙어 있던 사람은 임페리얼칼리지런던의 케빈 버자드입니다. 2024년부터 페르마의 마지막 정리 형식화 프로젝트를 이끌어 왔습니다.

영국 공학물리과학연구위원회의 지원을 2029년까지 받는 장기 프로젝트이고, 공개 저장소에서 여러 참여자와 함께 진행돼 왔습니다.

앤트로픽의 결과물은 이 프로젝트의 조각들을 가져다 썼습니다. 백지에서 시작한 것이 아닙니다.

flt-regular — 이미 쌓여 있던 벽돌

버자드 프로젝트만이 아닙니다. 정규 소수에 대한 페르마의 마지막 정리를 형식화한 flt-regular 프로젝트의 결과물도 활용됐습니다.

정규 소수의 경우는 19세기에 쿠머가 다룬 영역으로, 전체 정리의 일부에 해당합니다. 그 일부가 이미 Lean으로 옮겨져 있었습니다.

형식화된 수학은 이렇게 쌓입니다. 한 번 옮겨 놓은 것은 다음 사람이 그대로 딛고 올라섭니다. 이번 성과도 그 축적 위에 서 있습니다.

버자드의 평가와 그 안의 단서

버자드는 결과물을 검토하고 대단한 자동형식화 성과라고 평했습니다. 이 분야에서 가장 권위 있는 사람의 인정입니다.

다만 그가 고른 단어는 자동형식화입니다. 새로운 수학을 발견했다는 말도, 증명을 해냈다는 말도 아닙니다. 이미 있는 증명을 기계 언어로 옮기는 작업을 자동화했다는 평가입니다.

칭찬과 범위 지정이 한 문장 안에 같이 들어 있습니다. 이 구분이 이번 뉴스를 읽는 가장 정확한 각도입니다.

Lean 커뮤니티가 클로드를 언급하지 않은 이유

흥미로운 대목이 있습니다. Lean 진영에서 이 형식화를 소개하는 문서는 버자드 프로젝트를 주체로 놓고, 클로드를 언급하지 않는 서술을 택했습니다.

악의로 읽을 일은 아닙니다. 그쪽 관점에서 이 형식화는 여러 해 동안 쌓아 온 커뮤니티 작업의 결말이고, 마지막 구간에 대량의 계산이 투입된 것으로 보이기 때문입니다.

같은 사건을 두고 두 서술이 병존합니다. 한쪽은 11일을 강조하고 다른 쪽은 5년을 강조합니다. 둘 다 사실입니다.

공을 누구에게 돌릴 것인가

공로 배분은 감정 문제가 아니라 구조 문제입니다. 어디까지가 축적이고 어디부터가 이번 기여인지를 나누는 일입니다.

이번 사례에서 축적은 Mathlib, 버자드 프로젝트, flt-regular, Prove2Me입니다. 새로 투입된 것은 모델의 생성 능력과 대규모 계산 자원입니다.

둘 중 하나만 있었으면 결과가 나오지 않았을 겁니다. 이 사실을 인정하는 것이 다음 협업을 가능하게 합니다.

프리크 비데이크의 100문제, 마지막 한 칸

수학자 프리크 비데이크는 형식화의 진척을 재기 위해 100개의 대표 정리 목록을 만들어 두었습니다. 20년 넘게 형식화 진영의 비공식 계기판 역할을 해 왔습니다.

페르마의 마지막 정리는 그 목록에서 마지막까지 비어 있던 칸이었습니다. 이번 작업으로 100개가 모두 채워졌습니다.

한 시대의 벤치마크가 끝났다는 뜻입니다. 다음 계기판이 무엇이 될지는 아직 정해지지 않았습니다.

기계 검증이 주는 신뢰의 성격

기계 검증은 증명이 아름다운지, 통찰이 있는지를 말해 주지 않습니다. 논리적으로 빈 곳이 없는지만 말해 줍니다.

그런데 수학에서 이 보증은 생각보다 큽니다. 사람이 검토한 증명에서 나중에 구멍이 발견된 사례는 드물지 않습니다. 와일즈의 첫 발표에도 결함이 있어 1년 넘게 메워야 했습니다.

검사기가 통과시킨 증명은 그 종류의 사고에서 자유롭습니다. 대신 검사기 자체와 그 아래 깔린 정의가 옳다는 전제가 필요합니다.

형식화가 열어 두는 다음 문

형식화된 정리는 다음 사람이 그냥 가져다 씁니다. 새 증명을 쌓을 때 이미 검증된 벽돌을 신뢰하고 올라갈 수 있습니다.

이번 결과물이 정돈돼 공용 라이브러리로 흡수되면, 정수론의 상당 구간이 기계 검증된 기반 위로 올라갑니다. 그 자체가 다음 연구의 인프라가 됩니다.

반대로 흡수되지 못하고 한 번 쓰인 채 남으면, 1,300만 줄은 기록으로만 남습니다. 앞으로 몇 달이 이 갈림길입니다.

실제 사례 — 수학 밖에서 같은 구조가 쓰이는 곳

검사기가 즉시 정답을 판정해 주는 구조는 수학에만 있는 것이 아닙니다. 소프트웨어 개발에서 테스트 코드가 정확히 그 역할을 합니다.

테스트가 촘촘히 깔린 저장소에서는 AI가 코드를 고치고 바로 채점받을 수 있습니다. 반대로 테스트가 없는 저장소에서는 고쳤는지 망쳤는지를 사람이 일일이 확인해야 합니다.

이번 뉴스에서 개발자가 가져갈 교훈은 모델을 바꾸는 것이 아니라 채점자를 먼저 만드는 것입니다. 형식화가 뚫린 이유가 정확히 그것이었습니다.

저시력 사용자에게 이 뉴스가 닿는 지점

이 소식은 언뜻 접근성과 멀어 보입니다. 하지만 검증 가능한 작업을 기계가 대신 채운다는 구조는 접근성 도구가 오래 기다려 온 형태입니다.

화면 낭독기 호환성이나 대비 기준 준수 같은 항목은 기계가 판정할 수 있습니다. 판정이 자동이면 수정도 자동으로 밀어붙일 수 있습니다.

규격이 명확한 영역부터 AI가 실질적으로 일을 끝내기 시작한다는 신호로 읽으면, 이 뉴스는 접근성과 곧장 이어집니다.

핵심 정리

2026년 9월 4일 앤트로픽이 페르마의 마지막 정리를 Lean 4로 형식화한 결과물을 공개했습니다. 클로드가 11일간 대체로 자율적으로 작업했습니다.

규모는 Lean 코드 약 1,300만 줄, 증명된 정리 30,300개, 그중 최종 사용 29,500개, 출력 토큰 약 60억 개입니다. Lean 주 라이브러리의 다섯 배 규모입니다.

첫 시도는 실패했고, 오픈소스 협업 플랫폼 Prove2Me에 접근권을 준 뒤에 뚫렸습니다. 임페리얼칼리지 FLT 프로젝트와 flt-regular의 결과물도 활용됐습니다.

케빈 버자드는 대단한 자동형식화 성과라고 평했지만, 새 수학의 발견이 아니라 기존 증명의 기계 번역을 자동화한 것이라는 범위도 함께 지정했습니다. 이 형식화로 프리크 비데이크의 100문제 목록이 20여 년 만에 모두 채워졌습니다.

참고하실 만한 것

기술 보고서는 앤트로픽이 PDF로 공개해 두었습니다. 어디서 막혔고 무엇을 바꿨는지가 보도자료보다 훨씬 자세합니다.

형식화가 처음이라면 Lean 공식 사이트의 FLT 사례 소개가 진입점으로 좋습니다. Mathlib이 무엇이고 왜 중요한지가 함께 정리돼 있습니다.

공로 배분을 둘러싼 논의가 궁금하시면 케빈 버자드의 블로그 글을 직접 읽어 보시길 권합니다. 당사자가 쓴 한 편이 기사 열 편보다 정확합니다.

출처

• Anthropic — Formalizing Fermat's Last Theorem
• Anthropic 기술 보고서 (PDF)
• SiliconANGLE — Anthropic uses Claude to formalize proof of Fermat's Last Theorem
• Xena Project (Kevin Buzzard) — FLT: Anthropic has beaten me to it
• Lean Lang — Formalizing Fermat's Last Theorem in Lean
• AI Weekly — Anthropic's Claude Formalizes Fermat's Last Theorem in Lean
• Crypto Briefing — Claude helps complete first formalized proof of Fermat's Last Theorem
• arXiv — A complete formalization of Fermat's Last Theorem for regular primes in Lean

협업문의 : kuroicode@gmail.com
블로그 : https://blog.svil.dev/
홈페이지 : https://svil.dev/