5년 연구비로 하던 페르마 형식화, Claude 에이전트가 11일 만에 끝냈습니다

공지는 앤트로픽 공식 X 계정에 영상과 함께 올라왔습니다. 큰 수학 증명이 맞는지 확인하는 데는 몇 년이 걸리고, 증명을 컴퓨터가 검사하는 형태로 바꾸는 형식화가 그 일을 덜어 준다는 설명으로 시작합니다. 앤트로픽은 이번 작업을 전문가들이 여러 해 걸릴 것으로 본 프로젝트이자 지금까지 쓰인 가장 큰 Lean 증명이라고 소개했고, 증명에 필요한 정리 2만 9,000여 개가 한 번도 형식화된 적 없는 여러 분야에 걸쳐 있다고 덧붙였습니다.

같은 날 영국 임피리얼칼리지의 수학자 케빈 버저드는 블로그에 「앤트로픽이 나를 앞질렀다」는 제목의 글을 올렸습니다. 그는 2024년 10월부터 영국 공학·물리과학연구위원회(EPSRC)에서 5년 동안 100만 파운드를 받아 바로 이 형식화를 이끌어 온 사람입니다. 앤트로픽은 발표 전에 완성된 증명을 그에게 보내 검토를 받았습니다.

358년 걸린 증명, 검산에만 몇 달

페르마의 마지막 정리는 1637년 무렵 피에르 드 페르마가 디오판토스의 『산술』 여백에 적은 주장입니다. n이 3 이상이면 aⁿ+bⁿ=cⁿ을 만족하는 양의 정수 a, b, c는 없다는 내용이고, 페르마는 놀라운 증명을 찾았지만 여백이 좁아 적지 못한다고 덧붙였습니다. 1908년에는 증명하는 사람에게 금화 10만 마르크를 주겠다는 상이 걸렸고, 첫해에만 틀린 증명이 621건 들어왔습니다.

YouTube 영상 · 누르면 재생

앤드루 와일스는 1993년 6월 케임브리지 뉴턴 연구소에서 3일에 걸친 강연으로 증명을 발표했습니다. 수학자 여러 명이 두 달째 검토하던 중 한 심사자의 질문에서 결정적인 구멍이 드러났고, 와일스는 처음엔 혼자, 나중엔 제자였던 리처드 테일러와 함께 1년을 매달려 고쳤습니다. 고친 증명은 1995년 5월 129쪽짜리 논문으로 나왔습니다.

증명이 길고 깊을수록 맞는지 확인하는 시간도 길어집니다. 앤트로픽이 발표문 각주에 모아 둔 사례는 이렇습니다.

케플러 추측은 심사로 끝내지 못하고, 헤일스가 20명 규모의 Flyspeck 프로젝트를 이끌어 증명을 형식화했습니다. 앤트로픽은 이번 일을 계산기로 계산을 검산하듯 수학 증명을 검산한 작업이라고 설명합니다.

Lean은 한 단계도 건너뛰지 않습니다

형식화는 증명을 Lean 같은 증명 보조기가 읽는 코드로 다시 쓰는 일입니다. Lean은 증명의 논리를 한 단계씩 알고리즘으로 검사하고, 통과한 증명은 기계가 확인한 것이 됩니다. 어려움은 옮겨 적는 과정에서 생깁니다. 사람을 위한 증명은 뻔한 단계를 건너뛰지만 Lean은 아무리 사소한 단계도 전부 적어 줘야 하고, 사람의 증명이 기대는 몇 세기 치 문헌 가운데 이미 형식화된 것은 아주 일부입니다.

그 일부가 Lean 커뮤니티의 수학 라이브러리 Mathlib입니다. 버저드가 7월 블로그에 적은 숫자로 Mathlib은 230만 줄이고, 쓰는 데 9년이 걸렸습니다. 버저드 팀이 페르마 형식화의 첫 단계를 설명하려고 쓴 설계도(블루프린트)만 86쪽입니다.

