0부터 99까지의 수를 원 위에 놓고 몇 개를 고른다고 생각해 보자. 고른 두 수의 차이를 세되, 같은 차이가 세 번 이상 나오면 안 된다는 조건이 있다. 이 조건을 지키는 13개짜리 집합은 확인할 수 있었는데, 한 개를 더 골라 14개로 만들 수 있는지는 훨씬 큰 계산이 필요했다.
나는 하나의 예가 맞는지 확인하는 검사와, 더 큰 예가 없다는 검사를 나누어 진행했다. 이 글은 2026년 8월 18일 정리한 구성 검사와 탐색 점검을 다룬다. 이후 8월 20일에는 공개된 P2624 증명 파일을 다시 만드는 별도의 작업까지 이어졌으므로, 당시의 미완료 상태가 지금도 전체 작업의 마지막 단계인 것은 아니다.
두 수를 고르는 순서까지 세었다
이 문제에서 차이는 100으로 나눈 나머지로 읽는다. 3에서 98을 빼면 −95지만, 원 위에서는 5와 같은 차이로 본다. 순서를 바꾸어 98에서 3을 빼면 95가 되므로 두 방향은 각각 세어야 한다. 단, 서로 50만큼 떨어진 한 쌍은 어느 방향으로 빼도 나머지가 50이라 같은 차이에 두 번 기여한다.
13개 원소로 된 예를 별도 검사기에 넣어 서로 다른 두 원소의 차이를 직접 열거했다. 순서를 구분하는 쌍은 13 × 12 = 156개이며, 0이 아닌 어느 나머지도 두 번을 넘지 않았다. 탐색 프로그램의 판정만 읽는 대신, 선택한 수들이 조건을 만족하는지 짧은 계산으로 다시 확인한 것이다.
이 결과로 적어도 13개는 고를 수 있다는 사실을 알 수 있다. 그러나 14개짜리 집합 하나만 나타나도 최대 크기가 13이라는 결론은 깨진다. 따라서 다음 계산에서는 특정한 예를 잘 검사하는 것만으로 부족했고, 가능한 14개짜리 집합이 검토 범위에서 빠지지 않도록 해야 했다.
탐색 범위와 탐색 결과를 따로 점검했다
먼저 조건을 바꾸지 않고 서로 옮길 수 있는 집합들을 묶었다. 모든 수에서 같은 수를 빼거나, 100과 공약수가 1뿐인 수를 곱하면 차이의 중복 횟수는 유지된다. 이런 변환과 반사를 이용해 기준을 맞춘 뒤, 선택한 원소의 순서에 따라 탐색을 작은 분기로 나눴다. 대칭을 줄이는 규칙이 유효한지와 분기가 빠짐없이 이어지는지는 계산 결과에 앞서 확인할 부분이었다.
8월 18일의 점검에서는 저장된 최종 분기 목록에 누락이나 중복이 없고, 완료 기록에 14개짜리 예나 최종 시간초과가 남지 않았음을 확인했다. 과거에 시간초과가 났던 기록은 이력으로 보존하면서 최종 계산의 근거에서는 제외했고, 일부 분기는 별도로 작성한 탐색기로 다시 실행한 기록과 대조했다.
여기서 남은 문제가 있었다. 저장된 목록이 완전하다는 사실은 각 분기 안의 계산까지 모두 옳았다는 보증이 아니었다. 당시의 자체 탐색에는 전역 계산을 별도로 전부 재실행한 기록이나, 모든 경우의 불가능성을 검사할 수 있는 증명서가 아직 없었다.
계산의 결론을 다시 검사할 수 있게 만들기
그다음 경로로는 조건을 SAT 문제로 옮기는 방식을 준비했다. SAT는 여러 참·거짓 조건을 한꺼번에 만족시킬 수 있는지 묻는 문제다. 여기서는 각 수를 고를지와 차이의 중복 제한을 조건으로 적어, 14개짜리 집합이 가능한지 검사하도록 했다.
계산 프로그램이 해를 찾지 못했다는 응답과 불가능성을 확인한 증명서는 구분했다. 제한시간이 끝난 실행은 결론을 내리지 못한 것이며, 조건을 모두 만족시키는 해가 없다는 UNSAT 판정도 그 입력에 대한 증명 출력이 별도 검사기를 통과해야 재검사 가능한 근거가 된다. 그래서 파일 내용에서 계산하는 식별값인 해시로 입력과 증명 파일을 고정하고 함께 확인하는 경로를 마련했지만, 8월 18일 패키지에서 이 전역 SAT 증명서까지 완성한 것은 아니었다.
이후에는 공개된 증명 객체를 재구성하는 다른 경로로 진척이 생겼다. 8월 20일 작업에서는 가능한 경우의 갈림길을 담은 P2624 증명 트리 일곱 개를 다시 생성하고, TheoremDB의 공개 파일별 해시를 맞춘 뒤 별도 검사기로 모든 갈림길을 따라 확인했다. 원래의 자체 SAT 실행을 완료한 결과와는 구분해야 하며, 공개 원증명을 처음 만들었다는 뜻도 아니다. 그 과정과 검증 범위는 P2624 증명 파일 재구성 기록에 이어 적었다.
이 초기 작업에서 남긴 것은 13개짜리 예의 직접 검사와, 더 큰 예를 배제하려는 탐색을 어디까지 믿을 수 있는지 가려낸 기록이다. 이후의 증명 재구성까지 함께 읽으면 한 구성을 확인하는 작은 검사에서 계산 전체를 다시 확인할 수 있는 파일로 어떻게 작업이 이어졌는지 볼 수 있다.