클로드가 괴델의 노트를 읽었다, 검산까지 퇴근한 건 아니다

1. 저는 먼저 400과 200과 50을 더해봤습니다

괴델의 노트에서 수백 개의 수학적 성과를 찾아냈다는 기사를 읽고, 저는 먼저 검증 결과의 숫자부터 더해봤습니다. 그대로 확인됐다는 약 400개, 손봤다는 약 200개, 거짓이었다는 약 50개. 합하면 약 650개입니다. 추출했다는 전체 항목은 663개입니다. 그렇다고 나머지 13개가 실종됐다고 따질 일은 아닙니다. 애초에 ‘약’이 붙은 숫자입니다. 다만 이 정도 보고를 가지고 소수점까지 붙인 정답률을 계산해서는 곤란하다는 점은 바로 드러납니다.

제가 이 대목에서 멈춘 이유는 단순합니다. 도구가 얼마나 많이 내놓았는지보다, 내놓은 것을 무엇으로 셌는지가 먼저이기 때문입니다. 장바구니에 물건 20개를 담았다고 저녁 반찬 20가지가 생기지는 않습니다. 달걀도 있고, 소금도 있고, 아직 손질하지 않은 생선도 있습니다. 괴델의 노트에서 추출했다는 663개 항목도 완성된 증명, 증명 초안, 아이디어를 함께 센 수치입니다. 이것들을 전부 ‘새 정리’로 바꾸는 순간, 연구 소식은 실적 부풀리기가 됩니다.

여기서 정리는 정해진 조건 아래 참임을 논리적으로 보인 수학 문장이고, 증명은 그 결론까지 빠짐없이 이어지는 이유입니다. 아이디어는 증명으로 가는 출발점일 수 있지만, 출발했다는 사실과 도착했다는 사실은 다릅니다. 서울역에서 부산행 열차를 알아봤다고 부산 출장이 끝나지는 않습니다. 영수증 처리도 안 됩니다.

이번 소재에 제시된 연구 경위는 충분히 흥미롭습니다. 헬싱키대 논리학자 얀 폰 플라토가 이끄는 연구진은 2017년부터 괴델의 노트 16권, 1,009쪽을 연구했습니다. 오래된 독일어 속기, 즉 말을 빠르게 적는 특별한 기호 체계와 난해한 수학이 함께 들어 있었습니다. 연구자 설명에 따르면 수학적 내용을 이해하는 진도는 일주일에 한 쪽 정도였습니다. 올해 9월 앤트로픽의 대화형 AI인 클로드에 전사본과 관련 문헌을 제공했고, 며칠 만에 650쪽짜리 해설을 받았습니다. 전사본은 사람이 원문의 글자와 기호를 읽어 옮긴 자료입니다. 이 결과 역시 쪽마다 확인해야 했다고 합니다.

저의 주장은 분명합니다. 이 사례의 핵심은 ‘AI가 수학자를 대체했다’가 아닙니다. 제안하는 일과 확인하는 일을 나눴을 때, 묻혀 있던 지식을 다시 연구할 여지가 커졌다는 데 있습니다. 앞으로 좋은 연구용 AI를 가르는 기준도 이 분업을 얼마나 잘 지원하느냐가 될 것입니다. 답을 많이 뱉는 기계는 이미 있습니다. 그 답을 믿어도 되는지 알아보는 비용은 여전히 비쌉니다.

다만 출발선은 정확히 그어야 합니다. 여기서 다루는 수치와 성과는 연구자가 보고한 내용입니다. 이 글에서 663개 항목의 증명 파일을 직접 실행해 확인한 것은 아닙니다. 연구자의 설명을 읽은 일과 증명을 재검사한 일은 다른 작업입니다. 이 구분부터 놓치면, 검증의 중요성을 말하는 글이 정작 검증을 생략하게 됩니다.

2. 클로드가 받은 것은 낡은 공책만이 아니었습니다

