앤트로픽, 클로드로 '페르마의 마지막 정리' 증명 형식화 시도
한 줄 요약: 앤트로픽이 클로드를 활용해 '페르마의 마지막 정리' 증명을 기계 검증이 가능한 형식으로 옮기는 작업을 진행 중인 것으로 전해졌다.
핵심
- 앤트로픽이 자사 모델 클로드로 페르마의 마지막 정리(Fermat's Last Theorem)의 증명 **형식화(formalization)**를 지원했다고 SiliconANGLE이 보도했다.
- 형식화란 사람이 쓴 증명을 Lean 같은 증명 보조 도구가 한 단계씩 자동 검증할 수 있는 형태로 옮기는 작업을 뜻한다.
- 페르마의 마지막 정리는 1994년 앤드루 와일스가 증명한 난제로, 그 방대한 증명을 형식화하는 것은 그 자체로 대규모 프로젝트로 꼽힌다.
왜 중요한가
수학 증명 형식화는 AI의 논리적 추론 능력을 가늠하는 대표적 시험대다. 이번 시도는 대형 언어모델이 단순 문장 생성을 넘어 엄밀한 수학·검증 영역에서 실제 연구를 보조할 수 있는지를 보여주는 사례로 읽힌다.