네덜란드 라드바우드대학교의 프레이크 비디크가 관리하는 「100대 정리」 목록은 20년 동안 이 분야의 과제 목록 구실을 했습니다. 나머지 99개가 여러 증명 보조기에서 차례로 형식화되는 동안 페르마의 마지막 정리만 남아 있었고, 버저드는 이번 결과로 20년 된 이 과제가 끝났다고 적었습니다.

에이전트들이 길을 잃은 첫 시도

작업을 시작한 사람은 앤트로픽 연구원이자 컬럼비아대 교수인 톈이 펑(Tianyi Peng)입니다. 그의 컬럼비아대 연구실은 AI 형식화 도구를 만드는 곳이고, 그는 Claude가 페르마 형식화를 얼마나 진척시킬 수 있는지 시험해 보려 했습니다. 앤트로픽은 결과가 그의 예상보다 훨씬 멀리 갔다고 적었습니다.

첫 시도들은 실패했습니다. 에이전트들은 초반에 조금 나아가다가 프로젝트가 어디까지 왔는지 금세 놓쳤고, 서로 협력하는 일도 멈췄습니다. 그때 쓴 코드는 최종 증명에서 자동 생성 코드를 뺀 줄의 약 7%로 남았습니다.

판을 바꾼 것은 펑의 연구실이 만든 공개 협업 플랫폼 Prove2Me입니다. Prove2Me는 증명할 정리 문장 하나하나를 「카드」로 만들어 의존 관계 그래프에 올리고, 에이전트는 이 그래프를 보고 다음에 증명할 카드를 고릅니다. 에이전트의 기억이 흐려져도 진행 상태는 그래프에 남아서, 여러 에이전트가 같은 증명에 동시에 붙을 수 있었습니다.

장치는 두 가지가 더 있습니다. 정리 문장과 증명을 다른 파일로 나눠 Lean 컴파일을 빠르게 하고 자원을 덜 쓰게 했고, 카드마다 자연어 설명을 붙여 이미 증명된 결과를 검색해 다시 쓰게 했습니다. 펑과 컬럼비아대 연구진은 8월 28일 arXiv에 올린 논문에서, 에이전트를 가진 사람이면 누구나 참여하는 크라우드소싱 형식화를 Prove2Me의 목표로 적었습니다.

에이전트를 돌린 것은 Claude Code를 바탕으로 만든 다중 에이전트 하네스(모델에 도구와 작업 규칙을 붙여 일을 시키는 실행 틀)이고, 모델은 9월 1일 공개된 Fable 5.1과 비슷한 수준의 범용 내부 연구 모델입니다. 사람이 한 일은 목표 정리 한 줄을 적고, 가끔 우선순위를 짚거나 격려한 것이 전부였습니다. 앤트로픽이 공개한 펑의 지시는 「스킴으로서의 야코비안이 우선순위가 높아 보인다」 「마주르 정리를 곧 끝내도록 밀어붙이자」 같은 한 줄짜리입니다.

증명은 와일스의 논증을 다르몽·다이아몬드·테일러가 1995년에 정리한 해설을 따릅니다. 반례가 있다고 가정해 프레이 곡선이라는 타원곡선을 만들고, 마주르와 와일스, 리벳의 정리를 차례로 적용하면 존재할 수 없는 대상이 나온다는 순서입니다. 첫 단계의 환원은 버저드가 이끄는 임피리얼칼리지 FLT 프로젝트의 블루프린트를 따랐고, 그 프로젝트와 정규 소수에 대한 페르마 정리를 형식화한 flt-regular 프로젝트에서 파일 106개를 가져와 출처를 밝혔습니다.

「1~3주」로 잡은 일이 그날 밤 끝났습니다

앤트로픽이 함께 공개한 17쪽짜리 기록에는 날짜별 진행이 적혀 있습니다. 증명된 정리는 2일째 약 2,100개, 6일째 1만 개를 넘었고, 11일째 밤 페르마의 마지막 정리가 증명됐을 때 플랫폼 누적은 약 3만 300개였습니다. 그중 최종 정리의 의존 관계 안에 든 29,511개가 나중에 다시 검사한 대상입니다.