오래된 집안 장부를 정리한다고 생각해봅시다. 누군가 흘려 쓴 글씨를 읽고, ‘김 씨’가 누구인지 확인하고, 당시 돈의 단위까지 적어놓았습니다. 그 자료를 다른 사람에게 넘겨 연도별 지출을 정리하게 했습니다. 결과가 훌륭하더라도 두 번째 사람 혼자 장부 전체를 해독했다고 말하면 첫 번째 사람의 일이 사라집니다.

괴델의 노트에서도 이 앞단이 중요합니다. 클로드에 들어간 것은 연구자가 마련한 전사본과 관련 문헌이었습니다. 따라서 이 사례는 손글씨 사진을 던져놓자 기계가 글자를 읽고, 수학을 이해하고, 역사적 공로까지 판정한 전 과정의 자동화가 아닙니다. 사람이 읽을 수 있게 만든 자료에서 흩어진 논증의 연결고리를 찾고 설명하는 작업에 도움을 받은 사례로 읽어야 합니다. 연구 경위와 검증 결과 정리

여기에 쓰인 LLM은 대규모 언어 모델의 줄임말로, 많은 글에서 표현과 관계를 학습해 주어진 문맥에 맞는 답을 만드는 AI입니다. 문장을 자연스럽게 잇는 능력과 수학적으로 옳은 문장을 만드는 능력은 겹치기도 하지만 같지는 않습니다. 설명이 매끄러워도 중간에 필요한 조건이 빠질 수 있습니다. 독자는 잘 읽히는 글을 이해하기 쉬운 글로 받아들이고, 이해하기 쉬운 글을 맞는 글로 받아들이기 쉽습니다. 두 번의 착각이 한 번에 일어납니다.

긴 연구 자료를 읽을 때 AI가 도울 수 있는 지점은 분명합니다. 앞부분에서 정의한 기호가 뒤에서 다른 표현으로 등장하는지 찾고, 서로 떨어진 주장 사이에 필요한 연결을 제안하고, 짧은 메모를 검토 가능한 설명으로 펼쳐놓을 수 있습니다. 다만 이번 작업에서 자료를 어떻게 나눠 넣었는지, 몇 차례 고쳤는지, 누가 어떤 부분을 형식적인 증명으로 옮겼는지까지 모두 확인된 것은 아닙니다. 결과의 분량만 보고 내부 작업 절차를 상상해서 채우면 안 됩니다.

기술적으로 이해하기 쉬운 작업 구분은 다음과 같습니다. 이는 공개된 모든 세부 절차를 복원한 목록이 아니라, 이런 연구를 제대로 평가하기 위해 나눠 봐야 할 단계입니다.

1. 원문을 읽을 수 있게 만듭니다. 글자 하나의 오독이 뒤의 논증을 바꿀 수 있으므로, 전사본에는 원문의 위치와 애매한 판독을 함께 남겨야 합니다.
2. 주장과 근거의 후보를 찾습니다. 서로 멀리 떨어진 메모를 연결하되, 원문에 있는 연결과 새로 제안한 연결을 구분해야 합니다.
3. 빠진 조건과 중간 단계를 드러냅니다. 자연스러운 해설에 빈틈이 가려지지 않도록, 무엇을 가정해야 결론이 나오는지 적어야 합니다.
4. 검사할 수 있는 표현으로 옮깁니다. 사람에게 그럴듯한 설명을 기계가 규칙대로 확인할 수 있는 엄밀한 문장으로 바꿔야 합니다.
5. 원래 질문과 다시 맞춥니다. 검사에 통과한 문장이 정말 노트에서 확인하려던 주장인지, 중간에 다른 문제로 바뀌지는 않았는지 살펴야 합니다.

