중요X
Anthropic, Claude가 11일 만에 페르마의 마지막 정리 컴퓨터 검증 완료
수십 개 Claude 에이전트가 Lean 코드 1300만 줄 자율 생성. 형식검증·정리증명 자동화 가능성 시사.
요약
Anthropic의 AI 모델 Claude가 페르마의 마지막 정리(Fermat’s Last Theorem)를 컴퓨터가 완전히 검증할 수 있는 형태로 11일 만에 증명했다. 이는 1995년 앤드루 와일스가 증명한 기존 정리를 논리적 단계별로 컴퓨터가 확인 가능한 형태로 변환한 성과다. Claude는 자율적으로 수십 개의 에이전트를 가동해 1,300만 줄의 Lean 코드와 약 29,500개의 보조 정리를 생성했다. 이 과정에서 대수학, 기하학, 정수론 등에 걸쳐 이전에 공식화되지 않았던 수학적 정리들도 기계 검증이 가능한 형태로 다수 도출했다. 이번 성과는 향후 수학자들이 연구를 빠르게 검증하고 숨겨진 오류를 찾아내며, AI가 생성한 증명을 엄밀하게 평가하는 데 기여할 것으로 기대된다.
AI가 원문을 요약한 내용으로, 부정확할 수 있습니다.
원문 제목 @kimmonismus: Respect where respect is due: Anthropic says Claude completed the first fully computer-checked proof of Fermat’s Last Theorem in 1
원문 보기 ↗