想象一下，你正漫步在一座宏大且不断扩张的数学思想图书馆中。在这座图书馆里，每一本新书（即证明）都必须引用它所使用的旧书。通常情况下，当一位数学家撰写新的证明时，他们会尝试使用当时最常见、最经久不衰的工具。但有时，他们会采取一条奇特的、意想不到的路径，使用一种从未有人想过要混合在一起的奇怪工具组合。一个核心问题是：仅仅通过观察他们所使用的书籍清单，我们如何判断他们的路径是真正令人惊喜的，还是仅仅是一个常规的绕道？这就是形式数学中“新颖性”的谜题。虽然人类可以争论一个证明是否“优雅”或“原创”，但计算机难以处理这些模糊的感觉。它们需要一种硬性的、机械化的方法来衡量一个证明是否采取了一条在当时已知条件下不太可能发生的路径。这正是“惊异度”（surprisal）这一概念引入的地方——你可以把它想象成一种衡量标准，让图书馆在看到证明时发出感叹：“等等，我真没想到你会用那个特定的工具来做这项工作！”

于是有了 PriorProof，一个旨在充当“时空旅行图书管理员”的新工具。它并不询问人类：“这个证明是否聪明？”，而是向系统提出一个冷酷而硬性的问题：“如果将图书馆冻结在这一证明编写的准确时刻，其所使用的工具清单会有多令人惊讶？”研究人员构建了一个系统，该系统可以读取一个形式化证明（使用名为 Lean 的语言编写），剥离掉华丽的格式，并创建一个由该证明所使用的特定数学机制构成的“足迹”。然后，它回到过去，回到该证明存在之前的图书馆快照中。它会问道：“基于那个时期具有相似目标的其他证明，有人使用这些特定工具的可能性有多大？”如果答案是“极不可能”，那么该证明就会获得一个很高的“新颖性得分”。研究发现，这种机械化的得分通常能与人类专家达成一致，即在两者关于某个证明是否采取了更不寻 el 路径的看法一致时，得分差异较大。不过，作者也谨慎地指出，这并不是解决一切问题的魔杖；它是一个有用的信号，主要在两个证明之间的差异非常明显时最为有效，它衡量的不是数学的“美感”或“重要性”，而仅仅是路径的“出人意料程度”。

时空旅行图书管理员

想象你是一名侦探，试图弄清楚一名窃贼是否使用了一种从未见过的秘密方法来破解保险箱。你无法询问窃贼当时的想法，但你可以观察他们留下的工具。PriorProof 就是那位侦探，只不过它是针对数学证明的。它不在乎窃贼的动机或劫案看起来多么酷炫，它只关心解决问题所使用的工具（数学常数和引理），以及这些工具在那个时代是否属于奇特的选择。

这个“魔术表演”的具体步骤如下：

1. 足迹（The Footprint）： 当数学家在 Lean（一种用于数学的计算机语言）中编写证明时，计算机将其转化为一份包含其使用的每一个工具的详尽列表。PriorProof 获取此列表并对其进行清理，将相似的工具归类为“家族”（例如，将所有的锤子归为一类，或将所有的螺丝刀归为一类）。这就是“足迹”。
2. 时光机（The Time Machine）： 系统随后穿越回过去。它抓取了该证明编写之前整个数学库的一个快照。它查看了那个时期正在尝试解决类似问题的所有其他证明。
3. 预测（The Prediction）： 利用一个智能计算机模型（语言模型），它会预测：“如果我在那个时候编写这个问题的证明，我可能会使用哪些工具？”它建立了一个“先验”预期，就像是数学工具的天气预报。
4. 惊异得分（The Surprise Score）： 最后，它将实际使用的工具与预测进行对比。如果证明使用的工具是预测中认为极不可能使用的（低概率），系统就会给出一个很高的“惊异度”得分。高分意味着：“哇，那真是条奇怪的路径！”

侦探的发现

研究人员在数学库的一个特定部分——拓扑学（涉及形状与空间的研究）上测试了这个系统。他们没有仅凭直觉，而是设计了一个盲测。他们选取了 100 对证明，并展示给三位人类数学专家。专家们必须选出每一对中哪一个证明采取了“较不标准”（更令人惊讶）的路径。他们看不到得分，仅凭大脑判断。

随后，他们将人类专家的选择与 PriorProof 的预测进行了对比。结果如下：

• 在 76 个独特的证明对中（部分对经过多次展示以检查一致性），PriorProof 在 53 个对中与大多数人类专家达成了一致。这大约是 69.7%。
• 对于那 12 对专门挑选出来的、作为“教科书级案例”的惊喜 vs 标准证明对，Prior-Proof 答对了 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 是一种全新的、机械化的方法，通过观察证明在编写时的工具选择有多么令人意外，来衡量一个数学证明的“非标准性”。它的表现足以在三分之二的情况下与人类专家达成一致，并且在两个证明之间的差异明显时表现得更好。它不能告诉我们一个证明是否美丽、重要或卓越，但它确实提供了一个可靠的、带有时间戳的信号，告诉我们：“嘿，这条路径出人意料。”它是一个帮助研究人员发现值得研究的有趣案例的工具，而不是对数学伟大程度的最终裁决。作者建议，未来我们可以利用它来帮助识别有趣的机器生成证明，或研究数学库是如何演进的，但就目前而言，它只是一个非常聪明、非常具体的衡量“惊异度”的方法。