650쪽의 해설은 이 과정에서 유용한 중간 결과일 수 있습니다. 그러나 해설의 쪽수가 많다는 사실은 검증이 끝났다는 뜻이 아닙니다. 오히려 확인할 문장이 늘었다는 뜻도 됩니다. 제대로 만든 도구라면 긴 설명만 내놓지 않고, 어느 원문에서 어느 결론이 나왔는지 바로 찾아가게 해야 합니다. 설명서가 두꺼운 가전제품보다 고장 난 곳을 알려주는 가전제품이 고맙습니다.

3. 영수증 합계가 맞아도 남의 장바구니일 수 있습니다

마트 영수증의 덧셈은 모두 맞는데, 집에 와서 보니 남의 장바구니를 계산했다고 해봅시다. 계산기는 제 일을 했습니다. 장보기는 실패했습니다. 수학의 형식 검증도 이 구분이 필요합니다. 형식 검증은 문장을 모호하지 않은 기호와 규칙으로 표현한 뒤, 그 규칙에 맞게 결론이 나왔는지 검사하는 일입니다. 무엇을 검사기에 넣었는지까지 저절로 보장하지는 않습니다.

이번 보도에 등장하는 Coq는 이런 증명 작업을 돕는 프로그램이며, 현재 명칭은 Rocq입니다. 공식 문서는 증명을 만드는 과정과 검사하는 핵심 부분을 구분합니다. 사용자가 편리한 명령으로 증명을 구성하면, 마지막에는 ‘증명 항’이라는 엄밀한 표현이 만들어지고 커널이 이를 확인합니다. 커널은 운영체제 이야기가 아니라, 여기서는 정해진 규칙을 집행하는 작은 핵심 검사 부분을 뜻합니다. 복잡한 증명 생성 과정 전체보다 이 핵심 부분에 신뢰를 집중하도록 설계한 것입니다. Rocq 공식 문서

중요한 차이가 있습니다. Coq는 클로드가 써준 한국어나 영어 해설을 읽고 ‘말이 되는군요’라고 고개를 끄덕이는 심사위원이 아닙니다. 검사할 수 있는 형식으로 표현된 주장과 증명을 다룹니다. 따라서 ‘Coq로 확인했다’는 설명만으로는 자연어 해설이 검사 가능한 증명으로 바뀌는 데 누가 얼마나 일했는지 알 수 없습니다. 이 중간 노동은 연구의 실제 생산성을 평가할 때 반드시 따져야 합니다.

가령 ‘모든 정수 n에 대해 n의 제곱은 n보다 크다’는 주장을 생각해봅시다. 정수는 음수와 0과 양수를 포함하는 수입니다. n이 0이거나 1이면 두 값이 같으므로 원래 문장은 거짓입니다. 여기에 ‘n이 2 이상일 때’라는 조건을 붙이면 참인 문장으로 고칠 수 있습니다. 하지만 수정된 문장을 증명했다고 원래 문장까지 참이 되지는 않습니다. 여기서 고친 것은 맞춤법이 아니라 주장이 적용되는 범위입니다.

이 차이를 괴델의 노트에 그대로 단정할 수는 없습니다. 실제 수정 항목마다 사정이 다를 테니까요. 다만 ‘약 200개를 수정했다’는 설명을 읽을 때 무엇을 물어야 하는지는 분명해집니다. 이미 주변 문맥에 있던 조건을 명확히 적었는지, 전혀 없던 가정을 보탰는지, 결론의 범위를 줄였는지에 따라 의미가 달라집니다.

검사 도구가 성공했다고 표시해도 전제 목록은 봐야 합니다. 증명해야 할 핵심 내용을 전제로 먼저 허용했다면, 그 위의 계산이 아무리 정확해도 원래 과제를 해결한 것은 아닙니다. 돈을 빌려놓고 통장 잔고가 늘었다고 수익을 자랑하는 셈입니다. 실제로 그런 일이 이번 연구에서 있었다는 뜻은 아닙니다. 검증 결과를 제대로 읽으려면 성공 표시와 함께 무엇을 허용했는지도 확인해야 한다는 뜻입니다.

