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

# PriorProof: A Point-in-Time Measure of Technique Novelty for Formal Proofs
Source: [https://arxiv.org/html/2607.16997](https://arxiv.org/html/2607.16997)
\(July 2026\)

###### Abstract

Mathematicians distinguish proofs that explain, simplify, or introduce a nonstandard route, but these judgments are difficult to operationalize\. We study a deliberately narrower construct:*time\-relative proof\-route nonstandardness*in formal mathematics\. For aLeantheorem,PriorProofextracts the dependency footprint of its elaborated proof term and scores the weighted surprisal of that footprint under a retrieval\-conditioned, hierarchically smoothed prior built only from an earlier quarterly snapshot ofMathlib\. The method requires no hand\-built technique ontology and no human labels: statement retrieval is learned from proof\-derived contrastive pairs, while the scored object is read mechanically from proof terms\. In a blinded topology study, 100 presentations collapse to 76 distinct underlying pairs: 12 canonical contrasts shown three times for consistency screening and 64 distinct stratified pairs\. Against the majority of three retained domain raters,PriorProofagrees on 53/76 pairs \(69\.7%, Wilson 95% CI 58\.7–78\.9%\), including 11/12 canonical pairs \(91\.7%, 64\.6–98\.5%\) and 42/64 stratified pairs \(65\.6%, 53\.4–76\.1%\)\. Score\-gap quartiles are nonmonotone after repeat collapse; the endpoints are 12/19 \(63\.2%, 41\.0–80\.9%\) in the smallest\-gap bin and 16/19 \(84\.2%, 62\.4–94\.5%\) in the largest, supporting an endpoint\-calibration tendency rather than a resolved staircase\. The best language\-model condition agrees on 60/76 pairs \(78\.9%, 68\.5–86\.6%\); on paired outcomes,PriorProofalone is correct on 8 pairs and the model alone on 15 \(exact two\-sided McNemarp=0\.210p=0\.210\), so the difference is not established at this sample size\. We therefore presentPriorProofnot as a replacement for expert or model judgment, but as a decomposable, time\-anchored signal whose score gap provides an interpretable reliability indicator\.

## 1Introduction

Formal proof libraries expose a record that informal mathematics usually does not: an elaborated term identifies the constants used by a proof, and version control identifies which declarations existed beforehand\. This makes formal mathematics a useful controlled setting for a question that is otherwise hard to pose mechanically: how nonstandard was a proof route relative to the techniques available when the proof was written?

The question concerns one proof virtue among several\. Philosophers and mathematicians have separately analyzed explanation, purity of method, and elegance\(Steiner,[1978](https://arxiv.org/html/2607.16997#bib.bib2); Lange,[2014](https://arxiv.org/html/2607.16997#bib.bib3); Detlefsen and Arana,[2011](https://arxiv.org/html/2607.16997#bib.bib4); Inglis and Aberdein,[2015](https://arxiv.org/html/2607.16997#bib.bib5)\)\. Route novelty is not reducible to any of them\. A routine statement can admit an unexpected proof, while an important theorem can be established through familiar machinery\. The judgment is also temporal: a route that is surprising when introduced may later become standard\.

This distinction is increasingly relevant as learned theorem provers produce formal proofs at scale\(Lampleet al\.,[2022](https://arxiv.org/html/2607.16997#bib.bib13); Yanget al\.,[2023](https://arxiv.org/html/2607.16997#bib.bib11); Xinet al\.,[2024](https://arxiv.org/html/2607.16997#bib.bib14); Lamontet al\.,[2025](https://arxiv.org/html/2607.16997#bib.bib15)\)\. Existing evaluations primarily ask whether a theorem is proved, how much search is required, or how well a model transfers\. They do not directly ask whether a successful proof follows a route that the earlier library would have made likely\. A mechanical signal for that question could support analysis of machine\-generated proofs, historical studies of formal libraries, and high\-recall triage for expert review\.

We introducePriorProof, a quarterly point\-in\-time measure of*proof\-route nonstandardness*forLean4 /Mathlib\(de Moura and Ullrich,[2021](https://arxiv.org/html/2607.16997#bib.bib6); The mathlib Community,[2020](https://arxiv.org/html/2607.16997#bib.bib7)\)\. For a declarationDDwritten at timett, the pipeline \([fig\.˜1](https://arxiv.org/html/2607.16997#S1.F1)\) performs three operations:

1. 1\.extract a weighted dependency\-family footprint from the elaborated proof term;
2. 2\.retrieve similar theorem statements from a library snapshot strictly earlier than the start ofDD’s quarter and construct a smoothed prior over dependency families; and
3. 3\.score the weighted surprisal of the observed footprint under that prior\.

A high score means that the proof uses families of prior machinery that were improbable for earlier theorems with similar statements\. The score is about the proof*as written*; it is not a claim about the author’s originality, the theorem’s importance, or the proof’s explanatory value\.

![Refer to caption](https://arxiv.org/html/2607.16997v1/x1.png)Figure 1:PriorProofseparates what was*expected*from what was*used*\. Statement\-only retrieval over a pre\-bin library induces a priorqt​\(f∣D\)q\_\{t\}\(f\\mid D\)over dependency families, while the elaborated proof term yields an observed footprintΦt​\(D\)\\Phi\_\{t\}\(D\)\. Their weighted surprisal is the score\.Our contributions are:

- •a mechanical, annotation\-free definition of time\-relative proof\-route nonstandardness as dependency\-footprint surprisal;
- •a temporal leakage discipline in which retrieval, family support, reuse counts, and encoder fine\-tuning are restricted to pre\-bin data;
- •an empirical study onMathlibtopology, including mechanical validation, a blinded three\-rater comparison, and an identically prompted language\-model baseline; and
- •evidence for an*endpoint\-calibration tendency*: the smallest score\-gap bin is statistically compatible with chance and the largest has the highest agreement point estimate, but intervals are wide at this sample size\.

The headline result should be read narrowly\. Overall agreement with the three\-rater majority is 53/76 \(69\.7%, Wilson 95% CI 58\.7–78\.9%\), and the broad stratified subset is 42/64 \(65\.6%, 53\.4–76\.1%\)\. The canonical behavior check is 11/12 \(91\.7%, 64\.6–98\.5%\), but its distinct sample is small and its interval wide\. The strongest conclusion is not universal ranking accuracy but a candidate reliability indicator in this sample: the absolute score gap\. To our knowledge, prior work has not scored an existing formal proof by the surprisal of its dependency footprint under a statement\-conditioned prior restricted to the library’s earlier state\. This is an operationalization of one component of technique novelty, not a complete theory of mathematical novelty\.

## 2Related work

#### Premise selection and retrieval\.

Learning\-assisted premise selection ranks prior facts that may help prove a target theorem, from hammer\-style systems for Isabelle/HOL to neural retrieval in large formal corpora\(Blanchetteet al\.,[2016](https://arxiv.org/html/2607.16997#bib.bib8); Irvinget al\.,[2016](https://arxiv.org/html/2607.16997#bib.bib9); Bansalet al\.,[2019](https://arxiv.org/html/2607.16997#bib.bib10)\)\. LeanDojo combines retrieval with language\-model proof search inLean\(Yanget al\.,[2023](https://arxiv.org/html/2607.16997#bib.bib11)\), while miniCTX studies proving with evolving, long\-form context and releasesntp\-toolkitfor extractingLeandata\(Huet al\.,[2024](https://arxiv.org/html/2607.16997#bib.bib12)\)\.PriorProofuses retrieval for a different estimand: not to propose a proof, but to define what dependency families an earlier library would have made expected for a statement\.

#### Learned theorem proving\.

Neural provers have advanced through learned proof search, retrieval augmentation, synthetic data, and diversity\-aware search\(Lampleet al\.,[2022](https://arxiv.org/html/2607.16997#bib.bib13); Yanget al\.,[2023](https://arxiv.org/html/2607.16997#bib.bib11); Xinet al\.,[2024](https://arxiv.org/html/2607.16997#bib.bib14); Lamontet al\.,[2025](https://arxiv.org/html/2607.16997#bib.bib15)\)\. These systems motivate the evaluation question addressed here: conditional on success, did a model recover a standard route or use unexpectedly different machinery?PriorProofis model\-agnostic after a proof has been checked byLean\.

#### Formal\-library structure and proof dependencies\.

Lean andMathlibprovide the elaborated objects and library organization on which our extractor operates\(de Moura and Ullrich,[2021](https://arxiv.org/html/2607.16997#bib.bib6); The mathlib Community,[2020](https://arxiv.org/html/2607.16997#bib.bib7)\)\. LeanDojo and miniCTX demonstrate large\-scale extraction and temporally aware theorem\-proving datasets\(Yanget al\.,[2023](https://arxiv.org/html/2607.16997#bib.bib11); Huet al\.,[2024](https://arxiv.org/html/2607.16997#bib.bib12)\)\. Work on proof structures and the network organization ofMathlibstudies dependency graphs as mathematical objects\(Wernhard and Bibel,[2024](https://arxiv.org/html/2607.16997#bib.bib26); Liet al\.,[2026](https://arxiv.org/html/2607.16997#bib.bib25)\); concurrent work such as TheoremGraph uses graph representations to connect formal and informal mathematics\(Kurganet al\.,[2026](https://arxiv.org/html/2607.16997#bib.bib24)\)\. Our target differs: a declaration\-level, time\-sliced surprisal score for the route taken by an existing proof\.

#### Novelty and surprisal\.

Surprisal is the negative log probability of an observation\(Shannon,[1948](https://arxiv.org/html/2607.16997#bib.bib1)\)\. Related operationalizations appear in anomaly detection\(Ruffet al\.,[2021](https://arxiv.org/html/2607.16997#bib.bib17)\)and bibliometrics, where atypical combinations of references are used as a signal of scientific novelty\(Uzziet al\.,[2013](https://arxiv.org/html/2607.16997#bib.bib16)\)\. The analogy is useful but incomplete\. A formal proof supplies mechanically checked dependencies rather than author\-selected citations, and a versioned library permits a stricter temporal counterfactual\.

#### Proof virtues\.

Work on mathematical explanation, purity, and aesthetic appraisal emphasizes that proof quality is multidimensional\(Steiner,[1978](https://arxiv.org/html/2607.16997#bib.bib2); Lange,[2014](https://arxiv.org/html/2607.16997#bib.bib3); Detlefsen and Arana,[2011](https://arxiv.org/html/2607.16997#bib.bib4); Inglis and Aberdein,[2015](https://arxiv.org/html/2607.16997#bib.bib5)\)\. We do not collapse these virtues into one score\.PriorProoftargets only whether the proof route uses unexpectedly distributed prior machinery\.

## 3Method

### 3\.1Temporal object and notation

LetDDbe a theorem declaration with statementxDx\_\{D\}, elaborated proof termpDp\_\{D\}, and commit timett\. Letb​\(t\)b\(t\)be the beginning of the quarterly snapshot bin containingtt, and let

ℒ<b​\(t\)=\{E:time⁡\(E\)<b​\(t\)\}\\mathcal\{L\}\_\{<b\(t\)\}=\\\{E:\\operatorname\{time\}\(E\)<b\(t\)\\\}\(1\)be the library available to the implementation\. Conceptually, the desired counterfactual is the library immediately beforett; the implementation uses the stricter pre\-bin slice in[eq\.˜1](https://arxiv.org/html/2607.16997#S3.E1)\. This prevents target leakage but excludes declarations introduced earlier in the same quarter, so temporal resolution is quarterly rather than commit\-exact\.

### 3\.2From a proof term to a dependency footprint

Surface tactics such assimporlinarithare poor units of technique: they are syntactic interfaces whose mathematical work depends on the lemmas and instances eventually elaborated\. At the opposite extreme, raw constant names are too specific and over\-credit proofs that create fresh helper objects\. We therefore construct a weighted family footprint in four stages\.

#### Actual\-use extraction\.

For each compiled theorem value, the proof\-term backend callsLean’sgetUsedConstants\. This yields constants actually referenced by the declaration’s elaborated value, rather than all imports of its source file\. In the reported run, every normalized dependency reference is marked as proof\-term\-derived \([section˜4](https://arxiv.org/html/2607.16997#S4)\)\.

#### Deterministic filtering\.

A documented filter removes generated recursors, coercions, routine typeclass and notation plumbing, and common tactic boilerplate\. This is a design choice rather than a theorem about mathematical relevance; filter variants are therefore part of the validation interface\.

#### Established\-machinery frontier\.

A proof\-local or recently introduced dependency is recursively replaced by the older dependencies on which it rests until the traversal reaches declarations established inℒ<b​\(t\)\\mathcal\{L\}\_\{<b\(t\)\}\. Establishment is defined by a pre\-bin reuse\-count threshold\. Reuse is never counted in a snapshot containing the target, preventing a batch of co\-introduced declarations from making one another appear established\. Surviving dependencies receive deterministic inverse\-frequency\-style weights from the implementation\.

#### Family backoff\.

Each surviving constant maps to the finest family with at least five pre\-bin occurrences, backing off through declaration, parent namespaces, module, library area, and global levels\. This reduces accidental novelty from rare names without introducing a separately annotated technique taxonomy\. The resulting footprint is

Φt​\(D\)=\{\(fi,wi\)\}i=1mD,wi\>0,\\Phi\_\{t\}\(D\)=\\\{\(f\_\{i\},w\_\{i\}\)\\\}\_\{i=1\}^\{m\_\{D\}\},\\qquad w\_\{i\}\>0,\(2\)wherefif\_\{i\}is a supported dependency family andwiw\_\{i\}is its deterministic footprint weight\.

### 3\.3Statement encoder and pre\-bin retrieval

The retriever embeds only the theorem statementxDx\_\{D\}, neverpDp\_\{D\}\. It begins fromsentence\-transformers/all\-MiniLM\-L6\-v2, a compact sentence\-embedding model descended from MiniLM\(Reimers and Gurevych,[2019](https://arxiv.org/html/2607.16997#bib.bib18); Wanget al\.,[2020](https://arxiv.org/html/2607.16997#bib.bib19)\)\. Contrastive fine\-tuning examples are mined mechanically from the pre\-bin formal corpus\. Positive pairs share signals such as dependency families, downstream users, major dependency links, or namespace\-local symbols\. Hard negatives include lexically similar statements with disjoint families, cross\-module false friends, and statements with similar heads but different shapes\. Training uses Multiple Negatives Ranking Loss for one epoch with batch size 64, AdamW at learning rate2×10−52\\times 10^\{\-5\}, 10% linear warmup, a 256\-token maximum sequence length, shuffled batches, and hard negatives enabled\. The device is selected automatically by Sentence\-Transformers\. No training seed was set, so the learned embedding is nondeterministic across runs\.

Because the training signal is proof\-derived, an encoder trained on future proofs could leak future dependency structure into retrieval\. The pipeline therefore mines pairs and trains a separate encoder for each scoreable bin using only declarations before that bin\. A cheaper shared\-encoder path is permitted by the code only after a neighbor\-stability test; in the reported run, cross\-bin overlap was 0\.43 against a prespecified 0\.75 threshold, so per\-bin encoders were enforced\.

For targetDD, the encoder retrievesk=32k=32statement\-nearest theorems fromℒ<b​\(t\)\\mathcal\{L\}\_\{<b\(t\)\}by cosine similarity ofℓ2\\ell\_\{2\}\-normalized embeddings\. Neighbor evidence is weighted by a softmax with fixed temperature 0\.2\. Their proofs contribute empirical mass to the families they used\. Retrieval is thus conditioned on the target statement while remaining independent of the target proof\.

### 3\.4Hierarchically smoothed prior

Letqr,tq\_\{r,t\},qn,tq\_\{n,t\},qm,tq\_\{m,t\}, andqg,tq\_\{g,t\}denote empirical family distributions derived respectively from retrieved neighbors, the target namespace, the target module, and the full pre\-bin library\. The prior has the mixture form

qt​\(f∣D\)=λr​qr,t​\(f∣D\)\+λn​qn,t​\(f∣D\)\+λm​qm,t​\(f∣D\)\+λg​qg,t​\(f\),q\_\{t\}\(f\\mid D\)=\\lambda\_\{r\}q\_\{r,t\}\(f\\mid D\)\+\\lambda\_\{n\}q\_\{n,t\}\(f\\mid D\)\+\\lambda\_\{m\}q\_\{m,t\}\(f\\mid D\)\+\\lambda\_\{g\}q\_\{g,t\}\(f\),\(3\)with nonnegative weights summing to one and additive smoothing parameterα\>0\\alpha\>0\. The components are computed from pre\-bin weighted family counts\. Mixture weights andα\\alphaare selected by chronological log likelihood: hide each eligible proof, build its prior only from earlier declarations, and maximize the probability assigned to the families the proof actually used\. This fitting objective is predictive rather than tuned to the human study\.

### 3\.5Novelty score and pairwise confidence signal

ThePriorProofscore is the realized weighted surprisal of the footprint:

St​\(D\)=∑i=1mDwi​\[−log⁡qt​\(fi∣D\)\]\.S\_\{t\}\(D\)=\\sum\_\{i=1\}^\{m\_\{D\}\}w\_\{i\}\\big\[\-\\log q\_\{t\}\(f\_\{i\}\\mid D\)\\big\]\.\(4\)This is not a cross\-entropy against a separate reference distribution; it is the weighted surprisal of the observed families\. Every contribution can be decomposed into a named dependency family, its weight, and its pre\-bin probability\.

For a pair\(A,B\)\(A,B\), the metric selects the proof with larger score\. Its internal confidence signal is the absolute score gap

Δ​\(A,B\)=\|StA​\(A\)−StB​\(B\)\|\.\\Delta\(A,B\)=\|S\_\{t\_\{A\}\}\(A\)\-S\_\{t\_\{B\}\}\(B\)\|\.\(5\)The human study tests whether larger gaps correspond to more reliable pairwise judgments\.

### 3\.6Leakage discipline

The pre\-bin slice mechanically excludes the target, its formal descendants, future retrieval candidates, future reuse counts, and future family\-support evidence\. Two residual channels require separate treatment\.

First, the pretrained encoder initialization can contain parametric knowledge of later mathematics\. This cannot be removed by slicing\. The counterfactual\-retrieval probe replaces relevant retrieved context with unrelated pre\-bin context; a score that changes demonstrates dependence on retrieved evidence, whereas invariance flags cases in which retrieval is not materially influencing the output\. The probe measures sensitivity but does not prove the absence of parametric memory\.

Second, proof\-derived encoder fine\-tuning can transmit future dependency patterns\. Per\-bin training fromℒ<b​\(t\)\\mathcal\{L\}\_\{<b\(t\)\}addresses this channel mechanically\. A remaining unobservable channel is diffuse human influence: a later proof may use an idea learned fromDDwithout a dependency edge toDD\. Such influence would make an earlier route appear more standard than it was, biasing the metric downward rather than manufacturing novelty\.

### 3\.7Directness assumption and redundancy backstop

PriorProofscores the proof as written\. It is meaningful when the proof is reasonably direct, rather than padded with an eliminable detour that re\-derives an available theorem through exotic machinery\. The pipeline implements two redundancy checks againstℒ<b​\(t\)\\mathcal\{L\}\_\{<b\(t\)\}: a top\-level path for wrappers that reduce to a single prior theorem, and a nested path that compares sub\-derivation conclusions with prior statements up to trivial equivalence\. Both paths pass a constructed re\-derivation fixture\. The live proof\-term backend, however, emits top\-level dependency sets but no proof subterms, so the nested path is dormant in the reported corpus\. This backstop catches redundancy with the existing library, not arbitrary baroqueness around genuinely new intermediates\.

### 3\.8Scope of the construct

The score omits several phenomena often called novelty\. It is blind to novelty residing primarily in definitions; it measures unexpected dependency families rather than unexpected*connections*between otherwise familiar families; and it does not target elegance, explanatory value, difficulty, importance, or authorship credit\. Point\-in\-time scoring also means later simplification does not retroactively change the score assigned at introduction\.

## 4Experimental setup

### 4\.1Corpus and provenance

The study uses target declarations underMathlib\.Topology\.MetricSpace,Mathlib\.Topology\.Compactness, andMathlib\.Topology\.Separation, with neighboring topology modules retained as support context\.[Table˜1](https://arxiv.org/html/2607.16997#S4.T1)summarizes the corpus\. The 2023Q4 snapshot is the first conditioning baseline; targets in 2024Q1–2024Q2 are scoreable because they have an earlier in\-manifest corpus\. Each snapshot is pinned to the latest commit on theMathlibmasterbranch at or before the quarter start: 2023Q4 on 2023\-10\-01, 2024Q1 on 2024\-01\-01, and 2024Q2 on 2024\-04\-01\. Full commit hashes andLeantoolchains are reported in[appendix˜B](https://arxiv.org/html/2607.16997#A2)\.

Table 1:Corpus and extraction summary\. Support declarations condition retrieval and smoothing but are not part of the reported target population\.QuantityCountScoped declarations10,132Target declarations2,026Support declarations8,106Scored post\-baseline targets248Normalized proof\-term dependency references, full extraction4,707,281Proof\-term dependency references, topology scope264,914Records with extracted proof subterms0The extraction report recordsbackend: proof\-term; all 4,707,281 normalized dependency references are taggedsource: proof\_term\. The absence of proof subterms explains why nested redundancy detection is fixture\-validated but inactive on live data\.

### 4\.2Mechanical validation

We evaluate six properties before comparing with raters: \(i\) chronological likelihood of observed versus randomly chosen families; \(ii\) retrieval and smoothing ablations; \(iii\) counterfactual\-retrieval sensitivity; \(iv\) score sensitivity to footprint construction; \(v\) redundancy\-fixture behavior; and \(vi\) correlation between score and family\-backoff depth\. The reuse threshold is swept over\{3,5,8,13\}\\\{3,5,8,13\\\}with a bucket\-identity diagnostic\. Because every declaration maps to identical final family buckets in this sweep, it is reported as inert rather than as independent robustness evidence\.

### 4\.3Blinded human study

The evaluation packet contains 100 blinded*presentations*of 76 distinct underlying proof pairs\. Twelve hand\-selected canonical contrasts are each shown three times, giving 36 presentations, and 64 score\-gap\-stratified corpus pairs are each shown once\. The canonical repeats were included deliberately as a consistency instrument rather than as independent outcome replicates\. For each side, raters see the declaration name, theorem statement, proof narrative, and completeLeansource\. They do not see scores, family probabilities, or canonical/stratified labels\. The prompt is:

> *Which proof uses the less standard mathematical route to its result?*

The wording deliberately avoids asking which proof is more “original\.”

Outcome analysis is performed on the 76\-pair universe\. Each left/right choice is first normalized to the underlying proof identity, and each distinct pair is assigned a canonical binary orientation\. For each judge, the primary label for a repeated canonical pair is the majority choice across its three presentations; the 64 singleton pairs pass through unchanged\. No collapse ties occur for any retained rater or language\-model condition\. A first\-presentation\-only sensitivity analysis changes every reported aggregate by at most one pair\.PriorProofis deterministic across presentations by construction\.

Four topology mathematicians completed the packet\. One response set was screened post hoc after the sequence described in[section˜5\.2](https://arxiv.org/html/2607.16997#S5.SS2); all headline outcome statistics use the three retained raters\. The screening response is reported separately and never enters the majority labels used below\.

The task was conducted by an independent researcher with no institutional affiliation requiring institutional review\. It involved expert judgments over public mathematical content, posed minimal risk, and collected no sensitive research data\. Raters were told that their responses would be used in research\. Names and payment details were collected only for recruitment and payment, retained privately, and omitted from every released artifact\. Each completed packet was compensated at $1,500; the estimated completion time was roughly two hours \(about $750/hour, and $500/hour under a three\-hour completion assumption\)\. Every recruited rater was paid in full, including the screened rater\. Human and model responses remain private because the consent language did not address public release\.

### 4\.4Language\-model baseline

Judgments were collected through the OpenAI Responses API under the provider model namesgpt\-5andgpt\-5\-mini, crossed with two prompt\-strictness variants, producing 400 judgments over the same 100 blinded presentations\. No date\-pinned model identifiers were available in the run records, and temperature was not explicitly set, so the API default applied\. For each condition, repeated presentations are collapsed by the same proof\-identity and majority procedure used for human judges\. A four\-condition majority vote is then formed on the 76 distinct pairs, excluding 2–2 ties\. Requests and responses for the designated run and a second identical\-setting run are retained privately; the two runs of the best logged condition disagreed on 17 of the 100 presentations\. Execution dates were not logged, so the baseline should be interpreted as a contemporaneous provider\-name comparison rather than an exactly reproducible model benchmark\. Proof narratives shown to both human and model judges were generated withgpt\-5\-miniunder a system instruction that prohibited formal\-system metadata, evaluation vocabulary, and judgments about whether a route was standard or surprising; outputs were checked against forbidden terms and patterns and retried on failure\. We cite the model\-family documentation for context\(OpenAI,[2025](https://arxiv.org/html/2607.16997#bib.bib23)\), not as evidence for the reported judgments\.

### 4\.5Statistics and availability

Agreement proportions and Wilson score intervals are computed on distinct underlying pairs after repeat collapse\(Wilson,[1927](https://arxiv.org/html/2607.16997#bib.bib20)\)\. Pairwise rater agreement is reported with Cohen’sκ\\kappa\(Cohen,[1960](https://arxiv.org/html/2607.16997#bib.bib21)\); three\-rater agreement uses Fleiss’κ\\kappa\(Fleiss,[1971](https://arxiv.org/html/2607.16997#bib.bib22)\)\. Allκ\\kappacalculations use a canonical binary orientation defined separately for each proof pair\. The comparison betweenPriorProofand the best language\-model condition uses an exact two\-sided McNemar test on the same 76 distinct pairs\. Wilson intervals remain descriptive because all pairs share a small rater panel and the canonical subset is hand\-selected, but repeated presentations are not treated as independent outcomes\.

Code and the blinded study\-packet machinery are available under the MIT License at[https://github\.com/neelsomani/priorproof](https://github.com/neelsomani/priorproof)\. The results reported in this paper correspond to Git tag[v1\.0\-arxiv](https://github.com/neelsomani/priorproof/tree/v1.0-arxiv)\. Human and language\-model response data are not public because the rater disclosure did not cover public release; consequently, the released pipeline reproduces the method and can generate a fresh study through the same tooling, but it does not reproduce the exact reported judgment aggregates\.

## 5Results

### 5\.1Mechanical validation

Observed footprint families receive higher chronological probability than random alternatives: mean log probability−10\.132\-10\.132versus−12\.056\-12\.056, a margin of 1\.924 nats over 5,629 footprint items\. The topology\-specific fit is strongly retrieval\-weighted, whereas a broader all\-Mathlibfit is more balanced \([table˜2](https://arxiv.org/html/2607.16997#S5.T2)\)\. This difference cautions against treating the topology mixture as universal\.

Table 2:Chronologically fitted prior mixtures\. The topology slice relies heavily on retrieved neighbors; the broader fit assigns more mass to structural backoff\.FitRetrievalNamespaceModuleGlobalα\\alphaTopology0\.900\.040\.030\.030\.05AllMathlib0\.400\.250\.200\.150\.10Ablations raise observed\-footprint surprisal on average, but effects are uneven across declarations \([table˜3](https://arxiv.org/html/2607.16997#S5.T3)\)\. The no\-namespace ablation is especially weak: its mean is positive but only 40% of declarations move upward, consistent with namespace smoothing acting mostly as a small floor in this slice\. The counterfactual\-retrieval probe has no empty\-retrieval rows among the 248 scored targets; mean signed sensitivity is 1\.31 and mean absolute sensitivity is 1\.59\. Backoff depth is essentially uncorrelated with score \(r=0\.046r=0\.046,n=992n=992family observations\)\. There are no live redundancy hits\. All 10,132 scoped declarations have identical family buckets across reuse thresholds 3, 5, 8, and 13\.

Table 3:Ablations relative to the fitted topology prior\. PositiveΔ\\Deltameans greater surprisal on observed footprints after removing a component\.AblationMeanΔ\\DeltasurprisalFraction withΔ\>0\\Delta\>0Global only\+5\.490\.65No retrieval\+1\.850\.52No module\+0\.710\.51No namespace\+0\.340\.40
### 5\.2Rater screening and repeat consistency

The quality screen was developed post hoc\. Outcome statistics were initially computed with all four raters\. One response set was then flagged by a median response time of roughly seven seconds per presentation for a packet designed around 90–120 seconds of reading, by weak agreement with the other human and automated judges, and by the rater’s subsequent explanation\. The order\-normalized repeat\-consistency statistic was constructed last and became the criterion of record\.

For each triplicated canonical pair, choices are normalized to proof identity\. The within\-judge majority identifies the reference choice for that group\. The vote score counts how many of the 36 presentations match that majority, so its mechanical floor is 24/36; a random binary responder has expectation 27/36\. The group score counts fully consistent triplicates, with random\-response expectation 3/12\.[Table˜4](https://arxiv.org/html/2607.16997#S5.T4)reports the result\.

Table 4:Order\-normalized repeat consistency\. Vote counts are matches to each judge’s within\-group majority; group counts are fully consistent triplicates\. The language\-model row gives the range over all four model–prompt conditions\.JudgeMajority\-match votes /36Fully consistent groups /12PriorProof\(by construction; order\-invariant\)3612Retained rater A3511Retained rater B3511Retained rater C339Four language\-model conditions \(range\)33–359–11Screened rater284Random binary response baselinefloor 24;𝔼=27\\mathbb\{E\}=27𝔼=3\\mathbb\{E\}=3The screened response yields 28/36 majority\-match votes and 4/12 fully consistent groups\. Under random binary responding,Pr⁡\(X≥4\)=0\.351\\Pr\(X\\geq 4\)=0\.351for the group count, so this statistic alone does not strongly reject chance and lies within roughly one standard deviation of its expectation\. The retained raters yield 35, 35, and 33 votes and 11, 11, and 9 fully consistent groups; even the lowest retained group count has chance probability approximately4×10−44\\times 10^\{\-4\}\. The screen cannot distinguish a random responder from a fixed position\-biased responder, but either pattern indicates failure to engage with proof identity; the seven\-second median supplies independent engagement evidence\. All headline results use the three retained raters\. The language\-model conditions yield 33–35 votes and 9–11 groups, so the language\-model baseline survives the study’s own consistency instrument and cannot be dismissed on the same ground\.

### 5\.3Rater agreement

On the 76 distinct pairs, the three retained rater\-pair Cohen coefficients are0\.5480\.548,0\.4610\.461, and0\.5500\.550\. Fleiss’κ\\kappais0\.5190\.519overall,0\.7500\.750on the 12 canonical pairs, and0\.4760\.476on the 64 stratified pairs\. All three raters are unanimous on 49/76 pairs \(64\.5%, Wilson 95% CI 53\.3–74\.3%\)\. Thus, the broad stratified subset is a moderately noisy construct target rather than ground truth\. Theκ\\kappacalculation uses a per\-pair binary orientation; treating proof identities as global categories would make chance agreement artificially tiny and inflateκ\\kappatoward raw agreement\.

### 5\.4Agreement with the rater majority

[Table˜5](https://arxiv.org/html/2607.16997#S5.T5)reports agreement with the three\-rater majority after canonical repeats are collapsed\.PriorProofselects the majority\-preferred route on 53/76 distinct pairs \(69\.7%, Wilson 95% CI 58\.7–78\.9%\)\. Agreement is 11/12 on the canonical behavior check \(91\.7%, 64\.6–98\.5%\) and 42/64 on the broader stratified sample \(65\.6%, 53\.4–76\.1%\)\. The canonical point estimate is high, but its interval is wide because the distinct canonical set contains only 12 pairs\.

Table 5:Agreement with the three\-rater majority on distinct underlying pairs after repeat collapse\. The canonical set is a behavior check; the stratified set is the broader generalization estimate\.SubsetCorrectAgreementWilson 95% CIAll distinct pairs53/7669\.7%\[58\.7%, 78\.9%\]Canonical11/1291\.7%\[64\.6%, 98\.5%\]Stratified42/6465\.6%\[53\.4%, 76\.1%\]
### 5\.5Endpoint\-calibration tendency by score gap

![Refer to caption](https://arxiv.org/html/2607.16997v1/x2.png)Figure 2:Agreement with the three\-rater majority by quartile of absolute score gap on 76 distinct pairs \(n=19n=19per bin\)\. Error bars are Wilson 95% intervals\. After repeated canonical presentations are collapsed, the interior bins are nonmonotone; the evidence is an endpoint tendency, not a resolved staircase\.After collapse, the 76 distinct pairs divide evenly into four score\-gap bins of 19\. Agreement is 12/19 in the smallest\-gap bin \(63\.2%, Wilson 95% CI 41\.0–80\.9%\), 11/19 in the second \(57\.9%, 36\.3–76\.9%\), 14/19 in the third \(73\.7%, 51\.2–88\.2%\), and 16/19 in the largest \(84\.2%, 62\.4–94\.5%\)\. The interior point estimates are nonmonotone, and all intervals are wide\. The evidence therefore supports only an endpoint tendency: the smallest\-bin interval includes chance, while the largest bin has the highest point estimate and excludes 50%\. High\-gap comparisons are the more reliable regime in this sample, but no resolved four\-step calibration staircase is established\.

### 5\.6Language\-model comparison

The best logged language\-model condition \(gpt\-5\-mini, strict prompt\) agrees with the rater majority on 60/76 distinct pairs \(78\.9%, Wilson 95% CI 68\.5–86\.6%\)\. The four\-condition majority, excluding five 2–2 ties, agrees on 57/71 non\-tied pairs \(80\.3%, 69\.6–87\.9%\)\. Both point estimates are nominally higher thanPriorProof’s 53/76 result \(69\.7%, 58\.7–78\.9%\)\.

On the 76 paired outcomes for the best condition,PriorProofalone is correct on 8 pairs and the language\-model judge alone is correct on 15\. The exact two\-sided McNemar test givesp=0\.210p=0\.210; the discordant counts andpp\-value are identical under the primary majority collapse and the first\-presentation\-only sensitivity rule\. The paired test therefore does not resolve the difference at this sample size, but its direction is clear: the language\-model judge has the higher nominal pairwise\-agreement estimate\. As[table˜4](https://arxiv.org/html/2607.16997#S5.T4)shows, every language\-model condition also survives the repeat\-consistency screen\. Across two identical\-setting API runs, the best condition changes its decision on 17 of 100 presentations, a presentation\-level nondeterminism diagnostic rather than a distinct\-pair accuracy result\.PriorProof’s value consequently rests on properties the model judgment lacks: a fixed point\-in\-time corpus, mechanical decomposition, and an explicit score\-gap signal\.

## 6Discussion

#### What the calibration result buys\.

A scalar ranking metric is most useful when it indicates when its own ordering is fragile\. In this study, the largest score\-gap bin has the highest agreement point estimate and excludes chance, while the smallest\-gap bin does not; the two interior bins are nonmonotone and the intervals are wide\. This supports a selective workflow in which high\-gap contrasts receive priority for automatic surfacing and low\-gap cases are deferred to domain judgment\. It does not establish a universal threshold, and a second library area is required before treating the pattern as transferable\.

#### Interpretability\.

A score decomposes into family\-level termswi​\[−log⁡qt​\(fi∣D\)\]w\_\{i\}\[\-\\log q\_\{t\}\(f\_\{i\}\\mid D\)\]\. This makes it possible to inspect whether a high score is driven by a genuinely unexpected mathematical area, a coarse backoff family, or an implementation artifact\. The backoff\-depth diagnostic reduces one obvious confound, but interpretability does not make the family hierarchy uniquely correct\.

#### Relation to learned provers\.

The natural downstream experiment is to score multiple checked proofs of the same theorem: human proofs, model\-generated proofs, and search variants\. Because the score is evaluated after proof checking, it can compare provers without changing their search procedure\. Care is essential, however: machine\-generated proofs may exploit detours or library idiosyncrasies more aggressively than curatedMathlibproofs, making normalization and nested redundancy detection prerequisites for strong claims\.

#### Why this is not an originality detector\.

Unexpected dependencies can arise from genuine invention, an awkward proof, a deliberate obfuscation, missing library lemmas, or a mismatch between the target and retrieval corpus\. Conversely, an original conceptual insight can elaborate to standard dependencies\. The measure is therefore evidence about a formal route, not evidence about plagiarism, priority, intent, or deservingness of credit\.

## 7Limitations

#### Construct validity\.

Dependency\-family surprisal is only one component of technique novelty\. The metric misses definitional novelty and connection\-level novelty, and it does not measure explanation, elegance, difficulty, or importance\. The family hierarchy inheritsMathlib’s namespaces and modules, which are organizational rather than a canonical ontology of mathematical technique\.

#### Temporal precision and leakage\.

The implementation is quarterly\. Using the start of the target’s bin is leakage\-safe but may overstate novelty by omitting legitimate earlier declarations from the same quarter\. Pretrained encoder memory is measured only indirectly through context sensitivity, not eliminated\. Diffuse human\-mediated influence without a formal edge remains unobservable and biases novelty downward\.

#### Proof normalization\.

The score applies to proofs as written\. The live extractor exposes no subterms, leaving nested redundancy detection inactive\. A contrived or machine\-generated proof can inflate its score by importing unusual machinery or taking a long detour\. The zero live\-hit result is evidence about the detector’s visible target class in this curated corpus, not proof that every proof is direct\.

#### Statistical scope\.

The evaluation covers 248 targets in oneMathlibdomain, three retained mathematicians, and 76 distinct comparison pairs\. Only 12 canonical contrasts are distinct; their three presentations are a consistency instrument and must not be treated as separate outcomes\. Counting repeats as observations would overstate both precision and apparent performance\. Agreement is weakest on the 64\-pair stratified subset\. The screening rule was constructed after inspection, and the screened rater’s 4/12 fully consistent groups havePr⁡\(X≥4\)=0\.351\\Pr\(X\\geq 4\)=0\.351under random binary responding; the exclusion therefore also depends on the approximately seven\-second median and the broader engagement evidence\. The score\-gap result is an endpoint tendency with wide intervals, not a resolved calibration curve\.

The language\-model judge has the higher nominal point estimate, survives the same repeat\-consistency instrument, and has 15 paired\-only wins versus 8 forPriorProof; the exact McNemar test does not resolve the difference at this sample size\. The contribution should therefore be judged by the metric’s mechanical provenance, temporal anchoring, decomposition, and candidate reliability signal, not by a claim to match or beat the model judge\. A second library area and a substantially larger distinct canonical set, with repeats retained as a consistency instrument, are structural requirements before any cross\-domain claim\.

#### Baseline and reproducibility metadata\.

TheMathlibcommit hashes,Leantoolchains, encoder hyperparameters, retrieval settings, prior grid, and MIT code license are recorded\. Exact date\-pinned language\-model identifiers and execution timestamps were not logged; encoder package versions, checkpoint hashes, pair\-sampling seeds, and measured hardware/runtime logs were also not retained\. Human and model responses are private, so the released code cannot regenerate the exact reported judgment tables, although item\-level records retained by the author support controlled reanalysis\. These gaps limit exact bitwise reproduction and external audit but do not alter the supplied aggregates\.

#### Adversarial use\.

The metric can be gamed by adding irrelevant rare machinery\. Conversely, coarse backoff can suppress a subtle but meaningful novelty\. It should not be optimized as a standalone reward until proof normalization and gaming tests are substantially stronger\.

## 8Ethics, intended use, and broader impact

PriorProofis intended as a research instrument for analyzing checked formal proofs and prioritizing cases for expert inspection\. Appropriate uses include historical library analysis, comparing proof\-search systems, and selecting high\-gap examples for qualitative study\. Inappropriate uses include automated plagiarism findings, authorship attribution, hiring or promotion decisions, or allocation of mathematical credit\. Such decisions require evidence about provenance, intent, and conceptual contribution that the score does not contain\.

The system processes public formal\-library artifacts\. The expert\-annotation study was conducted by an independent researcher outside an institution requiring review, was minimal risk, and collected no sensitive research data\. Raters were informed that their judgments would be used in research and were compensated $1,500 per completed packet; all four were paid in full\. Names and payment details remain private and no identifying information appears in released artifacts\. Individual responses are withheld because public release was not covered by the rater disclosure\. This protects privacy but limits auditability; a future study should obtain consent for de\-identified release or establish a controlled\-access protocol\.

The main foreseeable negative impact is false authority: a quantitative “novelty” label may be over\-interpreted\. We mitigate this by naming the narrower construct, reporting broad\-pair performance and rater disagreement, exposing the weaker endpoint\-calibration tendency, and explicitly prohibiting person\-level conclusions\. A positive impact is more disciplined evaluation of machine\-generated mathematics\. Rather than treating proof success as the sole outcome, researchers could examine whether successful systems merely reproduce expected dependency patterns or discover routes that merit human attention\. The metric should serve as a hypothesis generator, not an arbiter\.

#### Funding and competing interests\.

This work received no external funding and was self\-funded by the author, including rater compensation\. The author declares no competing interests\.

#### AI\-assistance disclosure\.

Portions of the manuscript prose and analysis scripts were drafted with LLM assistance; all claims, numbers, and citations were verified by the author against primary artifacts and sources\.

## 9Conclusion

We presentedPriorProof, a mechanical signal of quarterly point\-in\-time proof\-route nonstandardness\. The method compares a proof\-term dependency footprint with a statement\-conditioned prior induced solely from an earlierMathlibsnapshot\. On topology, it agrees with a three\-rater majority on 53/76 distinct pairs \(69\.7%, Wilson 95% CI 58\.7–78\.9%\), including 11/12 canonical contrasts \(91\.7%, 64\.6–98\.5%\) and 42/64 stratified pairs \(65\.6%, 53\.4–76\.1%\)\. The largest score\-gap bin has the highest point estimate, 16/19 \(84\.2%, 62\.4–94\.5%\), versus 12/19 \(63\.2%, 41\.0–80\.9%\) in the smallest; the nonmonotone interior bins and wide intervals make this an endpoint tendency rather than a resolved calibration curve\. The language\-model judge has a higher nominal estimate, and an exact paired test does not resolve the difference at this sample size\. The result supports cautious selective use of the metric when score gaps are large, not unqualified ranking of arbitrary proofs\. Future work should add finer\-grained temporal slicing, subterm\-aware proof normalization, connection\-level priors, a second mathematical domain, a larger distinct canonical set, preregistered rater screening, and a consented or controlled\-access route for paired human/model judgments\.

## References

- HOList: an environment for machine learning of higher order logic theorem proving\.InProceedings of the 36th International Conference on Machine Learning,Proceedings of Machine Learning Research, Vol\.97,pp\. 454–463\.Cited by:[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px1.p1.1)\.
- J\. C\. Blanchette, D\. Greenaway, C\. Kaliszyk, D\. Kühlwein, and J\. Urban \(2016\)A learning\-based fact selector for Isabelle/HOL\.Journal of Automated Reasoning57\(3\),pp\. 219–244\.External Links:[Document](https://dx.doi.org/10.1007/s10817-016-9362-8)Cited by:[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px1.p1.1)\.
- J\. Cohen \(1960\)A coefficient of agreement for nominal scales\.Educational and Psychological Measurement20\(1\),pp\. 37–46\.External Links:[Document](https://dx.doi.org/10.1177/001316446002000104)Cited by:[§4\.5](https://arxiv.org/html/2607.16997#S4.SS5.p1.3)\.
- L\. de Moura and S\. Ullrich \(2021\)The Lean 4 theorem prover and programming language\.InAutomated Deduction – CADE 28,Lecture Notes in Computer Science, Vol\.12699,pp\. 625–635\.External Links:[Document](https://dx.doi.org/10.1007/978-3-030-79876-5%5F37)Cited by:[§1](https://arxiv.org/html/2607.16997#S1.p4.2),[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px3.p1.1)\.
- M\. Detlefsen and A\. Arana \(2011\)Purity of methods\.Philosophers’ Imprint11\(2\),pp\. 1–20\.Cited by:[§1](https://arxiv.org/html/2607.16997#S1.p2.1),[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px5.p1.1)\.
- J\. L\. Fleiss \(1971\)Measuring nominal scale agreement among many raters\.Psychological Bulletin76\(5\),pp\. 378–382\.External Links:[Document](https://dx.doi.org/10.1037/h0031619)Cited by:[§4\.5](https://arxiv.org/html/2607.16997#S4.SS5.p1.3)\.
- J\. Hu, T\. Zhu, and S\. Welleck \(2024\)miniCTX: neural theorem proving with \(long\-\)contexts\.Note:arXiv preprint arXiv:2408\.03350External Links:2408\.03350,[Link](https://arxiv.org/abs/2408.03350)Cited by:[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px1.p1.1),[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px3.p1.1)\.
- M\. Inglis and A\. Aberdein \(2015\)Beauty is not simplicity: an analysis of mathematicians’ proof appraisals\.Philosophia Mathematica23\(1\),pp\. 87–109\.External Links:[Document](https://dx.doi.org/10.1093/philmat/nku014)Cited by:[§1](https://arxiv.org/html/2607.16997#S1.p2.1),[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px5.p1.1)\.
- G\. Irving, C\. Szegedy, A\. A\. Alemi, N\. Eén, F\. Chollet, and J\. Urban \(2016\)DeepMath: deep sequence models for premise selection\.InAdvances in Neural Information Processing Systems 29,pp\. 2235–2243\.Cited by:[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px1.p1.1)\.
- S\. Kurgan, E\. Wang, E\. Leonen, S\. Szeto, L\. Alexander, A\. Remizov, J\. Alper, G\. Inchiostro, and V\. Ilin \(2026\)TheoremGraph: bridging formal and informal mathematics\.Note:arXiv preprint arXiv:2606\.25363External Links:2606\.25363,[Link](https://arxiv.org/abs/2606.25363)Cited by:[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px3.p1.1)\.
- S\. Lamont, C\. Walder, A\. Dezfouli, P\. Montague, and M\. Norrish \(2025\)3D\-Prover: diversity driven theorem proving with determinantal point processes\.InAdvances in Neural Information Processing Systems 38,External Links:[Link](https://proceedings.neurips.cc/paper_files/paper/2025/hash/5d9d078006840c0643b62013981ad195-Abstract-Conference.html)Cited by:[§1](https://arxiv.org/html/2607.16997#S1.p3.1),[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px2.p1.1)\.
- G\. Lample, T\. Lacroix, M\. Lachaux, A\. Rodriguez, A\. Hayat, T\. Lavril, G\. Ebner, and X\. Martinet \(2022\)HyperTree proof search for neural theorem proving\.InAdvances in Neural Information Processing Systems 35,pp\. 26337–26349\.Cited by:[§1](https://arxiv.org/html/2607.16997#S1.p3.1),[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px2.p1.1)\.
- M\. Lange \(2014\)Aspects of mathematical explanation: symmetry, unity, and salience\.The Philosophical Review123\(4\),pp\. 485–531\.External Links:[Document](https://dx.doi.org/10.1215/00318108-2749730)Cited by:[§1](https://arxiv.org/html/2607.16997#S1.p2.1),[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px5.p1.1)\.
- X\. Li, N\. Peng, S\. Severini, and P\. Shafto \(2026\)The network structure of Mathlib\.Note:arXiv preprint arXiv:2604\.24797External Links:2604\.24797,[Link](https://arxiv.org/abs/2604.24797)Cited by:[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px3.p1.1)\.
- OpenAI \(2025\)GPT\-5 system card\.Note:Technical reportModel\-family documentation; exact API snapshots used in the reported baseline were not retainedExternal Links:2601\.03267,[Link](https://openai.com/index/gpt-5-system-card/)Cited by:[§4\.4](https://arxiv.org/html/2607.16997#S4.SS4.p1.1)\.
- N\. Reimers and I\. Gurevych \(2019\)Sentence\-BERT: sentence embeddings using siamese BERT\-networks\.InProceedings of EMNLP\-IJCNLP,pp\. 3982–3992\.External Links:[Document](https://dx.doi.org/10.18653/v1/D19-1410)Cited by:[§3\.3](https://arxiv.org/html/2607.16997#S3.SS3.p1.3)\.
- L\. Ruff, J\. R\. Kauffmann, R\. A\. Vandermeulen, G\. Montavon, W\. Samek, M\. Kloft, T\. G\. Dietterich, and K\. Müller \(2021\)A unifying review of deep and shallow anomaly detection\.Proceedings of the IEEE109\(5\),pp\. 756–795\.External Links:[Document](https://dx.doi.org/10.1109/JPROC.2021.3052449)Cited by:[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px4.p1.1)\.
- C\. E\. Shannon \(1948\)A mathematical theory of communication\.Bell System Technical Journal27\(3\),pp\. 379–423\.External Links:[Document](https://dx.doi.org/10.1002/j.1538-7305.1948.tb01338.x)Cited by:[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px4.p1.1)\.
- M\. Steiner \(1978\)Mathematical explanation\.Philosophical Studies34\(2\),pp\. 135–151\.External Links:[Document](https://dx.doi.org/10.1007/BF00354494)Cited by:[§1](https://arxiv.org/html/2607.16997#S1.p2.1),[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px5.p1.1)\.
- The mathlib Community \(2020\)The Lean mathematical library\.InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs,pp\. 367–381\.External Links:[Document](https://dx.doi.org/10.1145/3372885.3373824)Cited by:[§1](https://arxiv.org/html/2607.16997#S1.p4.2),[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px3.p1.1)\.
- B\. Uzzi, S\. Mukherjee, M\. Stringer, and B\. Jones \(2013\)Atypical combinations and scientific impact\.Science342\(6157\),pp\. 468–472\.External Links:[Document](https://dx.doi.org/10.1126/science.1240474)Cited by:[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px4.p1.1)\.
- W\. Wang, F\. Wei, L\. Dong, H\. Bao, N\. Yang, and M\. Zhou \(2020\)MiniLM: deep self\-attention distillation for task\-agnostic compression of pre\-trained transformers\.InAdvances in Neural Information Processing Systems 33,pp\. 5776–5788\.Cited by:[§3\.3](https://arxiv.org/html/2607.16997#S3.SS3.p1.3)\.
- C\. Wernhard and W\. Bibel \(2024\)Investigations into proof structures\.Journal of Automated Reasoning68,pp\. 24\.Note:Article 24External Links:[Document](https://dx.doi.org/10.1007/s10817-024-09711-8)Cited by:[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px3.p1.1)\.
- E\. B\. Wilson \(1927\)Probable inference, the law of succession, and statistical inference\.Journal of the American Statistical Association22\(158\),pp\. 209–212\.External Links:[Document](https://dx.doi.org/10.1080/01621459.1927.10502953)Cited by:[§4\.5](https://arxiv.org/html/2607.16997#S4.SS5.p1.3)\.
- H\. Xin, D\. Guo, Z\. Shao, Z\. Ren, Q\. Zhu, B\. Liu, C\. Ruan, W\. Li, and X\. Liang \(2024\)DeepSeek\-Prover: advancing theorem proving in LLMs through large\-scale synthetic data\.Note:arXiv preprint arXiv:2405\.14333External Links:2405\.14333,[Link](https://arxiv.org/abs/2405.14333)Cited by:[§1](https://arxiv.org/html/2607.16997#S1.p3.1),[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px2.p1.1)\.
- K\. Yang, A\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. J\. Prenger, and A\. Anandkumar \(2023\)LeanDojo: theorem proving with retrieval\-augmented language models\.InAdvances in Neural Information Processing Systems 36,pp\. 21573–21612\.Cited by:[§1](https://arxiv.org/html/2607.16997#S1.p3.1),[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px1.p1.1),[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px2.p1.1),[§2](https://arxiv.org/html/2607.16997#S2.SS0.SSS0.Px3.p1.1)\.

## Appendix AAlgorithmic specification

For a target declarationDDin binb​\(t\)b\(t\), the released pipeline implements the following high\-level procedure:

1. 1\.Check out the library snapshot at the beginning of the bin and restrict every corpus\-derived quantity toℒ<b​\(t\)\\mathcal\{L\}\_\{<b\(t\)\}\.
2. 2\.Extract actual used constants frompDp\_\{D\}with the proof\-term backend\.
3. 3\.Apply the deterministic plumbing filter\.
4. 4\.Recursively unfold non\-established dependencies to the established\-machinery frontier using pre\-bin reuse counts\.
5. 5\.Map frontier constants to supported families by hierarchical backoff and assign deterministic footprint weights, yielding[eq\.˜2](https://arxiv.org/html/2607.16997#S3.E2)\.
6. 6\.EmbedxDx\_\{D\}with the encoder trained only on data before the bin and retrieve nearest statements fromℒ<b​\(t\)\\mathcal\{L\}\_\{<b\(t\)\}\.
7. 7\.Build the mixture prior in[eq\.˜3](https://arxiv.org/html/2607.16997#S3.E3)from retrieved, namespace, module, and global family counts\.
8. 8\.Compute[eq\.˜4](https://arxiv.org/html/2607.16997#S3.E4); emit the total and per\-family contributions\.

The implementation additionally records the snapshot ID, encoder path, family\-backoff level, retrieval neighborhood, prior mixture, redundancy flags, and counterfactual score, enabling audit of each score\.

## Appendix BExperimental provenance

### B\.1PinnedMathlibsnapshots andLeantoolchains

Each snapshot uses the latest commit from theMathlibmasterbranch at or before the bin start; extraction was performed on the listed start date\. The toolchain is the value in the pinned commit’slean\-toolchainfile\.

Table 6:Snapshot dates andLeantoolchains\.SnapshotStart / extraction dateLeantoolchain2023Q42023\-10\-01leanprover/lean4:v4\.2\.0\-rc12024Q12024\-01\-01leanprover/lean4:v4\.5\.0\-rc12024Q22024\-04\-01leanprover/lean4:v4\.7\.0\-rc2FullMathlibcommit identifiers:

2023Q4aef04106feb057e57456331886e5f38e392dea9f

2024Q12a17457d3236d97eec6687377c01a74fe2961ab7

2024Q2d8d7e696a4c05914b5f2dbff8768541fe1dd4b39

### B\.2Encoder training

Table 7:Per\-bin statement\-encoder configuration\. No seed was set\.FieldValueBase modelsentence\-transformers/all\-MiniLM\-L6\-v2ObjectiveMultiple Negatives Ranking Loss, with mined hard negativesTraining sliceContrastive examples restricted to declarations before the score binEpochs / batch size1 / 64OptimizerAdamW \(Sentence\-Transformers default, with learning rate overridden\)Learning rate / warmup2×10−52\\times 10^\{\-5\}/ 10% linear warmupMaximum sequence length256 tokensData orderShuffledDeviceAuto\-selected by Sentence\-Transformers \(CUDA when available, otherwise CPU\)SeedNone; DataLoader order and accelerator execution may vary across runsExact Sentence\-Transformers/PyTorch versions, accelerator model, and checkpoint hashes were not retained in the supplied experimental record\. The disclosed configuration therefore supports methodological reproduction but not bitwise reconstruction of the original learned embeddings\.

### B\.3Retrieval, family backoff, and prior grid

Retrieval usesk=32k=32, cosine similarity overℓ2\\ell\_\{2\}\-normalized embeddings, and softmax temperature 0\.2\. A raw declaration family is used only after at least five historical occurrences; otherwise the implementation backs off through parent namespaces, module, area, and global levels\. The prior grid crosses

α∈\{0\.01,0\.025,0\.05,0\.1,0\.25,0\.5\}\\alpha\\in\\\{0\.01,0\.025,0\.05,0\.1,0\.25,0\.5\\\}with the mixture candidates in[table˜8](https://arxiv.org/html/2607.16997#A2.T8)\. Parameters are selected by chronological log likelihood, independently of the human judgments\.

Table 8:Candidate prior mixtures\(λr,λn,λm,λg\)\(\\lambda\_\{r\},\\lambda\_\{n\},\\lambda\_\{m\},\\lambda\_\{g\}\)\.CandidateRetrievalNamespaceModuleGlobalDefault0\.550\.200\.150\.10Balanced0\.400\.250\.200\.15Retrieval\-heavy I0\.700\.100\.100\.10Retrieval\-heavy II0\.800\.080\.060\.06Retrieval\-heavy III0\.900\.040\.030\.03Retrieval only1\.000\.000\.000\.00No retrieval0\.000\.350\.300\.35The selected topology configuration is\(0\.90,0\.04,0\.03,0\.03\)\(0\.90,0\.04,0\.03,0\.03\)withα=0\.05\\alpha=0\.05; the selected all\-Mathlibconfiguration is\(0\.40,0\.25,0\.20,0\.15\)\(0\.40,0\.25,0\.20,0\.15\)withα=0\.10\\alpha=0\.10\. Reuse thresholds\{3,5,8,13\}\\\{3,5,8,13\\\}were swept, but family assignments were identical throughout the reported corpus\.

### B\.4Compute and randomness record

Wall\-clock logs were not retained\. The author records the encoder fine\-tuning as a single\-consumer\-GPU workload on the order of minutes per bin and extraction as a CPU workload on the order of hours per snapshot\. Hardware model, memory, storage, exact stage times, and total exploratory compute are unknown\. Nondeterministic components are: unseeded encoder fine\-tuning; language\-model API judgments \(17 of 100 presentation\-level decisions changed across two identical\-setting runs of the best condition\); and potentially packet sampling, for which a seed was not recovered from the supplied records\. The committed packet artifact fixes the evaluated sample even where the generating seed is unavailable\.

## Appendix CMechanical\-validation details

The fitted prior mixtures and ablations are reported in[tables˜2](https://arxiv.org/html/2607.16997#S5.T2)and[3](https://arxiv.org/html/2607.16997#S5.T3); they are not duplicated here\. The remaining mechanical diagnostics are: observed\-family mean log probability−10\.132\-10\.132versus−12\.056\-12\.056for random alternatives over 5,629 footprint items; counterfactual\-retrieval signed and absolute sensitivities 1\.31 and 1\.59 over 248 targets; score/backoff\-depth correlationr=0\.046r=0\.046over 992 family observations; zero live redundancy hits; and identical family buckets for all 10,132 declarations across reuse thresholds 3, 5, 8, and 13\.

## Appendix DComplete result tables

All outcome summaries in this section use the 76 distinct underlying pairs after the 12 triplicated canonical groups are collapsed\. The consistency instrument itself is reported separately in[table˜4](https://arxiv.org/html/2607.16997#S5.T4)\.

For the best language\-model condition, the paired discordances are 8PriorProof\-only correct pairs and 15 model\-only correct pairs; the exact two\-sided McNemar test givesp=0\.210p=0\.210\. The primary majority collapse and first\-presentation\-only sensitivity rule produce the same discordant counts andpp\-value\. Across all other aggregate outcomes, the first\-presentation sensitivity differs from the primary collapse by no more than one pair\.

Table 9:Score\-gap results used in[fig\.˜2](https://arxiv.org/html/2607.16997#S5.F2)\. Each bin contains 19 distinct pairs\.Gap quartileCorrectAgreementWilson 95% CISmallest12/1963\.2%\[41\.0%, 80\.9%\]Second11/1957\.9%\[36\.3%, 76\.9%\]Third14/1973\.7%\[51\.2%, 88\.2%\]Largest16/1984\.2%\[62\.4%, 94\.5%\]Table 10:Retained\-rater agreement on distinct pairs\. Cohen’sκ\\kappavalues are computed under a canonical binary orientation for each pair\.QuantityEstimateWilson 95% CI, if applicableCohen’sκ\\kappa, three rater pairs0\.548; 0\.461; 0\.550—Fleiss’κ\\kappa, all distinct pairs0\.519—Fleiss’κ\\kappa, canonical0\.750—Fleiss’κ\\kappa, stratified0\.476—Three\-rater unanimity49/76 = 64\.5%\[53\.3%, 74\.3%\]Table 11:Language\-model comparison on distinct pairs\. Five 2–2 ties are excluded from the four\-condition majority row\.ConditionCorrectAgreementWilson 95% CIBest logged condition:gpt\-5\-mini, strict60/7678\.9%\[68\.5%, 86\.6%\]Four\-condition majority, non\-tied pairs57/7180\.3%\[69\.6%, 87\.9%\]PriorProof53/7669\.7%\[58\.7%, 78\.9%\]
## Appendix EHuman\-study packet, screening, and ethics

Each comparison side contains four fields: declaration name, theorem statement, a natural\-language proof narrative, and fullLeansource\. The public rater packet excludes metric scores, priors, family buckets, metric\-derived explanations, and the canonical/stratified source label\. Narratives are generated from the blinded packet rather than from score artifacts\. The same materials and core question are passed to human and language\-model judges\.

The packet contains 100 presentations of 76 distinct underlying pairs\. Twelve canonical pairs are each presented three times; 10 of the 12 groups include a left/right swap and two retain the same order\. The remaining 64 stratified pairs are unique\. Repeats were deliberately included for consistency measurement\. For outcome analysis, left/right choices are normalized to proof identity, each pair receives a canonical binary orientation, and each judge’s repeated group is collapsed by majority\. No collapse ties occur for retained raters or model conditions, and the 64 singleton pairs remain unchanged\.

The quality screen was developed post hoc\. Outcome statistics were first computed with all four raters\. One response set was then flagged by approximately seven\-second median response time, weak agreement with other human and automated judges, and an explanation solicited from the rater\. The order\-normalized majority\-match statistic was constructed last and used as the criterion of record\. The screened rater records 28/36 majority\-match votes and 4/12 fully consistent groups, compared with 35/36, 35/36, and 33/36 votes and 11/12, 11/12, and 9/12 groups for the retained raters\. Random binary responding has vote floor 24/36, expected votes 27/36, and expected fully consistent groups 3/12;Pr⁡\(X≥4\)=0\.351\\Pr\(X\\geq 4\)=0\.351\. A fixed position bias and random responding are not separable under this instrument, but both fail to track proof identity\. The timing evidence is therefore part of the exclusion rationale\. All headline outcomes use the three retained raters\. The four language\-model conditions achieve 33–35 votes and 9–11 groups, so they pass the same consistency instrument\.

The study was conducted by an independent researcher with no institutional affiliation requiring review\. It involved expert annotation of public formal proofs, was minimal risk, and collected no sensitive research data\. Raters were informed that responses would be used in research\. Names and payment information were used only for recruitment/payment, retained privately, and omitted from released artifacts\. Compensation was $1,500 per completed packet, and every recruited rater was paid in full\. The estimated completion time was roughly two hours; this corresponds to approximately $750/hour, or $500/hour under a three\-hour completion assumption\. Human responses are not released because the disclosure to raters did not address public data release\.

Future studies should preregister the exact exclusion rule, preserve item\-level timestamps and responses in a dated manifest, enlarge the distinct canonical set while retaining repeats as an instrument, and add another mathematical domain\. A hierarchical model with item and rater random effects would better reflect the shared\-panel design\.

## Appendix FLanguage\-model baseline provenance

Judgments were collected through the OpenAI Responses API under the provider namesgpt\-5andgpt\-5\-mini; date\-pinned model IDs were not available in the run records\. Two prompt\-strictness levels were crossed with the two models\. Temperature was not explicitly set and therefore followed the API default\. Each condition’s repeated presentations are normalized to proof identity and collapsed before outcomes are scored\. A majority over the four conditions excludes 2–2 splits\. Request and response files for the designated run and a second identical\-setting run are retained privately\. The best condition differs on 17 of 100 presentations across those runs\.

Proof narratives were generated bygpt\-5\-mini\. The narrative system instruction forbade formal\-system metadata, evaluation vocabulary, and any judgment that a proof was standard, surprising, or preferred\. Outputs were checked against forbidden\-term and forbidden\-pattern lists and retried upon failure\. Exact prompt strings and pair templates are retained in the request archive but are not reproduced in this source package; they should be deposited verbatim with any venue supplement that requires request\-level reproducibility\. Execution dates were not logged, and exact\-model reproduction cannot be guaranteed because provider names may later resolve to updated snapshots\.

## Appendix GRelease, licensing, and reproduction map

The PriorProof code is released under the MIT License\. The public repository documents five reproduction stages:

1. 1\.Extraction and snapshots:freezeMathlibcommits, run theLeanproof\-term extractor, normalize declarations, and build pre\-bin reuse counts\.
2. 2\.Footprints:filter dependencies, unfold to the established frontier, back off to supported families, and write one footprint artifact per reuse threshold\.
3. 3\.Encoder and prior:mine pre\-bin contrastive pairs, fine\-tune per\-bin encoders, retrieve statement neighbors, and fit mixture weights by chronological likelihood\.
4. 4\.Scoring and mechanical validation:produce scores and priors, run ablations, create counterfactual priors, and aggregate threshold/backoff/redundancy diagnostics\.
5. 5\.Judgment study:assemble canonical and stratified presentations, render the blinded rater interface, generate identically structured model requests, and analyze responses after repeat collapse\.

The analysis command fails closed when it detects duplicate underlying pairs, including side\-swapped duplicates, unless\-\-allow\-repeats\-with\-collapseis supplied\. It accepts the screened response separately through\-\-screening\-response, assertsPriorProof’s determinism across presentations, and verifies that all collapsed labels use the canonical binary orientation\. These checks prevent repeated presentations or screened responses from silently entering outcome statistics\.

Generated corpora, model checkpoints, answer keys, human responses, and language\-model responses are excluded from the small public release\. Independent groups can regenerate the method and run a fresh blinded study, but cannot reproduce the exact reported human/model aggregates from public files alone\. The source package includes a third\-party asset ledger\. Exact installed Python package versions, encoder checkpoint hashes, hardware logs, and unlogged API execution dates remain unavailable\.

## Appendix HClaim\-to\-evidence map

Table 12:Scope of the paper’s principal claims\.ClaimEvidenceNon\-claimThe prior predicts used families better than random alternativesChronological mean log\-probability margin over 5,629 footprint itemsThe prior is a calibrated generative model of all valid proofsClear contrasts behave as intended11/12 = 91\.7% agreement, Wilson 95% CI \[64\.6%, 98\.5%\]The 12\-pair canonical estimate represents broad\-corpus accuracyLarger gaps are the more reliable endpoint in this sample16/19 = 84\.2% \[62\.4%, 94\.5%\] in the largest bin versus 12/19 = 63\.2% \[41\.0%, 80\.9%\] in the smallestA monotone calibration curve or a transferable thresholdThe metric is broadly informative but noisy42/64 = 65\.6% \[53\.4%, 76\.1%\] on stratified pairs; Fleiss’κ=0\.476\\kappa=0\.476Rater majority is objective ground truthThe model judge has the higher nominal point estimate60/76 = 78\.9% \[68\.5%, 86\.6%\] versus 53/76 = 69\.7% \[58\.7%, 78\.9%\]; McNemar discordances 8 versus 15,p=0\.210p=0\.210Statistically established superiority, equality, or non\-inferiorityRepeats function as a consistency instrumentRetained raters and model conditions have 9–11 fully consistent groups; screened response has 4; random expectation is 3A preregistered screen or evidence that the model baseline fails engagement