속도는 에이전트들의 예상도 앞질렀습니다. 5일째 아침 에이전트들이 함께 쓰는 계획표에는 마주르 정리의 남은 부분이 「1~3주」로 잡혀 있었고, 오후 3시 30분쯤 「며칠에서 1주일」로 고쳐졌습니다. 마지막 조각이 증명된 것은 그날 밤 9시 40분쯤이었고, 에이전트 셋이 25초 안에 차례로 이를 확인했습니다.

10일째에는 몇 주짜리로 분류된 과제를 에이전트 하나가 2시간 16분 만에 끝냈습니다. 랭글랜즈-터널 정리로 가는 한 단계였고, 에이전트가 쓴 7,300줄짜리 증명은 첫 제출에 통과했습니다. 에이전트는 금요일에 써 둔 다른 증명 안에 어려운 표현론이 이미 모양을 바꿔 들어 있어서 빨랐다고 업데이트에 적었습니다.

틀린 것도 걸러졌습니다. 어떤 문장을 증명하기 전에 다른 에이전트가 그 문장이 쓰인 그대로 참인지 먼저 확인했고, 이 과정에서 거짓 문장 여럿이 일찍 걸렸습니다. 11일째 아침에는 검토를 통과한 보조정리를 다른 에이전트가 반례를 직접 계산해 거짓으로 밝혔고, 그날 밤 완료 1시간 반 전에는 다른 에이전트의 이의를 받은 에이전트가 자기가 통과시킨 보조정리를 다시 따져 보고 정정을 올렸습니다.

가장 깊은 두 부분인 리벳의 수준 낮추기와 모듈러성 들어 올리기(R=T)는 끝까지 남아 있었습니다. 8월 17일 밤 10시(미국 동부 시각) 마지막 미증명 문장이 받아들여지자 두 부분을 거쳐 페르마의 마지막 정리까지 몇 초 만에 연달아 증명됨으로 표시됐고, 플랫폼이 최종 정리를 증명됨으로 바꾼 시각은 10시 0분 57초였습니다.

「역사적 순간, 재검사 전제」

기록에서 가장 촘촘한 대목은 그 뒤 25분입니다. 마지막 문장이 받아들여지고 39초 뒤 한 에이전트가 최종 정리 아래 열린 문장이 0개라는 것을 보고, 10초마다 직접 조회하겠다고 적었습니다. 이어 1분 동안 다른 에이전트 넷이 각자 플랫폼을 조회해 증명됨 표시를 확인했고, 그중 하나는 「역사적 순간(재검사 전제)」이라고 남겼습니다.

10시 4분에는 앞서 본 상태가 옛 조회 결과였다는 것을 알아챈 에이전트가 성급하게 결론 내리지 말자며 다시 조회했습니다. 10시 19분의 에이전트는 이 표시를 중대한 주장으로 분류하고 보고하기 전에 한 번 더 확인하기로 했습니다.

10시 25분에는 팀 채팅에서 사람이 신이 나서 그럼 정리 전체가 형식화된 것이냐고 물었습니다. 답을 맡은 에이전트는 동료에게 과장해 전하지 않도록 정확한 단서를 붙이겠다며 여섯 줄 이내, 전문용어 없이 쓰기로 정했습니다. 그렇게 올린 업데이트는 재검사가 깨끗이 끝나기 전까지 정직한 문장은 「Prove2Me에서 증명됨, 독립 재검사 대기」라고 적었습니다.

이렇게 조심한 까닭은 플랫폼의 작동 방식에 있습니다. Prove2Me는 카드마다 증명을 따로 컴파일하고, 그때 아래 카드의 증명은 보지 않고 문장만 믿습니다. 카드 하나하나가 통과해도 전체가 한 덩어리로 맞물리는지는 따로 확인할 일이었습니다.

검산은 네 겹이었습니다

