膨大な、絶えず拡大し続ける数学的アイデアの図書室を歩いているところを想像してみてください。この図書室では、あらゆる新しい本（証明）は、自らの議論を構築するために使用した古い本を引用しなければなりません。通常、数学者が新しい証明を書くとき、その瞬間に利用可能な最も一般的で使い古された道具を使おうとします。しかし、時には、誰も混ぜ合わせるとは考えもしなかった奇妙な道具の組み合わせを用いて、予期せぬ大胆な道を進むことがあります。大きな疑問は、彼らが使った本のリストを見るだけで、その道が本当に驚くべきものだったのか、それとも単なるルーチン通りの回り道だったのかを、どうすれば判断できるのかということです。これが「新奇性」というパズルです。人間は、ある証明が「優雅」か「独創的」かについて議論できますが、コンピュータはこうした曖昧な感覚を扱うのが苦手です。コンピュータには、その証明が、その時点で知られていたものに対してどれほど起こりにくい経路を辿ったかを測定するための、硬く機械的な方法が必要です。ここで「サプライザル（驚き度）」という概念が登場します。これは、図書室が「待て、この仕事にまさかその特定の道具を使うなんて！」と反応する度合いだと考えてください。

そこで、タイムトラベリング・司書として機能するように設計された新しいツール、PriorProofが登場します。PriorProofは人間に「この証明は巧妙でしたか？」と尋ねるのではなく、冷徹で硬い問いを投げかけます。「もしこの証明が書かれたまさにその瞬間に図書室を凍結させたとしたら、使用された道具のリストはどれほど驚くべきものだったでしょうか？」研究者たちは、形式的な証明（Leanと呼ばれる言語で書かれたもの）を読み込み、装飾的な書式を取り除き、使用された特定の数学的メカニズムの「足跡」を作成するシステムを構築しました。そして、その証明が存在する前の時点の図書室のスナップショットへと時間を遡ります。そしてこう問いかけるのです。「その当時の、似たような目標を持つ他の証明に基づいたとき、誰かがこれらの特定の道具を使う確率はどの程度だったでしょうか？」もし答えが「非常に低い」のであれば、その証明には高い「新奇性スコア」が与えられます。研究では、この機械的なスコアが、特にスコアの差が大きい場合に、どの証明がより特異なルートを辿ったかについて、人間の専門家の意見と一致することが分かりました。ただし、著者らは、これはすべてを解決する魔法の杖ではないことにも注意を促しています。これは、二つの証明の差が明白な場合に最も効果を発揮する有用なシグナルであり、数学の「美しさ」や「重要性」を測るものではなく、単にその経路がいかに予期せぬものであったかを測るものなのです。

タイムトラベリング・司書

あなたが、金庫破りに新しい秘密の手法が使われたかどうかを見極めようとしている探偵だと想像してください。あなたは泥棒の意図を聞き出すことはできませんが、彼が残していった道具を見ることはできます。PriorProofは、数学的証明におけるその探偵です。それは泥棒の動機や、その犯行がいかに格好良かったかには関心がありません。ただ、問題を解決するために使われた道具（数学的な定数や補題）と、それらの道具がその時代にとって奇妙な選択であったかどうかにのみ関心を持ちます。

このマジックの仕組みは、ステップごとに以下の通りです：

1. 足跡（Footprint）: 数学者がLean（数学のためのコンピュータ言語）で証明を書くと、コンピュータはそれを、使用したあらゆる道具の長く詳細なリストへと変換します。PriorProofはこのリストを取り込み、整理し、似たような道具を「ファミリー」（例えば、すべてのハンマーをまとめたり、すべてのドライバーをまとめたりするように）へとグループ化します。これが「足跡」です。
2. タイムマシン: 次に、システムは時間を遡ります。その証明が書かれる直前の、数学ライブラリ全体の全容をスナップショットとして取得します。そして、その時期に似たような問題を解決しようとしていた他のすべての証明を調べます。
3. 予測: スマートなコンピュータモデル（言語モデル）を使用して、「もし私が当時、この問題のための証明を書いていたとしたら、どのような道具を使う可能性が高いか？」を予測します。これは、数学的道具の天気予報のような「事前（プライア）」の期待値を構築します。
4. サプライザル・スコア: 最後に、実際の証明で使用された道具と、その予測を比較します。もし証明が、予測において起こりにくい（確率が低い）とされた道具を使用していた場合、システムは高い「サプライザル（驚き度）」スコアを与えます。高いスコアは、「おや、これは奇妙なルートを選んだな！」ということを意味します。