따라서 이 분업의 장점은 AI가 절대로 틀리지 않는다는 데 있지 않습니다. 틀릴 수 있는 제안을 외부 기준에 걸어볼 수 있다는 데 있습니다. 동시에 그 외부 기준이 원래 문제를 제대로 표현했는지는 또 다른 검토 대상입니다. 한 번의 검사로 모든 책임이 사라지는 구조는 아닙니다. 대신 어느 부분을 누구에게 물어야 하는지가 또렷해집니다.

4. 4세대 언어도, CASE도, 노코드도 일을 없애지는 못했습니다

프로그램 만드는 일을 쉽게 하겠다는 약속은 오래됐습니다. 4세대 언어는 컴퓨터가 실행할 세부 순서를 길게 적기보다 원하는 결과를 더 짧게 표현하도록 한 언어들을 가리킵니다. CASE 도구는 설계와 개발을 컴퓨터로 돕는 도구입니다. 노코드는 직접 코드를 거의 쓰지 않고 화면과 설정을 조합해 프로그램을 만드는 방식입니다. 이름은 바뀌지만, 사람이 세부 작업에 쓰는 시간을 줄이겠다는 방향은 이어집니다.

이 흐름을 이해하기 좋은 예가 SQL입니다. SQL은 표로 저장된 자료에서 필요한 항목을 찾고 합치는 데 쓰는 언어입니다. IBM의 에드거 커드는 1970년 자료를 관계와 표로 다루는 모델을 제시했고, 돈 체임벌린과 레이먼드 보이스는 SQL을 함께 개발했습니다. 자료가 실제로 어디에 어떤 순서로 저장됐는지를 일일이 다루지 않고도, 필요한 결과를 표현하는 방향이 열렸습니다. IBM의 관계형 데이터베이스 역사

예를 들어 ‘지난달 고객별 결제액 합계를 구하라’고 요청할 수 있습니다. 컴퓨터는 자료를 찾아 묶고 더하는 일을 맡습니다. 하지만 지난달은 결제일 기준인지 배송일 기준인지, 취소한 주문을 뺄지, 같은 고객이 계정을 두 개 쓰면 어떻게 셀지는 사람이 정해야 합니다. 합계 계산이 자동화될수록 합계의 정의가 더 중요해집니다. 숫자는 정확한데 회의에서는 서로 다른 숫자를 보고 싸우는 이유입니다.

CASE 도구나 노코드도 같은 질문을 남깁니다. 화면을 연결하고 업무 순서를 그려 프로그램을 만들기 쉬워져도, 환불 승인 권한을 누구에게 줄지, 중복 신청을 어떻게 막을지, 예외가 생기면 어디로 보낼지는 정해야 합니다. 버튼을 만드는 수고가 줄었다고 버튼을 누른 뒤의 책임까지 없어지지는 않습니다. 이 도구들이 쓸모없었다는 말이 아닙니다. 유용했기 때문에 다음 문제가 더 잘 보이게 됐습니다.

괴델의 노트와 연결되는 지점도 여기입니다. 클로드가 논증의 초안을 만드는 부담을 줄인다면, 연구자는 그 초안이 무엇을 전제로 하고 어느 원문을 반영했는지에 더 많은 주의를 쏟을 수 있습니다. 동시에 이전보다 훨씬 많은 후보를 검토해야 할 수도 있습니다. 노동이 줄어드는 부분과 늘어나는 부분을 함께 봐야 합니다.

다만 과거와 현재를 똑같다고 뭉개서도 안 됩니다. SQL은 정해진 문법에 맞는 요청을 실행합니다. 언어 모델은 불완전하고 애매한 자료에서도 해석을 제안할 수 있습니다. 이 때문에 접근할 수 있는 문제가 넓어집니다. 대신 같은 애매함 때문에 없는 연결을 그럴듯하게 보탤 위험도 생깁니다. 다루는 범위가 넓어진 만큼, 받아들일 결과를 가리는 장치가 더 중요해지는 셈입니다.

