Anthropic은 수십 개 Claude 에이전트가 페르마의 마지막 정리 증명을 11일 만에 Lean 코드 1300만줄로 옮겼다고 밝혔습니다. 출력 토큰 60억개를 써 보조 정리 3만개 이상을 만들었고 Lean 검증기와 별도 비교 도구 및 독립 커널로 논리 단계와 최종 명제를 확인했습니다. 새 수학을 발견한 결과는 아니며, 기존 증명을 기계가 검사할 수 있게 전환한 대규모 협업 자동화 사례입니다.