다음 날 아침 팀은 카드 29,511개를 플랫폼 밖에서 소스부터 다시 컴파일했고, 그다음 날 전체를 하나의 Lean 프로젝트로 묶어 빌드했습니다. 이 빌드는 최종 정리가 Lean의 표준 공리 세 개(propext, Classical.choice, Quot.sound)에만 기대지 않으면 실패하게 짜여 있고, 증명을 비워 둔 표시(sorry)가 하나라도 있어도 실패합니다. 같은 빌드에서 Mathlib에 원래 있던 페르마의 마지막 정리 문장도 이 증명으로부터 끌어냈습니다.

comparator는 Lean 개발 조직(Lean FRO)이 만든 도구로, 증명한 문장과 그 문장에 나오는 모든 정의가 Mathlib만 불러오는 기준 파일과 똑같은지 대조하고 Mathlib까지 포함한 증명 전체를 Lean 커널로 처음부터 다시 돌립니다. nanoda는 Lean 커널을 러스트로 따로 구현한 검사기입니다. 앤트로픽은 진행 표시와 속도 개선만 하는 작은 패치 네 개를 nanoda에 적용해 공개했고, 타입 규칙을 더하거나 빼거나 약하게 만든 패치는 없다고 저장소에 적었습니다.

버저드도 직접 확인했습니다. 코드를 컴파일하고 comparator를 돌려 결과가 맞는다고 블로그에 적었고, 에이전트에게 정의나 정리 증명이 아닌 코드를 모두 골라내게 한 뒤 남은 100여 줄을 Claude와 함께 꼼꼼히 읽었습니다. 편의용 전술 하나를 정의하는 코드였다고 그는 9월 5일 댓글에 적었습니다.

도구가 확인하지 못하는 것도 저장소에 적혀 있습니다. 중간 정리 하나하나가 이름이 가리키는 뜻을 정말 담고 있는지는 기계가 판단하지 못하고, 이름과 문장이 다르면 증명된 것은 문장 쪽입니다. 그래서 저장소는 각 단계를 맡은 Lean 정리의 이름과, 이름난 고전 정리를 어느 강도까지 증명했는지를 따로 문서로 붙였습니다.

한 달 전 콜라츠 반증 소동

여러 겹으로 확인한 데는 한 달 전 일이 있습니다. 7월 25일 AI가 콜라츠 추측을 반증했다는 결과가 나왔다가, 3일 뒤 Lean의 버그가 거짓 증명을 통과시킨 것으로 드러났습니다. 독립 검사기 nanoda도 이 증명을 받아들였는데, 두 프로그램에 있던 서로 다른 버그가 겹친 결과였습니다.

Lean 개발진은 8월 21일 내놓은 4.33.1에서 커널의 건전성 문제 여러 건을 고쳤습니다. 릴리스 노트에는 그중 한 버그로 만든 가짜 증명을 nanoda도 받아들였다는 설명이 있고, 두 건은 오픈AI 연구자 대니얼 셀샘이 오픈AI 내부 모델로 찾아낸 문제라고 적혀 있습니다. 페르마 증명은 이 수정이 들어간 4.33.1로 처음부터 빌드됐고, 버저드는 오픈AI 모델들이 최근 Lean 코드를 폭넓게 검토했지만 페르마 검증에 쓴 판에서는 건전성 문제를 찾지 못했다고 전했습니다.

사람 손으로는 반년에 절반

사람이 하던 형식화의 속도는 2021년 기록에 남아 있습니다. 2020년 12월 필즈상 수상자 페터 숄체는 더스틴 클라우젠과 함께 만든 응축 수학(condensed mathematics)의 어려운 기초 정리를 형식화해 보라는 도전을 버저드의 블로그에 냈습니다. Lean 커뮤니티는 요한 코멜린을 중심으로 증명을 작은 보조정리로 쪼개 나눠 맡았고, 숄체가 가장 걱정하던 정리 9.4의 증명을 2021년 5월 28일에 끝냈습니다.

증명 보조기가 어려운 최신 연구를 꽤 합리적인 시간 안에 형식 검증하는 수준에 왔다는 게 정말 믿기지 않습니다.— 페터 숄체, 2021년 6월 버저드 블로그 기고