探偵が見つけたもの

研究者たちは、このシステムをトポロジー（図形や空間を扱う分野）と呼ばれる数学ライブラリの特定のセクションでテストしました。彼らは単に推測したのではなく、ブラインドテストを実施しました。彼らは100組の証明のペアを用意し、それを3人の数学の専門家に提示しました。専門家は、各ペアの中でどちらの証明が「標準的でない（より驚くべき）」ルートを辿ったかを選択しなければなりませんでした。彼らはスコアを見ていません。ただ自分の脳を使って判断したのです。

次に、彼らはPriorProofの予測と、人間の専門家の選択を比較しました。結果は以下の通りです：

• 76組のユニークな証明ペア（一貫性を確認するために同じものが複数回提示されることもありました）のうち、PriorProofは大多数の人間専門家の意見と53組で一致しました。これは約**69.7%**です。
• 明らかに「教科書的な例」として選ばれた12組のペアについては、PriorProofは11回（約91.7%）正解しました。
• よりトリッキーな他の64組については、42組で正解しました（約65.6%）。

著者らはまた、「スコアの差（ギャップ）」、つまり二つの証明のサプライザル・スコアの差についても調査しました。彼らは、明快なパターンを見出しました。ギャップが大きかった場合（つまり、一方の証明がもう一方よりも圧倒的に驚くべきものであった場合）、システムは非常に信頼性が高く、人間の専門家と**84.2%の割合で一致しました。しかし、ギャップが小さかった場合（二つの証明が同程度に驚くべきものであった場合）、システムは確信が持てず、一致率は63.2%**に留まりました。これは、このツールが「大きな驚き」を見つけるのには優れているものの、差異が微妙な場合には曖昧になることを示唆しています。

それが「ではない」もの（および、それが否定するもの）

PriorProofが何を主張しているわけではないのかを理解しておくことは極めて重要です。著者らは以下のように明確に述べています：

• 「独創性」や「天才性」の尺度ではない: 高いスコアは、その数学者が天才であったことを意味しません。単に、彼らが奇妙な道具の組み合わせを使用したことを意味します。時には、奇妙なルートは、輝かしい洞察ではなく、単なる不器拙な回り道であることもあります。
• 「重要性」の尺度ではない: 証明は数学の世界にとって極めて重要であっても、非常に標準的で退屈な道具を使用している場合があります。PriorProofは、たとえその証明が歴史を変えたとしても、低いスコアを与えるでしょう。
• 「盗作検知器」ではない: システムは、誰かが証明をコピーしたかどうかには関心がありません。ただ、使用された道具の統計的な尤度に関心があるのです。
• 「完璧な」審判ではない: 著者らは、彼らの手法が「解決済み」の課題ではないことを明示しています。実際、PriorProofを強力なAI言語モデル（GPT-5-mini）と比較したところ、AIの方が人間専門家とわずかに多く一致しました（約78.9% 対 69.7%）。しかし、その差は、どちらかが決定的に優れていると言えるほど統計的に有意なものではありませんでした。PriorProofの真の価値は、AIに勝つことではなく、その透明性にあります。スコアを見れば、どの道具が驚きをもたらしたのかを正確に特定できますが、AIは答えを出すだけの「ブラックボックス」です。

結論

PriorProofは、数学的証明が書かれた当時の状況において、その道具の選択がいかに驚くべきものであったかを見ることで、数学的証明がどれほど「非標準的」であるかを測定する、新しい機械的な方法です。これは、二つの証明の差が明白な場合には、人間の専門家と約3分の2の割合で一致し、その差が顕著であればさらに精度が高まります。これは証明が美しいか、重要か、あるいは天才的かを教えるものではありませんが、「この経路は予期せぬものであった」という信頼できる、タイムスタンプ付きのシグナルを与えてくれます。これは、研究者が興味深い事例を見つけ出すためのツールであり、数学的偉大さを判定する最終的な審判ではありません。著者らは、将来的にはこれを、興味深い機械生成の証明を見つけたり、数学ライブラリがどのように進化するかを研究したりするために活用できる可能性があると考えていますが、現時点では、驚きを測定するための非常に巧妙で、非常に限定的な方法なのです。