Anthropic은 수십 개의 Claude 에이전트가 11일 동안 기존 페르마의 마지막 정리 증명을 Lean으로 형식화해 3만300개 정리와 약 1,300만줄 코드를 만들었다고 밝혔습니다. Lean과 독립 comparator 검사를 통과했고 형식수학자 Kevin Buzzard도 직접 컴파일했지만 새로운 수학 증명은 아닙니다. 약 60억 출력 토큰을 썼고 96코어와 500GB 메모리 환경에서도 다루기 어려워 기계적 정확성과 사람이 유지할 품질은 구분해야 합니다.