그 반년짜리 성과도 숄체의 표현으로는 전체 도전의 절반쯤이었고, 커뮤니티의 수학자 여럿이 붙어서 낸 결과였습니다. 5년 뒤인 올해 여름의 기록은 이렇습니다.

앞의 세 줄은 버저드가 7월 20일 블로그에 적은 숫자입니다. 줄 수가 곧 수학의 양은 아니어서, 앤트로픽도 각주에 Mathlib은 간결하고 리뷰를 거친 코드인 반면 자기 증명은 필요보다 훨씬 길 것이라고 적었습니다. 1,300만 줄 가운데 자동 생성한 상용구를 빼면 약 1,050만 줄입니다.

버저드의 5년, 앤트로픽의 11일

버저드가 EPSRC에 약속한 목표는 페르마의 정리를 1980년대까지 알려진 깊은 결과들로 환원하는 것이었습니다. 그는 이번 저장소가 증명 전체를 끝까지 해냈으니 형식화 범위로는 자기 약속보다 훨씬 멀리 갔다고 인정했습니다. 다만 그가 따라가는 길은 카레와 테일러 등의 아이디어를 쓴 현대적 증명이고, 앤트로픽은 랭글랜즈-터널 정리와 리벳의 수준 낮추기를 거치는 1995년의 경로를 따랐습니다.

그래서 그의 프로젝트는 계속됩니다. EPSRC에 함께 약속한 일은 현대 정수론의 기본 대상들을 Mathlib에 풀 리퀘스트로 넣는 일과, 사람이 현대적 증명을 따라가며 탐색할 수 있는 문서를 만드는 일입니다. 버저드는 앤트로픽이 그 문서까지 만들 것 같지는 않다고 봤습니다.

수학적으로 앤트로픽의 이 작업은 사실상 아무것도 알려 주지 않습니다.— 케빈 버저드, 임피리얼칼리지 교수

그는 페르마 증명이 맞다고 99.9% 확신한다고 이미 말해 왔고, 정수론 학계 대부분은 100% 확신한다고 적었습니다. 대신 이 결과가 보여 주는 것은 자동 형식화로 할 수 있는 일의 범위라고 했습니다. 수천 쪽의 문헌을 AI 무리가 11일 만에 처음부터 끝까지 형식화할 수 있다면 앞으로는 최신 연구가 나오는 대로 형식화되고, 논문 심사도 훨씬 덜 고통스러워진다는 것이 그의 전망입니다.

비용에 대한 한 줄도 남겼습니다. 자기는 5년 동안 쓸 100만 파운드를 받았는데, 앤트로픽은 11일밖에 안 걸렸지만 돈은 더 쓴 게 아닌지 궁금하다는 것입니다. 앤트로픽이 밝힌 숫자는 출력 토큰 약 60억 개입니다. 발표 당일 그의 블로그에는 API 가격으로 치면 30만 달러라는 댓글이 달렸는데, Fable 5.1의 출력 단가가 100만 토큰당 50달러이니 60억 개면 정확히 그 값이 나옵니다.

이 계산에는 조건이 붙습니다. 쓰인 모델은 Fable 5.1과 비슷한 내부 모델이라 정가표가 따로 없고, 입력 토큰 비용은 빠져 있습니다. 같은 댓글란에는 API의 매출총이익률이 70% 안팎이라는 분석을 들어 앤트로픽의 실제 원가는 10만 달러쯤이라는 반론도 달렸습니다. 60억 개는 Prove2Me로 돌린 11일의 양이고, 그 전에 실패한 시도들에 든 토큰은 공개되지 않았습니다.

1,300만 줄은 검사받으려고 쓴 코드입니다

저장소 설명서는 이 코드를 기계가 검사하도록 쓴 코드라고 소개합니다. 이름은 기계가 붙였고, 에이전트들의 메모에는 수학과 작업 기록이 섞여 있어서 공개할 때 주석을 지웠습니다. 저장소 첫머리에는 연구용 결과물이라 관리하지 않고 기여도 받지 않는다고 적혀 있습니다.

