앤스로픽, 클로드가 페르마의 마지막 정리 최장 증명 작성했다고 밝혀

앤스로픽은 클로드가 11일 만에 페르마의 마지막 정리를 형식적으로 증명했다고 밝혔다. 앤스로픽은 이 결과가 지금까지 작성된 가장 긴 수학적 증명이라고 말했다. 이 증명은 컴퓨터가 한 줄씩 확인할 수 있는 1,300만 줄의 코드를 포함한다. 페르마의 마지막 정리는 358년 동안 수학자들을 난처하게 했다. 케빈 버자드는 증명을 검토하고 수학 공리 외에 어떤 가정도 없이 정리를 증명한다고 말했다. 이번 작업은 새로운 수학을 발견한 것이 아니라 1995년 앤드루 와일스의 증명을 형식화한 것이다. 수십 개의 클로드 에이전트가 간헐적인 지시 외에는 거의 사람의 입력 없이 병렬로 작업했다. 초기 단계에서 나온 실패 시도는 최종 증명 줄 수의 약 7%를 차지한다. 펭의 팀은 에이전트들을 조율하고 중복 작업을 막기 위해 Prove2Me 도구를 사용했다. 클로드는 3만 개가 넘는 보조 정리를 증명했고 수십억 개의 토큰을 사용했다. 이 증명은 Mathlib보다 5배 넘게 크다. 임페리얼 칼리지 런던의 수학자 케빈 버자드는 2024년에 와일스의 증명을 Lean으로 옮기는 프로젝트를 시작했다. 이 프로젝트는 2029년까지 자금이 지원된다. 전체 증명은 수학자들이 검토할 수 있도록 GitHub에 공개돼 있다.