PriorProof: A Point-in-Time Measure of Technique Novelty for Formal Proofs

PriorProof measures time-relative nonstandardness in Lean proof routes without a hand-built technique ontology or human labels. It extracts the dependency footprint of an elaborated proof term and scores its weighted surprisal against a retrieval-conditioned, hierarchically smoothed prior built from an earlier quarterly Mathlib snapshot. In a blinded topology study, it matched the majority judgment of retained domain raters on 53 of 76 distinct pairs, or 69.7%. Agreement reached 84.2% in the largest score-gap quartile but was nonmonotone overall. The authors position it as an interpretable signal, not a replacement for experts or language models.