facts

11일이라는 기간 동안 대부분 자율적으로 수행된 이번 작업은 기존의 페르마의 마지막 정리 증명을 Lean(증명 보조기) 언어로 옮겨 컴퓨터가 종단 간(End-to-End) 검증할 수 있게 만든 사례다. 앤스로픽은 Claude Fable 5.1 수준의 내부 범용 연구 모델을 사용했으며, 이 과정에서 약 60억 개의 출력 토큰을 소비했다. 결과물은 총 1,300만 줄의 Lean 코드로, 이는 표준 수학 라이브러리인 Mathlib의 5배가 넘는 규모다.

증명 과정에서는 수십 개의 클로드 에이전트가 협업하여 총 3만 300개의 정리를 증명했으며, 최종 결과물에는 이 중 2만 9,500개가 사용됐다. 검증은 Lean 컴파일러와 comparator(Mathlib에 정의된 정리와 일치하는지 확인하는 도구)를 통해 수행됐다. 형식수학자 케빈 버자드(Kevin Buzzard)가 직접 코드를 컴파일해 검증 결과를 최종 확인했다.

how-it-works

다중 에이전트 하네스는 개념 정의와 중간 정리 증명을 수행한 뒤, 그 결과를 재사용해 더 복잡한 명제로 나아가는 파이프라인으로 작동한다. 초기 시도에서는 에이전트들이 전체 프로젝트 상태를 공유하지 못해 협업에 실패했으며, 이 과정에서 생성된 실패 코드가 최종 분량의 약 7%를 차지했다. 이를 해결하기 위해 도입된 Prove2Me(콜롬비아 대학교 티안이 펭 연구진 개발) 플랫폼은 정리 간의 의존성 그래프를 유지해 에이전트가 이미 증명된 결과와 다음 목표를 명확히 인지하게 한다.

Prove2Me는 정리 문장과 증명을 별도 파일로 분리해 관리함으로써 Lean의 컴파일 속도를 높이고 자원 사용량을 줄인다. 각 정리에 자연어 설명을 부착해 에이전트가 기존 결과를 검색하거나 더 단순한 증명 경로를 찾도록 유도하는 구조다. 클로드는 1995년 앤드루 와일즈(Andrew Wiles)와 리처드 테일러(Richard Taylor)가 정리한 증명 방식을 따랐으며, 랭글랜즈-터널(Langlands-Tunnell) 정리와 리벳(Ribet)의 준위 내림 정리를 통해 논증을 전개했다.

다만 생성된 코드의 효율성은 낮다. 사람이 검토해 다듬은 Mathlib과 달리, 클로드의 결과물은 중복이 많고 필요 이상으로 길다. 96코어 머신에서도 Mathlib보다 컴파일 시간이 약 20배 더 소요되며, 500GB 메모리를 탑재한 머신에서도 저장소 탐색이 불편할 정도로 거대하다. 이는 컴퓨터에 의한 논리적 정확성 확보와 사람이 읽고 유지보수할 수 있는 코드 품질이 서로 다른 문제임을 보여준다.

implementation-impact

이번 성과는 새로운 수학적 발견보다 수천 쪽의 기존 문헌을 단기간에 형식화할 수 있는 가능성을 입증한 데 의미가 있다. 특히 소규모 환경에서의 재현 가능성도 확인됐다. 개인용 Claude Max 요금제 3개와 Prove2Me만으로 비노그라도프(Vinogradov)의 세 소수 정리를 3일 만에 형식화한 실험 결과가 이를 뒷받침한다.

이러한 자동 형식화 기술은 향후 오래된 논문의 논리적 공백이나 잘못 인용된 결과를 찾는 작업, 그리고 새로운 논문의 심사 부담을 줄이는 도구로 활용될 수 있다. AI가 생성하는 방대한 수학적 결과물을 인간 심사자가 모두 검토하기 어려운 한계를 보완하는 장치가 될 가능성이 크다.

실무적으로는 AI를 이용한 수학 연구 시, 가설과 중간 결과를 즉각적으로 점검하기 위해 Lean과 같은 형식 검증 도구를 파이프라인에 통합하는 전략이 유효하다. 특히 인간이 작성한 논문과 컴퓨터가 검증하는 형식 증명을 동시에 제공하는 방식이 수학적 신뢰성을 확보하는 새로운 표준이 될 것으로 보인다.