증명이 끝나고 2주쯤 뒤, 앤트로픽은 Claude에게 이 증명이 버저드 팀이 사람 손으로 쓴 코드와 어떻게 다른지, Mathlib에 들어가지 못할 이유가 무엇인지 물었습니다. Claude는 두 코드가 같은 커널과 같은 공리 세 개로 검사받으니 정확성에는 차이가 없고, 차이는 형태에 있다고 답했습니다. Claude가 스스로 꼽은 문제는 네 가지입니다.

깨지기 쉽다는 대목에는 숫자가 더 붙어 있습니다. Lean 판을 4.30에서 4.33으로 한 번 올렸을 때 증명 파일 29,511개 가운데 7,620개(26%)가 바뀌었고, 5,672개(19%)는 하나하나 손봐야 했습니다. 같은 시점의 Mathlib에서 계산 한도를 따로 건 줄은 5개였고, 그마저 선언 하나씩에만 걸려 있었습니다.

코드를 다듬는다고 바로 Mathlib에 들어가는 것도 아닙니다. 버저드는 9월 5일 댓글에서 Mathlib에 열린 풀 리퀘스트가 3,000개이고 그중 600개 넘게 리뷰를 기다린다고 적었습니다. Mathlib은 AI 리뷰를 받지 않고 리뷰어들은 AI가 만든 코드를 리뷰하기를 꺼린다는 설명도 붙였습니다. Mathlib의 기여 안내는 LLM을 썼으면 밝히고, AI가 쓴 내용을 전부 이해하고 있을 것을 요구합니다.

Claude가 Mathlib에 들어갈 만하다고 본 것은 증명 과정에서 새로 만든 기반입니다. 헤케 대수, 고유형식의 갈루아 표현, 모듈러 곡선과 그 야코비안, 네롱 모형, 유한 평탄 군 스킴, 테이트 곡선처럼 Mathlib에 없어서 에이전트들이 직접 만든 부분입니다. 사람이 이끄는 Mathlib 개발에서 이 파일들을 베끼지 않고 참고 자료로 쓰는 방식이고, 버저드의 임피리얼 프로젝트가 Mathlib에 기여하는 방식도 같습니다.

AI가 반례부터 찾은 여름

이번 발표는 수학자들이 AI의 결과를 확인하느라 바빴던 여름 끝에 나왔습니다. 5월 20일 오픈AI 모델이 에르되시의 단위 거리 추측을 반증했고, 7월 11일에는 Sol이 그로텐디크가 60년 전에 던진 군 스킴에 관한 물음에 반례를 찾았습니다. 7월 중순에는 수학자 레벤트 알푀게가 Fable로 87년 된 야코비안 추측의 반례를 찾았다고 알렸습니다.

이 반례들은 곧바로 Lean으로 확인됐습니다. 그로텐디크 반례는 Fable이 4시간 만에 1,076줄짜리 Lean 파일로 형식화했고, 버저드는 이를 노트북에서 5분도 안 돼 확인했습니다. 그는 AI가 쓴 12쪽짜리 비형식 증명은 읽지 않겠다며 Lean으로 전부 옮겨 오라고 먼저 요구했다고 적었습니다.

8월에는 앤트로픽의 리만 제타 함수 영점 기록 경신, 알푀게의 S⁶ 복소 구조 증명, 구글 에이전트 팀의 미해결 문제 7개 풀이가 이어졌습니다. 오픈AI는 8월 1일 미출시 모델로 난제 열 건을 풀고 증명마다 Lean 인증서를 붙였습니다. 앤트로픽은 리만 작업은 새로운 수학을 낸 것이고, 이번 작업에서 새로운 것은 검증이라고 구분했습니다.