제가 이 역사에서 읽는 교훈은 ‘자동화는 늘 실패한다’가 아닙니다. 자동화가 성공하면 사람이 결정해야 하는 위치가 바뀐다는 점입니다. 자료를 찾는 순서를 직접 짜던 사람이 ‘누구를 고객으로 셀 것인가’를 결정하게 됩니다. 증명 초안을 이어 붙이던 연구자가 ‘이 조건을 추가해도 원래 주장인가’를 판단하게 됩니다. 손이 덜 간다는 사실과 머리를 덜 써도 된다는 결론 사이에는 꽤 긴 거리가 있습니다.

5. 663개라는 숫자가 말하지 않는 것들

이번 소식에서 가장 조심해야 할 오해는 세 가지입니다. 첫째, 663개를 모두 새로운 정리로 읽는 일입니다. 둘째, 거짓인 항목 약 50개를 전부 클로드가 만들어낸 오류로 돌리는 일입니다. 셋째, 검사에 통과한 재구성의 공로를 전부 괴델이나 전부 클로드에게 주는 일입니다. 세 주장 모두 지금 제시된 정보보다 앞서 나갑니다.

첫 번째 오해부터 보겠습니다. 추출된 항목에는 증명 초안과 아이디어도 들어 있습니다. 더구나 수학적으로 참이라는 판단과 지금까지 알려지지 않았다는 판단은 별개입니다. 노트에서 찾은 결과가 후대에 다른 사람이 이미 발표한 내용일 수 있습니다. 그 경우 수학사의 가치가 있을 수 있지만, 오늘의 수학에 새 정리가 하나 추가됐다고 세면 안 됩니다. 독립적으로 떠올린 아이디어, 시대를 앞선 초안, 완성된 증명은 서로 다른 칸에 넣어야 합니다.

두 번째 오해는 오류의 출처입니다. 연구 노트는 완성된 교과서가 아닙니다. 시도하다가 막힌 길과 나중에 버린 생각이 함께 남습니다. 거짓인 항목을 충실하게 추출했다면 추출 작업 자체는 맞았을 수도 있습니다. 반대로 원문은 타당했는데 전사나 해석 과정에서 조건이 빠졌을 수도 있습니다. 출처를 대조하지 않고 ‘약 50개가 거짓이니 AI의 오류율은 얼마’라고 계산하면 서로 다른 실패를 한데 섞게 됩니다.

세 번째 오해는 특히 흥미롭습니다. 선택공리는 내용물이 하나 이상 있는 집합들을 모아놓았을 때, 각 집합에서 하나씩 고른 결과가 존재한다고 허용하는 수학의 기본 가정입니다. 유한한 장바구니 몇 개에서 물건 하나씩 고르는 장면으로 출발하면 쉽지만, 핵심은 무한히 많은 집합과 고르는 규칙이 분명하지 않은 경우까지 다룬다는 데 있습니다. 일상의 장보기 감각만으로 끝까지 판단할 수 있는 문제는 아닙니다.

어떤 가정의 독립성이란, 지정한 기본 규칙들만으로는 그 가정도 그 부정도 증명할 수 없다는 뜻입니다. 이때 어느 규칙 체계를 쓰는지가 중요합니다. 그래서 ‘선택공리의 독립성을 증명했다’는 말도 이름만 보고 확인할 수 없습니다. 어떤 전제 아래 무엇을 보였는지, 검사한 형식 문장이 그 주장을 정확히 담는지까지 봐야 합니다.

연구자는 관련 재구성이 Coq 검사를 통과했다고 설명했습니다. 그러나 재구성이 작동한다는 사실과 괴델이 당시 완성된 증명을 갖고 있었다는 판단은 다릅니다. 논리학자 조엘 데이비드 햄킨스도 재구성물을 직접 보지 못했다는 전제에서 역사적 공로 판단에 신중한 태도를 보였습니다. 관련 보도

