클로드, 괴델 노트서 정리 후보 663건 추려…Coq서 약 400건은 제시된 형태로 검증

핀란드 논리학자 얀 폰 플라토는 괴델의 미출간 노트에서 Claude가 정리 후보 663건을 추렸다고 Guardian에 밝혔습니다. 후보에는 괴델이 증명을 적은 항목뿐 아니라 증명 개요와 아이디어를 남긴 항목도 포함됩니다. 폰 플라토가 Claude에 제공한 자료는 노트의 필사본, 그가 앞서 쓴 괴델 연구서 6권, 관련 과학 문헌이었습니다. 그는 며칠 만에 650쪽 분량의 해설을 받았다고 전했습니다. Claude는 사람이 필사한 자료를 종합하고 후보를 정리하는 단계에 투입됐습니다.

괴델의 노트에는 독일어 속기인 가벨스베르거(Gabelsberger)와 논리 기호가 섞여 있습니다. 헬싱키대 괴델 에니그마 프로젝트는 괴델의 미출간 자료를 연구하며 속기 판독, 논리·기초 연구, 역사 연구 방법을 함께 사용합니다. 이 프로젝트를 이끄는 폰 플라토는 Claude를 활용하기 전까지 노트의 수학적 내용을 파악하는 속도가 대략 일주일에 한 쪽이었다고 Guardian에 말했습니다.

폰 플라토는 2026년 8월 프랑스에서 열린 인공지능과 정리 증명 관련 학회에서 Claude의 도움을 활용하자는 제안을 받았습니다. 헬싱키로 돌아온 뒤 필사본과 관련 자료를 Claude에 제공했습니다. 그는 사람이 여러 쪽을 차례로 읽으면 긴 자료 곳곳의 연결을 기억하기 어렵지만, Claude는 전체를 한데 놓고 살펴볼 수 있었다고 설명했습니다. 다만 Claude의 해설은 쪽마다 대조해야 했습니다.

Claude에 처음 맡긴 과제 중 하나는 괴델의 노트에 선택공리 독립성의 증명이 있는지 살펴보는 일이었습니다. 독립성은 주어진 공리 체계 안에서 어떤 명제를 증명하거나 반증할 수 없는 상태를 가리킵니다. Guardian 보도에 따르면 괴델은 1966년 폴 코언이 선택공리와 연속체 가설의 독립성을 보인 공로로 필즈상을 받은 뒤, 자신도 1940년대에 해당 결과를 증명했다고 말했습니다. 동료들이 증명을 요구했을 때 괴델은 노트에서 이를 다시 구성하지 못했습니다.

폰 플라토는 Claude가 내놓은 답이 거의 긍정적이었다고 전했습니다. 괴델의 노트에는 정의 하나가 잘못 적혀 있었지만, 그보다 2년 앞선 기록에는 올바른 정의가 있었다고 설명했습니다. 폰 플라토는 Claude가 재구성한 증명을 Coq에 넣어 검사했고 통과했다고 밝혔습니다. 몇 달 더 연구했다면 괴델이 올바른 증명에 도달했을 것이라는 판단은 폰 플라토의 해석입니다.

폰 플라토는 Claude가 추린 663건을 Coq으로 점검했습니다. 약 400건은 제시된 형태 그대로 검증됐고, 약 200건은 명제를 더 정확하게 쓰거나 가정을 추가한 뒤 검증됐습니다. 약 50건은 거짓으로 분류됐습니다. 각 수치는 근사치로 제시됐으며, 집계 대상에는 완성된 증명뿐 아니라 증명 개요와 아이디어 단계의 후보도 포함됩니다.

Coq은 정리와 증명을 컴퓨터가 다룰 수 있는 형식으로 적으면, 핵심 검증기가 증명이 정해진 논리 규칙에 맞는지 검사하는 증명 보조기입니다. 선택공리 사례에서 확인된 것은 형식화된 명제에 대한 Claude의 재구성 증명이 Coq 검사를 통과했다는 점입니다. 노트의 속기를 어떻게 읽었는지와 그 아이디어의 역사적 귀속은 필사·수학적 해석·역사 연구가 다루는 문제입니다. 노트의 증명 재구성을 아직 보지 못했다고 밝힌 노트르담대 논리학자 조엘 데이비드 햄킨스는 증명이 성립한다면 역사적으로 의미가 있으며, Claude와 괴델의 기여를 가르는 일은 역사가들의 몫이라고 말했습니다.