摘要
数学家通常区分那些能够解释、简化或引入非标准路径的证明，但这些判断难以操作化。我们研究了一个故意更狭窄的构造：形式数学中的时间相对证明路径非标准性。对于一个 Lean 定理，PriorProof 提取其详细证明项的依赖足迹，并根据从 Mathlib 的早期季度快照构建的检索条件、分层平滑的先验对该足迹的加权惊讶度进行评分。该方法不需要手工构建的技术本体和人类标签：语句检索是从证明派生的对比对中学习的，而被评分的对象则是从证明项机械读取的。
在一个盲测拓扑研究中，100 个演示收敛为 76 个独特的基础对：12 个经典对显示三次以进行一致性筛选，64 个不同的分层对。在三位保留领域评审者的多数意见中，PriorProof 在 76 对中的 53 对（69.7%，Wilson 95% CI 58.7-78.9%）上达成一致，其中包括 12/12 个经典对（91.7%，64.6-98.5%）和 42/64 个分层对（65.6%，53.4-76.1%）。评分差距四分位数在重复崩溃后呈现非单调特征；最小差距区间的端点为 12/19（63.2%，41.0-80.9%），而最大差距区间的端点为 16/19（84.2%，62.4-94.5%），支持一种端点校准趋势而非解决的阶梯。
在最佳语言模型条件下，PriorProof 在 76 对中达成一致的有 60 对（78.9%，68.5-86.6%）；在配对结果中，PriorProof 自身对 8 对是正确的，而模型自身对 15 对是正确的（确切的双尾 McNemar p = 0.210），因此在这个样本大小下差异并未确立。因此，我们将 PriorProof 视为一种可分解的、时间锚定的信号，其评分差距提供了可解释的可靠性指示，而不是专家或模型判断的替代品。
博主点评： PriorProof 提供了一种创新的方式来量化形式证明中的技术新颖性，不依赖于传统的手动标注，展现了机器学习在形式化数学中的潜力。其评分机制不仅能反映证明的独特性，还为未来的研究提供了可行的可靠性指标，值得在更广泛的数学领域进行探索和应用。