모델
Claude, 페르마의 마지막 정리를 Lean으로 형식화
Anthropic은 2026년 9월 4일, Claude가 페르마의 마지막 정리에 대한 최초의 완전한 컴퓨터 검증 증명을 만들었다고 밝혔다. Prove2Me 플랫폼에서 대체로 자율적인 멀티 에이전트 작업을 약 11일간 진행해 약 1,300만 줄의 Lean 코드를 작성하고 약 2만 9,500개의 중간 정리를 증명했으며, Lean의 표준 공리 3개와 Mathlib의 FLT와 일치하는 명제를 사용했다. Anthropic 연구원 티옌이 펑이 상위 우선순위를 지시했고, 케빈 버자드는 결과를 검토해 자동 형식화가 놀랍다고 평가하며 이런 기법이 AI가 만든 수학을 검증하고 심사 부담을 덜어 줄 수 있다고 말했다. Anthropic은 이를 와일스 정리 경로(다르몽–다이아몬드–테일러 경유)의 검증으로 설명하며, 리만 가설 관련 새 결과 같은 새로운 수학이나 Claude 소비자 제품 출시가 아니라고 밝혔다.
AI의 도움으로 번역되었습니다.