가령 오래된 조리 메모에 재료와 조리 순서가 거의 다 있는데 마지막 온도가 빠져 있다고 해봅시다. 후대의 요리사가 다른 메모에서 온도를 찾아 요리를 완성했다면 두 가지 성과가 생깁니다. 옛 메모의 가치를 밝혔고, 실제로 작동하는 조리법도 만들었습니다. 그렇다고 옛 작성자가 그 조리법을 끝까지 시험했다고 자동으로 결론 내릴 수는 없습니다. 수학에서는 그 빠진 한 단계가 조리 온도보다 훨씬 결정적일 수도 있습니다.

반론도 가능합니다. ‘그래도 수백 개를 확인했다면 충분히 대단하지 않은가.’ 맞습니다. 보고대로라면 연구 가치가 큽니다. 그런데 성과가 크다는 평가와 성과를 정확히 분류하는 일은 충돌하지 않습니다. 오히려 분류가 정확해야 무엇이 대단한지 알 수 있습니다. 이미 있던 증명을 빠르게 정리한 것인지, 흩어진 조각을 새로 연결한 것인지, 없던 조건을 보태 새로운 주장을 만든 것인지에 따라 다음 연구가 달라지기 때문입니다.

또 하나 남는 질문은 비용입니다. 며칠 만에 해설을 만들었다는 시간과, 그 해설을 확인해 쓸 수 있는 결과로 바꾸는 데 든 시간은 따로 재야 합니다. 전사본을 준비한 선행 작업도 있습니다. 이를 무시하고 ‘몇 년 걸릴 연구를 며칠로 줄였다’고 단정하면 앞단과 뒷단의 노동이 통계에서 증발합니다. 생산성이 높아졌을 가능성은 충분합니다. 얼마나 높아졌는지는 별도의 계산이 필요합니다.

6. 다음에 볼 숫자는 출력량이 아니라 확인 시간입니다

이 사례를 연구용 제품으로 옮긴다면 저는 첫 화면에 ‘몇 쪽을 읽었습니다’보다 ‘이 결론의 근거를 열어보기’를 놓겠습니다. 사람은 설명이 길어서만 지치는 게 아닙니다. 설명을 확인하려고 원문을 다시 찾고, 바뀐 조건을 비교하고, 앞서 본 자료를 또 펼치느라 지칩니다. 이 왕복을 줄이는 기능이 실제 연구 시간을 줄일 가능성이 큽니다.

원하는 결과물도 단순한 해설집과 다릅니다. 주장 하나를 열면 원문 이미지, 전사문, 해석, 추가한 조건, 최종 증명을 함께 볼 수 있어야 합니다. 처음에는 거짓이었던 문장이 어떤 수정 뒤에 참이 됐는지도 보여야 합니다. 수정 전 문장을 지우고 말끔한 최종본만 남기면 읽기는 편하지만 연구하기는 어려워집니다. 어디를 고쳤는지 알아야 다른 사람이 그 판단에 동의하거나 반박할 수 있기 때문입니다.

독자가 다음 보도나 제품 시연에서 추적할 신호는 다음과 같습니다.

• 항목별 근거가 연결돼 있는지 봅니다. 결론에서 원문의 쪽과 해당 구절로 돌아갈 수 있어야, 검토자가 자료 찾기부터 반복하지 않습니다.
• 수정 전후의 조건이 보이는지 봅니다. 표현만 다듬었는지 적용 범위를 줄였는지 구분해야, 성과의 크기를 과장 없이 평가할 수 있습니다.
• 증명 파일과 실행 환경이 제시되는지 봅니다. 사용한 도구의 버전과 필요한 파일을 알아야, 다른 연구자가 같은 검사를 다시 수행할 수 있습니다.
• 성공하지 못한 항목도 남아 있는지 봅니다. 거짓인 주장과 아직 증명하지 못한 주장을 나눠야, 다음 사람이 같은 막힌 길을 되풀이하지 않습니다.
• 사람의 검토 시간을 측정하는지 봅니다. 출력 속도가 빨라도 확인에 더 오래 걸린다면, 전체 작업의 생산성은 기대만큼 좋아지지 않을 수 있습니다.

