https://www.anthropic.com/research/formalizing-fermats-last-theorem

간단히 말하면, Claude가 페르마의 마지막 정리(FLT)를 Lean으로 완전히 형식화해서 컴퓨터가 검증 가능한 증명을 만들어냈다는 내용입니다.

핵심은 이렇습니다.

• Claude가 약 11일 동안 거의 자율적으로 작업해서 페르마의 마지막 정리의 최초의 완전한 컴퓨터 검증 증명을 만들었습니다.
• 이 과정에서 약 1,300만 줄의 Lean 코드와 약 3만 개의 중간 정리를 생성했습니다.
• 여러 Claude 에이전트가 동시에 하위 정리들을 나눠 풀었고, Prove2Me라는 협업 시스템이 어떤 정리를 먼저 풀어야 하는지 DAG 구조로 관리했습니다.
• 인간의 개입은 매우 적었고, 연구자가 가끔 “이 부분을 우선하라” 정도의 고수준 지시만 했다고 합니다.
• 완성된 증명은 Lean이 직접 검증했기 때문에, 단순히 LLM이 “그럴듯한 수학 증명”을 쓴 것과는 상당히 다릅니다.

다만 중요한 점은 Claude가 페르마의 마지막 정리를 새롭게 증명한 것은 아닙니다. 이미 알려진 Wiles의 증명 계열을 AI가 Lean이라는 엄격한 형식 언어로 옮겨서 컴퓨터 검증이 가능하게 만든 것입니다. Anthropic도 이것을 새로운 수학적 발견이라기보다는 formalization/verification의 돌파구로 설명합니다.

제가 보기엔 AGI 관점에서 더 흥미로운 부분은 “11일 동안 수십 개의 에이전트가 수만 개의 하위 문제를 관리하면서 장기 프로젝트를 끝냈다”는 점입니다. 단순 수학 벤치마크 점수가 아니라, 장기 계획 → 작업 분해 → 병렬 연구 → 오류 수정 → 최종 검증이라는 연구 자동화에 가까운 형태라서 꽤 강한 결과입니다.