당신이 거대하고 끊임없이 확장되는 수학적 아이디어의 도서관을 걷고 있다고 상상해 보십시오. 이 도서관에서는 모든 새로운 책(증명)이 자신의 논거를 구축하는 데 사용한 오래된 책들을 반드시 인용해야 합니다. 보통 수학자가 새로운 증명을 쓸 때는 그 당시에 사용할 수 있는 가장 흔하고 잘 다져진 도구들을 사용하려 노력합니다. 하지만 때때로 그들은 아무도 이들을 섞어 쓸 것이라고 생각지 못했던 기묘한 도구들의 조합을 사용하여, 예상치 못한 파격적인 길을 택하기도 합니다. 큰 질문은, 그들이 사용한 책의 목록을 보는 것만으로 그들의 경로가 진정으로 놀라운 것이었는지, 아니면 그저 일상적인 우회였는지를 어떻게 알 수 있느냐는 것입니다. 이것이 바로 "새로움(novelty)"에 관한 퍼즐입니다. 인간은 증명이 "우아하다"거나 "독창적이다"라고 논쟁할 수 있지만, 컴퓨터는 이러한 모호한 느낌을 다루는 데 어려움을 겪습니다. 컴퓨터에게는 증명이 당시 알려진 바에 비추어 볼 때 얼마나 일어나기 힘든 경로를 택했는지를 측정할 수 있는 단단하고 기계적인 방법이 필요합니다. 여기서 "놀라움(surprisal)"이라는 개념이 등장합니다. 이는 증명이 도서관을 향해 "잠깐, 이 일을 위해 저 특정한 도구를 사용했다고?"라고 말하게 만드는 척도로 생각하면 됩니다.

PriorProof라는 새로운 도구가 시간 여행을 하는 사서 역할을 하기 위해 등장했습니다. PriorProof는 인간에게 "이 증명이 영리했나요?"라고 묻는 대신, 차갑고 딱딱한 질문을 던집니다. "만약 이 증명이 쓰인 바로 그 순간에 도서관을 동결시킨다면, 사용된 도구들의 목록은 얼마나 놀라운가?" 연구진은 형식적인 증명(Lean이라는 언어로 작성된)을 분석하여, 화려한 서식을 제거하고 사용된 특정 수학적 기계 장치들의 "발자국(footprint)"을 만드는 시스템을 구축했습니다. 그런 다음, 그 증명이 존재하기 전의 시점으로 도서관의 스냅샷을 가지고 시간을 거슬러 올라갑니다. 그리고 묻습니다. "그 당시 비슷한 목표를 가진 다른 증명들을 바탕으로 볼 때, 누군가가 이 특정한 도구들을 사용할 확률이 얼마나 되었을까?" 만약 그 답이 "매우 낮음"이라면, 그 증명은 높은 "새로움 점수"를 받게 됩니다. 연구 결과, 이 기계적인 점수는 인간 전문가들이 어떤 증명이 더 특이한 경로를 택했는지에 대해 내린 결론과 자주 일치했으며, 특히 점수 차이가 클 때 그러했습니다. 그러나 저자들은 이것이 모든 것을 해결하는 마법 지팡이는 아니라고 주의를 기울입니다. 이것은 두 증명 사이의 격차가 명확할 때 가장 잘 작동하는 유용한 신호일 뿐이며, 수학의 "아름다움"이나 "중요성"을 측정하는 것이 아니라, 오직 그 경로가 얼마나 예상 밖이었는지를 측정할 뿐입니다.

시간 여행하는 사서

당신이 도둑이 금고를 털기 위해 이전에 본 적 없는 비밀스러운 방법을 사용했는지 알아내려는 탐정이라고 상상해 보십시오. 당신은 도둑의 의도를 물을 수는 없지만, 그가 남긴 도구들은 볼 수 있습니다. PriorProof는 수학적 증명에 대한 그 탐정입니다. 그것은 도둑의 동기나 범행이 얼마나 멋졌는지에는 관심이 없습니다. 오직 문제를 해결하기 위해 사용된 도구들(수학적 상수와 보조정리)과, 그 도구들이 해당 시기에 기이한 선택이었는지에만 관심을 가집니다.

이 마술의 단계별 과정은 다음과 같습니다:

1. 발자국(The Footprint): 수학자가 Lean(수학을 위한 컴퓨터 언어)으로 증명을 작성하면, 컴퓨터는 이를 사용된 모든 개별 도구의 길고 상세한 목록으로 변환합니다. PriorProof는 이 목록을 가져와 정리하고, 유사한 도구들을 "가족"(예를 들어 모든 망치를 하나로 묶거나, 모든 드라이버를 하나로 묶는 것과 같이)으로 그룹화합니다. 이것이 "발자국"입니다.
2. 타임머신(The Time Machine): 그런 다음 시스템은 시간을 거슬러 올라갑니다. 증명이 작성되기 전의 전체 수학 라이브러리의 스냅샷을 포착합니다. 그리고 그 당시에 비슷한 문제를 해결하려고 했던 모든 다른 증명들을 살펴봅니다.
3. 예측(The Prediction): 스마트한 컴퓨터 모델(언어 모델)을 사용하여 다음과 같이 예측합니다: "만약 내가 그 당시에 이 문제를 위한 증명을 쓰고 있다면, 나는 아마 어떤 도구들을 사용할 것인가?" 이는 수학적 도구에 대한 일기예보처럼 "사전(prior)" 기대치를 구축합니다.
4. 놀라움 점수(The Surprise Score): 마지막으로, 실제 증명에 사용된 도구들을 예측된 예보와 비교합니다. 만약 증명이 예보에서 매우 낮을 것이라고 예측된 도구들을 사용했다면, 시스템은 높은 "놀라움(surprisal)" 점수를 부여합니다. 높은 점수는 "와, 정말 특이한 경로를 택했군요!"라는 의미입니다.

