Kurt Gödel은 발표한 것보다 훨씬 많은 것을 남겼지만 대부분은 거의 읽을 수 없었습니다. The Guardian이 보도한 헬싱키 프로젝트는 언어 모델이 학자라면 몇 년이 걸릴 일을 며칠 만에 해냈음을 보여 줍니다. 1,009쪽 분량 노트의 내용을 정리하고 수백 개의 정리를 뽑아낸 것입니다. 글쓰기나 코드가 아니라 역사 연구에서 AI 모델이 쓸모를 보인, 지금까지 가장 분명한 사례 중 하나입니다.
자료는 Gödel이 1940년대 초에 채운 16권의 작업 노트로, 상당 부분이 그가 쓰던 당시에도 이미 사라진 독일어 속기법 Gabelsberger로 적혀 있습니다. Jan von Plato는 2017년부터 유럽연구위원회의 250만 유로 지원을 받아 헬싱키대학교에서 이 프로젝트를 이끌어 왔으며, 이 속기를 읽을 수 있는 사람은 세계에 6명뿐이고 자신이 그중 한 명이라고 말합니다. 8월 AI와 정리 증명에 관한 학회에 다녀온 뒤 그는 자신의 필사본, Gödel에 관해 쓴 자신의 책 6권, 그 밖의 2차 문헌을 Claude에 주었습니다. 이틀쯤 지나 650쪽짜리 해설이 나왔고, 그는 이를 한 쪽씩 확인해야 했다고 말합니다.
눈에 띄는 결과는 그다음입니다. 노트에 선택 공리의 독립성 증명이 있는지 묻자 Claude는 한 단계가 모자란 논증을 찾아냈습니다. 이는 Paul Cohen이 1966년 필즈상을 받은 결과이며, Gödel은 자신이 먼저 도달했다고 주장했습니다. 정의 하나가 틀렸지만 Gödel은 2년 전에 올바른 정의를 갖고 있었습니다. von Plato는 재구성된 증명이 증명 보조기 Coq에서 통과했다고 말합니다. 이어 Claude는 Gödel이 증명했거나 개요를 썼거나 아이디어를 남긴 정리 663개를 찾아냈습니다. Coq에서 약 400개는 그대로 검증되었고, 약 200개는 명제를 더 정확히 하거나 가정을 추가하는 수정이 필요했으며, 약 50개는 틀렸습니다.
긴 문서에 Claude를 쓰는 사람에게 주는 교훈은 조합에 있습니다. von Plato의 말대로 모델의 강점은 천 쪽을 한꺼번에 보는 것이고, 안전장치는 모델의 말을 그대로 믿지 않는 형식 검증기입니다. 우리가 수학과 검증 작업용으로 다루는 Lean 도구들도 같은 논리입니다.
의문도 분명합니다. 재구성은 공개되지도 검토되지도 않았고, Notre Dame의 논리학자 Joel David Hamkins는 이를 보지 못했다면서 Cohen의 증명과 비슷하다는 것이 그것을 가졌다는 뜻은 아니며 어디까지가 Claude이고 어디까지가 Gödel인지는 역사가가 가릴 일이라고 경고합니다. 탐구되지 않은 주제가 십여 개 넘게 있다는 주장도 아직 사람이 아니라 Claude에게서 나온 것입니다.