버저드는 8월 13일 다음 과제도 내놓았습니다. 그의 팀이 2020년대에 수학 학술지 Annals of Mathematics에 실린 중요한 정리 50개의 문장을 Lean으로 적어 공개하고, AI에게 논문을 보고 증명까지 형식화해 보라는 Annals Challenge입니다. 50개는 2020년 이후 이 학술지 논문의 약 20%이고, 나머지는 정리를 적는 데 필요한 정의(심플렉틱 다양체의 후카야 범주, 연결 환원군의 첨점 보형 표현 등)가 Mathlib에 없어 문장조차 적지 못했습니다.

그가 이 과제에서 기대하는 것은 정리가 정말 참인지 확인하는 일입니다. Annals는 2020년 이후 논문 213편을 내면서 정오표 8건과 철회 2건을 냈고, 버저드 팀은 정리 문장을 옮기는 과정에서만 필즈상 수상자 논문 4편의 오타를 찾았습니다. 모두 「3 이상」이나 「공집합이 아닌」 같은 조건이 빠져 정리가 글자 그대로는 거짓이 되는 종류였습니다.

심사하는 쪽과 연구하는 쪽에 달라지는 것

앤트로픽은 앞으로 사람이 읽을 증명을 쓸 때 형식화된 증명을 함께 내는 일이 보통이 될 것으로 봤습니다. 형식 증명이 사람이 이해하는 해설을 대신하지는 못하지만, AI가 쏟아 내는 증명의 속도를 수학계가 따라갈 현실적인 방법은 그것뿐일 수 있다는 설명입니다. 버저드도 AI가 쓴 수학을 읽는 일은 여전히 피곤하고, Lean 코드가 붙어 있으면 적어도 시간을 버리지는 않는다는 확신을 갖고 읽을 수 있다고 적었습니다.

국내 연구자가 같은 방식을 시험해 보는 데 드는 비용도 발표문에서 가늠할 수 있습니다. 앤트로픽 연구진은 개인용 Claude Max 요금제 세 개로 에이전트들을 Prove2Me에서 협업시켜, 비노그라도프의 세 소수 정리(충분히 큰 홀수는 모두 소수 세 개의 합으로 쓸 수 있다는 정리)를 3일 만에 형식화했습니다. 앤트로픽은 알맞은 틀만 있으면 소비자용 구독으로도 큰 정리를 함께 형식화할 수 있다고 봤고, Prove2Me는 에이전트만 있으면 누구나 과제를 올리고 참여하는 공개 플랫폼입니다.

다음 시험은 Annals Challenge입니다. 50개 문장은 Lean 평가 사이트 lean-eval에 올라가고, 버저드는 그중 적어도 두 편이 형식화되지 않은 군론 1만 쪽에, 한 편이 대수기하 2,000쪽에 기대고 있으며 가우스가 썼어도 됐을 쉬운 논문도 하나 있다고 적었습니다. 그는 50편 가운데 2~3편은 앞으로 정오표를 낼 것으로 어림했고, 형식화할 수 없는 논문이 하나 나올 확률을 반반으로 봤습니다. 저는 증명을 옮기는 속도보다 정의를 만드는 속도가 다음 1년의 형식화 속도를 정할 가능성이 크다고 봅니다. Annals 논문의 80%는 아직 정리 문장도 Lean으로 적지 못했고, 가장 큰 걸림돌이 정의이기 때문입니다.

버저드는 9월 4일 글을 1993년 이야기로 맺었습니다. 박사과정 2년 차였던 그는 와일스의 강연 첫날에 갔다가 하나도 알아듣지 못해 나머지 두 번을 빠지고 여자친구와 아일랜드로 휴가를 떠났고, 1주일 뒤 돌아와서야 증명 소식을 들었습니다. 올해 앤트로픽의 메일이 왔을 때는 같은 사람과 웨일스의 그린맨 음악 축제에 있었는데, 처음 보는 사람이 보낸 「페르마의 마지막 정리 Lean 형식화」 메일을 이상한 사람의 편지로 여기고 넘겼다가 1주일 뒤 밀린 메일 1,000통 가까이를 정리하다 소식을 알았다고 합니다.

읽어 주셔서 고맙습니다.

초이 드림