AI 요약
앤트로픽(Anthropic)이 자사의 AI 모델 클로드(Claude)를 활용해 페르마의 마지막 정리(FLT)의 최초 완전한 컴퓨터 검증 증명(공식화)에 성공했다고 발표한 기사입니다. 클로드는 11일간 거의 자율적으로 작업하며 Lean 프로그래밍 언어로 1,300만 줄의 코드와 29,500개의 중간 정리를 작성했습니다. 이는 1995년 앤드루 와일스가 제시한 129페이지 분량의 증명을 컴퓨터가 자동 검증 가능한 형태로 변환한 것으로, 케빈 버자드(임페리얼 칼리지 런던) 교수의 검증을 받았습니다. 이 성과는 수학적 증명의 신뢰성 검증 방식을 혁신할 잠재력을 지니며, AI가 생성하는 증명의 품질을 평가하는 부담을 크게 줄일 수 있을 것으로 기대됩니다.
핵심 포인트
- 클로드(Claude)가 11일간 자율 작업으로 페르마의 마지막 정리 증명을 Lean 언어로 공식화하는 데 성공
- 1,300만 줄의 Lean 코드와 29,500개의 중간 정리가 작성됨
- 1995년 앤드루 와일스의 129페이지 증명을 컴퓨터가 자동 검증 가능한 형태로 변환
- 케빈 버자드 교수는 "수학 공리 외에 다른 가정 없이 증명된 놀라운 성과"라고 평가
향후 전망
- AI 기반 증명 공식화 기술이 발전하면 수학계의 증명 검증 기간이 수년에서 수일로 단축될 가능성
- 리만 가설 등 다른 난제에 대한 AI 활용 연구가 가속화될 전망