Claude, 11일 만에 페르마의 마지막 정리 증명을 컴퓨터로 검증하다
Formalizing Fermat's Last Theorem
Anthropic의 연구진이 AI 어시스턴트 Claude를 활용해 페르마의 마지막 정리(Fermat's Last Theorem)에 대한 최초의 완전한 컴퓨터 검증 증명을 생성했습니다. 클로드는 11일 동안 거의 자율적으로 작업하며 13백만 줄의 Lean 코드와 29,500개의 중간 정리를 증명했습니다. 이 작업은 Columbia University의 Tianyi Peng이 설계한 오픈 협업 플랫폼 Prove2Me를 기반으로 여러 AI 에이전트가 협력하여 수행되었습니다. 이 성과는 수학적 증명의 검증 과정을 자동화하고, AI가 생성한 수학적 결과에 대한 신뢰를 높이는 데 중요한 진전으로 평가됩니다.
이 특별한 자동 형식화 성과는 페르마의 마지막 정리를 수학의 공리 외에는 어떤 가정도 없이 증명했으며, AI 자동 형식화 산출물이 이제 그 위에 구축될 수 있을 만큼 견고하다는 것을 보여줍니다.