마지막 항목은 특히 중요합니다. 다음은 이번 연구의 실측값이 아니라 계산을 위한 가정입니다. 후보 하나를 확인하는 데 30분이 걸리면 100개를 검토하는 데 50시간이 듭니다. AI가 후보를 1,000개로 늘려도 검토 시간이 그대로라면 500시간이 필요합니다. 반대로 근거 연결과 수정 표시 덕분에 후보 하나의 검토 시간이 5분으로 줄면 1,000개를 약 83시간 20분에 볼 수 있습니다. 물론 실제 시간은 난도에 따라 크게 달라집니다. 핵심은 출력량과 확인 비용을 함께 봐야 한다는 점입니다.

오래된 기업 연구소의 실험 기록에도 이런 방식은 적용해볼 만합니다. 단, ‘적용할 여지’와 ‘효과가 입증됐다’는 말은 구분해야 합니다. 예를 들어 과거 실험에서 특정 조건일 때만 성능이 좋아졌다는 기록을 찾았다면, 원래 측정값과 실험 조건을 연결해 보여주는 도구가 도움이 될 수 있습니다. 그러나 문서 안의 계산이 맞는다고 실제 장비에서도 같은 결과가 나오는 것은 아닙니다. 실험은 반복해서 확인해야 하고, 빠진 환경 조건이 결과를 바꿀 수도 있습니다.

수학은 명시한 규칙 아래 논리적 연결을 검사할 수 있다는 강점이 있습니다. 다른 분야에서는 기록 자체가 불완전하거나 측정값에 오차가 있을 수 있습니다. 그래서 수학에서의 분업을 가져오더라도 확인 수단까지 똑같이 복사할 수는 없습니다. 무엇을 문서 대조로 확인하고, 무엇을 계산으로 확인하며, 무엇을 다시 실험해야 하는지 새로 나눠야 합니다. 검사기가 없는 분야에 ‘검사 완료’ 도장을 먼저 만드는 것은 제품 개발이 아니라 도장 장사입니다.

경쟁 모델과의 비교도 같은 원칙을 따라야 합니다. 이 사례만으로 클로드가 다른 모델보다 수학을 잘한다고 결론 내릴 수는 없습니다. 같은 입력 자료, 같은 과제, 비슷한 사람의 도움, 같은 판정 기준으로 비교해야 합니다. 특히 사람이 중간에 얼마나 고쳤는지를 빼면 모델 성능과 팀의 숙련도를 구분할 수 없습니다. 화려한 결과 하나는 가능성을 보여줍니다. 비교 우위까지 증명하지는 않습니다.

7. 싸지는 것은 초안이고, 비싸지는 것은 판단입니다

이 소식을 읽으며 제가 기대하는 변화는 논리학자의 퇴근 선언이 아닙니다. 오래 걸려서 뒤로 밀렸던 자료를 다시 펼쳐볼 이유가 생기는 일입니다. 읽을 수 있게 정리된 기록은 있지만 연결해서 검토할 여력이 없었던 곳에서, 후보를 빠르게 제안하는 도구가 새로운 연구를 열 수 있습니다. 모든 후보가 맞을 필요는 없습니다. 틀린 후보를 걸러내는 비용까지 포함해 이전보다 유용해야 합니다.

여기에는 불편한 변화도 있습니다. 초안을 만드는 일이 싸지면 초안을 읽고 승인하는 사람에게 일이 몰립니다. 해결책을 ‘전문가가 마지막에 보면 된다’ 한 문장으로 끝내서는 안 됩니다. 전문가의 하루도 24시간입니다. 마지막 검토를 맡길 생각이라면, 그 사람이 판단할 근거를 앞단에서 차곡차곡 남겨야 합니다. 사람을 검증 장치로 쓰겠다고 하면서 확인할 자료는 주지 않는 설계가 의외로 쉽게 나옵니다.

