11일에 Lean 1300만 줄: 에이전트를 늘린 게 아니라 그래프 한 장을 공유시켰다

수십 개의 에이전트를 동시에 돌려서 큰 일을 끝냈다는 이야기는 흔하다. 이번 건에서 볼 대목은 그게 처음엔 실패했다는 부분이다.

Anthropic이 9월 4일 페르마의 마지막 정리를 Lean으로 형식화한 결과를 공개했다. 11일, Lean 코드 1300만 줄, 중간 정리 3만 300개 증명(최종 증명에 2만 9500개 사용). 이 분야의 공용 라이브러리인 Mathlib의 5배 크기다. 출력 토큰은 약 60억 개를 썼고 모델은 Claude Fable 5.1급의 내부 범용 모델이었다.

1995년 Andrew Wiles의 첫 증명은 129쪽이었고 검증에만 수개월이 걸렸다. 1993년 발표 두 달 뒤 결함이 드러났고 Wiles가 그걸 메우는 데 1년이 더 걸렸다. 이걸 컴퓨터가 자동으로 검사할 수 있는 형태로 옮기는 작업에 수학계는 몇 년을 예상했다. 초기 단계 설계도만 86쪽이다.

한 줄 정리

11일이라는 숫자보다 중요한 건 첫 시도가 왜 실패했고 두 번째가 왜 됐는지다.

처음엔 에이전트들이 협업을 못 했다

Anthropic이 밝힌 초기 실패의 원인은 모델 능력이 아니다. 에이전트들이 초반에 성과를 내다가 프로젝트 상태를 놓치고 서로 협업을 그만뒀다. 그 실패한 시도들이 최종 증명의 비보일러플레이트 코드 중 7% 정도만 남겼다.

방향을 바꾼 지점은 Prove2Me다. Columbia 대학의 Tianyi Peng 팀이 만든 공개 협업 플랫폼이고 하는 일이 셋이다.

정리 문장들의 방향 있는 비순환 그래프(DAG)를 유지한다. 에이전트는 이 그래프를 보고 다음에 뭘 증명할지 정한다. 컨텍스트가 길어지며 기억이 흐려지는 문제를 이걸로 막고 여럿이 동시에 붙을 수 있게 했다.
정리의 문장과 증명을 다른 파일로 분리한다. 둘 사이의 연결은 따로 관리한다. Lean 컴파일이 빨라지고 자원 소모가 준다.
정리마다 자연어 설명을 붙여 둔다. 검색과 재사용이 되니 증명 경로가 단순해진다.

사람이 넣은 수학적 입력은 가끔 던지는 고수준 지시뿐이었다. "스킴으로서의 야코비안이 우선순위가 높아 보인다" 정도의 한 줄이다.

개인 구독 세 개로 3일

같이 공개된 실험이 본편보다 실무에 가깝다. Anthropic 연구자들이 개인 Claude Max 요금제 3개만 써서 하디-리틀우드 원 방법의 응용을 형식화해 봤다. 전부 Prove2Me를 통해서만 협업했고 비노그라도프의 세 소수 정리 형식화를 3일에 끝냈다.

60억 토큰짜리 본편은 개인이 흉내 낼 수 없다. 소비자 구독 세 개짜리 실험은 다르다. 판만 제대로 깔면 큰 결과의 형식화가 일반 구독으로도 된다는 게 Anthropic의 판단이다.

검증도 짚어 둘 만하다. 완성된 증명은 Lean이 검사했고 Lean의 표준 공리 세 개만 쓴다. 별도 비교 도구로 증명한 정리의 문장이 Mathlib에 적힌 페르마의 마지막 정리 문장과 일치하는지도 확인했다. Kevin Buzzard가 검토했다.

새 수학이 아니라 검증이다

이 결과가 만든 게 새로운 수학은 아니다. Anthropic이 최근 낸 리만 가설 관련 작업은 새 수학을 만든 쪽이었고 이번 건은 검증 쪽이다. 이미 아는 증명을 컴퓨터가 한 줄씩 따질 수 있는 형태로 옮긴 것이다.

이게 왜 큰 일인지는 수학계의 검증 관행을 보면 나온다. 케플러 추측은 심사에 4년이 걸렸고 12명짜리 심사단이 "99% 확신"에서 멈췄다. 푸앵카레 추측은 학계가 받아들이는 데 4년과 300쪽짜리 해설 세 편이 필요했다. 약한 골드바흐 추측은 2013년 증명이 아직 심사 중이다. 틀린 결과가 몇 년간 정설로 남아 다른 이론의 토대가 된 사례도 있다.

Kevin Buzzard가 짚은 지점이 실무적이다. 자동 형식화가 지금 가능하다면 현대 수학 문헌 전체를 기계가 검사하는 방향으로 크게 다가선 것이고, 그 도구는 심사자의 부담을 덜 뿐 아니라 AI가 만들어 낸 수학을 검사하는 데 쓰인다. 지금은 그 검사를 사람이 하고 있고 비용이 크다.

anyAX 관점

이 프로젝트가 실무에 주는 교훈은 수학이 아니라 실패한 첫 시도에 있다. 같은 모델, 같은 목표, 다른 결과. 갈린 것은 작업 상태를 어디에 두느냐였다.

에이전트를 여러 개 돌려 본 팀이라면 아는 장면이다. 처음엔 잘 굴러가다가 서로 뭘 했는지 모르는 상태가 되고, 같은 걸 두 번 하거나 아무도 안 한 구멍이 남는다. 사람을 더 붙여도 안 풀리는 종류의 문제다. Anthropic이 이걸 푼 방법은 에이전트를 더 똑똑하게 만드는 쪽이 아니라 무엇이 끝났고 다음에 뭐가 가능한지를 담은 판 하나를 바깥에 두고 전부 거기를 보게 한 것이다.

일반 업무로 옮기면 그 판은 정리 그래프가 아니라 작업 목록이다. 콘텐츠 팀이라면 기획·초안·검수·발행 상태를 한 곳에서 읽고 쓰는 표, 커머스라면 상품별 남은 단계다. 지금 대부분의 팀은 그걸 채팅 스레드와 각자의 머리에 나눠 갖고 있고, 그래서 에이전트를 붙이면 사람이 겪던 혼선이 더 빠른 속도로 재현된다.

순서가 이렇게 뒤집힌다. 자동화할 일을 정하는 게 먼저가 아니라 일의 상태를 한 곳에 적는 게 먼저다. 판이 없으면 에이전트 하나를 잘 돌리는 데서 멈추고, 판이 있으면 그때부터 개수를 늘리는 게 의미를 갖는다. 11일과 3일이라는 숫자는 판을 깐 다음에 나온 것들이다.