탐정이 발견한 것

연구진은 이 시스템을 위상수학(Topology)(모양과 공간을 다루는 분야)이라는 특정 수학 영역에 대해 테스트했습니다. 그들은 단순히 추측한 것이 아니라, 블라인드 테스트를 실시했습니다. 그들은 100개의 증명 쌍을 가져와 세 명의 인간 수학 전문가에게 보여주었습니다. 전문가들은 각 쌍에서 어떤 증명이 "덜 표준적인"(더 놀라운) 경로를 택했는지 골라야 했습니다. 그들은 점수를 보지 않았으며, 오직 자신의 지식을 사용했습니다.

그 후, 그들은 인간 전문가의 선택과 Prior-Proof의 예측을 비교했습니다. 결과는 다음과 같습니다:

• 76개의 고유한 증명 쌍(일관성을 확인하기 위해 일부는 여러 번 제시됨) 중에서, PriorProof는 53개에서 다수의 인간 전문가 의견과 일치했습니다. 이는 약 **69.7%**입니다.
• 놀랍거나 표준적인 증명의 "교과서적인 사례"로 특별히 선정된 12개의 쌍에 대해서는, PriorProof가 11개를 맞혔습니다(약 91.7%).
• 조금 더 까다로웠던 나머지 64개의 쌍에 대해서는, 42개를 맞혔습니다(약 65.6%).

저자들은 또한 "점수 격차(score gap)", 즉 두 증명 사이의 놀라움 점수 차이를 살펴보았습니다. 그들은 흥미로운 패턴을 발견했습니다. 만약 격차가 매우 컸다면(즉, 한 증명이 다른 증명보다 훨씬 더 놀라웠다면), 시스템은 매우 신뢰할 수 있었으며 인간과 **84.2%**의 확률로 일치했습니다. 하지만 격차가 작았을 때(두 증명이 비슷하게 놀라웠을 때), 시스템은 확신이 떨어졌으며 인간과 **63.2%**만 일치했습니다. 이는 이 도구가 "큰 놀라움"을 포착하는 데는 뛰어나지만, 차이가 미묘할 때는 모호해질 수 있음을 시사합니다.

이것이 아닌 것 (그리고 배제하는 것)

PriorProof가 무엇을 주장하고 있지 않은지 이해하는 것이 매우 중요합니다. 저자들은 이에 대해 매우 명확히 밝히고 있습니다:

• "독창성"이나 "천재성"의 척도가 아닙니다: 높은 점수가 수학자가 천재였다는 것을 의미하지는 않습니다. 단지 그가 기이한 도구의 조합을 사용했다는 것을 의미할 뿐입니다. 때로는 기이한 경로가 찬란한 통찰이 아니라 그저 서투른 우회일 수도 있습니다.
• "중요성"의 척도가 아닙니다: 어떤 증명은 수학계에 엄청나게 중요할 수 있지만, 매우 표준적이고 평범한 도구들을 사용할 수 있습니다. PriorProof는 그 증명이 역사를 바꿨더라도 낮은 점수를 줄 것입니다.
• "표절 탐지기"가 아닙니다: 시스템은 누군가 증명을 베꼈는지 여부에는 관심이 없습니다. 오직 사용된 도구들의 통계적 확률에만 관심을 가집니다.
• "완벽한" 판사가 아닙니다: 저자들은 자신들의 방법이 "해결된 문제"가 아님을 명시적으로 밝힙니다. 실제로 Prior-Proof를 강력한 AI 언어 모델(GPT-5-mini)과 비교했을 때, AI가 인간 전문가와 더 자주 일치했습니다(약 78.9% 대 69.7%). 그러나 그 차이는 어느 한쪽이 확실히 더 낫다고 말할 만큼 통계적으로 유의미하지 않았습니다. Prior-Proof의 진짜 가치는 AI를 이기는 데 있는 것이 아니라, 그것이 투명하다는 데 있습니다. 당신은 점수를 보고 정확히 어떤 도구가 놀라움을 유발했는지 알 수 있지만, AI는 답만 내놓는 "블랙박스"입니다.

결론

Prior-Proof는 수학적 증명이 작성될 당시 그 도구들의 선택이 얼마나 놀라웠는지를 살펴봄으로써, 해당 증명이 얼마나 "비표준적"인지를 측정하는 새로운 기계적 방법입니다. 이 도구는 두 증명 사이의 차이가 명확할 때 인간 전문가와 약 3분의 2의 확률로 일치하며, 차이가 분명할수록 더 잘 작동합니다. 이것이 증명의 아름다움, 중요성, 혹은 탁월함을 말해주지는 않지만, "이 경로는 예상 밖이었다"라고 말해주는 신뢰할 수 있는, 시간 기록이 된 신호를 제공합니다. 이는 연구자들이 연구할 흥미로운 사례를 찾기 위한 도구이지, 수학적 위대함을 판가름하는 최종 심판이 아닙니다. 저자들은 미래에 이를 통해 흥미로운 기계 생성 증명을 식별하거나 수학 라이브러리가 어떻게 진화하는지 연구하는 데 도움을 줄 수 있을 것이라 제안하지만, 현재로서는 그저 놀라움을 측정하는 매우 영리하고 구체적인 방법일 뿐입니다.