컴퓨터가 가능한 경우를 모두 검사했다는 결론을 읽을 때, 그 검사 과정을 다른 프로그램으로도 확인할 수 있는지가 궁금하다. P2624에서는 공개된 설명과 파일별 식별값을 바탕으로 증명 트리 일곱 개를 다시 생성해 비교했다. 2026년 8월 20일 남긴 결과는 전체 299,903,736개 노드와 일곱 파일의 SHA-256 해시가 공개 기록에 모두 일치한다는 것이었다.
트리는 검사할 경우가 어떻게 갈라지고 어디에서 막히는지를 담은 파일이다. 숫자 하나로 된 결론보다 크지만, 검사기가 각 갈림길을 따라가며 빠진 경우가 없는지 확인할 수 있다. 내가 재구성한 대상은 Jordan Boisclair의 TheoremDB 계정에 공개된 R6088–R6090의 증명 객체다. 원증명의 새로움을 주장하는 작업은 아니다.
무엇을 빠짐없이 검사하는가
이 문제에서는 0부터 99까지의 수를 원형으로 생각한다. 두 수를 빼서 음수가 나오면 100을 더해 같은 원 위의 차이로 읽는다. 선택한 서로 다른 두 수의 순서를 구분해 차이를 셌을 때, 0이 아닌 어떤 차이도 두 번을 넘지 않도록 14개의 수를 고를 수 있는지가 질문이다. 이 조건을 만족하는 13개짜리 집합은 알려져 있어, 14개가 불가능함을 확인하는 쪽이 핵심이다.
모든 집합을 곧바로 늘어놓기 전에, 수를 20으로 나눈 나머지에 따라 묶었다. 각 나머지에 몇 개가 들어가는지를 점유 벡터로 표현하면 가능한 형태가 일곱 부류로 나뉜다. 조건을 통과한 원시 점유 벡터는 총 204,360개였고, 평행이동과 조건을 보존하는 곱셈으로 서로 바뀌는 경우를 묶으면 대표 1,341개가 남는다. 이런 대칭에 따른 묶음을 affine orbit이라고 부른다.
대표를 골랐다고 검사가 끝나는 것은 아니다. 같은 나머지를 가진 수는 원래의 100개 수 안에 다섯 개씩 있으므로, 각 대표에서 실제로 어떤 수를 선택할 수 있는지 다시 펼쳐야 한다. 이 과정을 담은 것이 lift tree다. 검사기는 갈림길마다 가능한 선택을 직접 계산해 각각에 대응하는 자식 트리가 있는지 확인하고, 막다른 지점에서는 정말 더 고를 수 없는지 검사한다.
같은 경우를 어떤 순서로 기록할 것인가
수학적으로 같은 경우를 다뤄도 파일이 만들어지는 순서가 다르면 노드 수와 해시가 달라질 수 있다. 처음에 자연스럽게 보였던 원시 점유값의 사전식 정렬은 일부 부류에서 공개값과 맞지 않았다. 재구성에서는 한 개 이상 들어 있는 자리, 두 개 이상 들어 있는 자리, 세 개 들어 있는 자리를 각각 이진 층으로 나누어 비교했다.
이 세 층을 나란히 놓고, 나머지 20개를 옮기는 160개 affine 변환 중 가장 앞서는 표현을 골라 정렬했다. 트리를 만들 때는 가능한 선택이 가장 적은 변수부터 고르되, 동률이면 작은 변수 번호를 먼저 쓰고 선택 마스크도 숫자 순서대로 읽었다. 이 규칙을 맞추자 일곱 트리의 노드 수뿐 아니라 파일별 해시까지 모두 일치했다. 해시는 파일 내용에서 계산하므로, 단순히 총합을 맞춘 것보다 훨씬 구체적인 비교다.
생성기와 검사기를 나누어 확인했다
별도로 구현한 검사기는 카탈로그를 다시 만들고, 재구성한 일곱 트리의 모든 노드를 순회했다. 생성기가 어느 변수를 먼저 골랐는지 그대로 믿는 대신, 그 노드에서 허용되는 선택을 다시 계산하도록 했다. 금지된 값을 받아들이는지도 보려고 한 트리의 예약 비트 하나를 바꾸었고, 검사기는 그 파일을 거절했다. 예약 비트는 형식상 반드시 0으로 남겨 두는 자리다.
13개짜리 집합도 따로 확인했다. 순서를 구분하는 두 원소의 차이를 직접 열거하면 156쌍이 나오며, 0이 아닌 99개 나머지 중 다섯 개는 0회, 32개는 1회, 62개는 2회 나타났다. 최대 중복이 2라는 조건을 실제 집합이 만족하는지 확인하는 작은 검사다.
일곱 파일의 일치는 증명 구성요소를 재현했다는 근거다. 공개되지 않은 원본 ZIP의 나머지 파일이나 압축 설정·시간 정보까지 복구한 것은 아니어서, 새 패키지에는 별도의 이름과 해시를 붙였다. 자체 생성기와 검사기 코드는 MIT, 자체 문서와 생성 자료는 CC BY 4.0 범위로 구분했으며 외부 TheoremDB 문구와 코드를 재라이선스하지 않았다. 남긴 것은 공개된 결론을 그대로 옮긴 요약이 아니라, 그 결론을 검사하는 파일을 다시 만들어 대조할 수 있는 경로다.