앤트로픽의 AI 모델 클로드가 '페르마의 마지막 정리'를 컴퓨터가 검증할 수 있는 형식(formalization)으로 변환하는 작업을 11일 만에 완성했다고 9월 4일 밝혔다. 수십 개의 클로드 에이전트가 협업해 증명 보조기 린(Lean)으로 약 1300만 줄의 코드를 작성하고 2만9500개의 중간 정리를 증명했으며, 이는 현재까지 작성된 가장 큰 규모의 Lean 증명이다. 컬럼비아대 연구진이 개발한 협업 플랫폼 프로브투미(Prove2Me)를 활용해 여러 에이전트의 작업 순서와 상태를 관리하면서 협업 효율을 높였다. 앤트로픽은 이번 성과가 새 정리 증명이 아니라 기존 증명의 컴퓨터 검증화라는 점을 강조하며, AI가 만든 수학 결과를 사람이 검증해야 하는 부담을 줄이는 데 의미가 있다고 설명했다.

• •당초 수년 걸릴 것으로 예상된 형식화 작업을 클로드가 11일 만에 완료
• •약 1300만 줄의 Lean 코드 작성, 2만9500개 중간 정리 증명 — 역대 최대 규모 Lean 증명
• •수십 개 클로드 에이전트가 협업, 컴럼비아대 개발 플랫폼 프로브투미로 작업 조율
• •새로운 수학적 증명이 아니라 기존 와일스 증명의 컴퓨터 검증 가능한 형식화
• •이후 비노그라도프의 세 소수 정리도 3일 만에 형식화하는 후속 실험 진행