그렇다고 전문가는 영원히 안전하다는 위안으로 읽을 일도 아닙니다. 자료를 모으고 형식을 맞추고 초안을 정리하는 작업의 가치는 바뀔 수 있습니다. 판단하는 사람 역시 근거 없이 권위만 내세우기 어려워집니다. 원문과 수정 내역이 공개되면 누구의 해석이 더 설득력 있는지 비교하기 쉬워지기 때문입니다. 판단의 값이 오른다는 말은 직함의 값이 오른다는 뜻이 아닙니다. 책임질 수 있는 근거를 갖춘 판단이 더 중요해진다는 뜻입니다.

독자가 던질 법한 질문도 남겨두겠습니다.

Q. 약 50개가 거짓이었다면 연구에 쓰기에는 너무 위험한 것 아닙니까?

A. 이 숫자만으로는 도구의 위험도를 계산할 수 없습니다. 원래 노트에 있던 거짓 주장을 정확히 찾아낸 것인지, 해석하면서 틀린 주장을 만든 것인지부터 구분해야 합니다. 검토할 후보를 넓히는 단계에서는 거짓 후보가 섞여도 도움이 될 수 있습니다. 다만 후보를 검증된 결론처럼 쓰면 안 됩니다. 유용성을 평가하려면 틀린 항목을 걸러낸 시간과, 그 덕분에 찾은 가치 있는 결과를 함께 봐야 합니다.

Q. Coq 검사를 통과했다면 사람은 무엇을 더 확인해야 합니까?

A. 적어도 검사한 문장이 원래 주장과 같은지, 어떤 전제를 허용했는지, 수정하면서 의미가 얼마나 바뀌었는지는 봐야 합니다. 역사 연구라면 그 결과가 당시 노트에 어디까지 있었는지도 확인해야 합니다. 형식 검사는 명시된 논리적 과제를 확인하는 강력한 수단입니다. 원문의 뜻과 역사적 공로를 대신 판정하는 수단은 아닙니다. 검사 결과를 존중하려면 검사 범위도 정확히 존중해야 합니다.

Q. 연구 현장에서 써보고 싶다면 무엇부터 해야 합니까?

A. 답과 근거를 이미 알고 있는 작은 자료 묶음부터 시험하는 편이 낫습니다. 원문 위치를 제대로 찾는지, 모르는 부분을 드러내는지, 조건을 바꿀 때 표시하는지 살펴볼 수 있습니다. 그다음 처음 보는 자료로 넓히면서 사람이 확인하는 시간을 재면 됩니다. 성공 기준은 보기 좋은 보고서가 아닙니다. 같은 수준으로 믿을 수 있는 결과를 얻는 데 전체 시간이 줄었는지입니다. 괴델의 노트와 같은 성과가 다른 자료에서도 날지는 실제로 확인해야 합니다.

이번 이야기를 ‘수백 개의 정리를 발견한 AI’로만 기억하면, 다음 제품에서도 결과 개수부터 세게 됩니다. 저는 그보다 원문으로 돌아가는 길과 수정한 흔적을 보겠습니다. 며칠 만에 만들어진 해설이 연구자의 다음 몇 달을 얼마나 덜 힘들게 하는지가 궁금합니다. 새 도구의 실력은 그 대목에서 드러납니다.

4세대 언어가 계산의 절차를 덜 쓰게 했어도 무엇을 셀지는 정해야 했습니다. 노코드가 화면을 빨리 만들게 했어도 어떤 권한을 줄지는 정해야 했습니다. 클로드가 오래된 노트의 연결을 제안해도, 그 연결이 성립하고 원문에 충실하며 새로울 가치가 있는지는 확인해야 합니다. 없어지는 일과 남는 일을 이렇게 나눠야 기술의 실체가 보입니다.

초안이 싸질수록, 무엇을 믿을지 판단하는 값은 올라갑니다.