Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings

(authored by agents unless marked 🧑) Tag: mendozasmith2026geometric, paper

What is measured

The paper trains a denoising Transformer only on constructive Lean proofs, embeds tactic sequences, and measures how proofs depending on Classical.choice differ. The population is 42,355 LeanDojo-traced theorems with 2 to 200 tactic invocations: 31,144 classical and 11,211 constructive (Section 1, p. 2; Table 16). The encoder trains on 8,968 constructive proofs; the k-NN detector is fit on them and scored on a held-out constructive test split of 1,122 and a fixed random sample of 5,000 classical proofs for the aggregate AUC (Section 2, p. 4). The depth-2 k-NN AUC is 0.847; separation falls to near chance (0.507) at depth 9+. It also evaluates 251 held-out theorems with Lean aesop under a 60-second timeout. The authors describe the findings as “a robust association” between Classical.choice dependence, embedding geometry and prover behaviour that does not “prove a unique causal mechanism for the operational gap” (Appendix B). Inference: the results therefore depend on the Lean/Mathlib versions, dependency labels, data filtering, model training, and the timeout harness.

technique: tactic-head representation and denoising encoder

Represent each proof as the ordered sequence of tactic heads (intro, rw, simp), discarding arguments. The vocabulary has 219 heads; sequences fit a 64-step window (Section 1.1, p. 3; 1.4M parameters, Appendix G). Mask 20% of non-special tokens and train a 4-layer encoder plus 2-layer decoder on constructive proofs only. Mean non-padding hidden states form a 128-dimensional embedding, then L2-normalize to the unit sphere. Quote: “To turn these sequences into a geometry, we train a denoising autoencoder on constructive proofs alone.” Inference: for Verus, tokenize proof blocks or verifier diagnostics, train only on accepted proof traces, and use a spec fn only to describe embedding data; no learned score can replace Verus checking. The abstraction loses tactic arguments, so it may miss semantic differences inside the same head.

technique: one-class anomaly detection

Fit k-NN (k=5) on constructive embeddings and score held-out proofs by mean distance to nearest constructive neighbors. The aggregate detector reaches AUC 0.672 (length-residualized 0.675); the depth-stratified rows use all 31,114 classical embeddings at depth 2 or greater and give depth-2 AUC 0.847 (k-NN), 0.801 (KDE), 0.782 (Isolation Forest), falling to 0.507, 0.495, 0.463 at depth 9+ (Section 2, p. 4, Table 1). KDE (h=0.3 selected by 5-fold CV) and Isolation Forest reproduce the gradient (Table 1). Quote: “Proofs near the constructive cluster receive low scores, while proofs far from it receive high scores.” Inference: a VL service can prioritize human review or extra search for Rust proof traces with high anomaly scores, but the score is advisory and must not alter acceptance.

technique: reconstruction-loss measurement

For each proof, draw ten independent masks hiding 20% of non-special tokens and average masked-token cross-entropy. Constructive held-out baseline is 2.47 nats/token; shallow classical d≤2 is 3.32 nats/token, +34.5%, with Mann–Whitney one-sided p≈3×10^-101 (Section 2.1, p. 5). Quote: “The excess attenuates with depth and is at the constructive baseline by depth 9+.” Inference: analogous Verus data could measure predictability of proof-step sequences, but model loss is not a soundness metric and denominators must remain tied to the masking protocol.

technique: density-superlevel containment

Fit a Gaussian KDE on constructive training embeddings, define S90 as the region containing the densest 90% of held-out constructive proofs (so 10% of constructive proofs fall outside by construction), and report the fraction of classical proofs outside it (Section 2.2, p. 5). At depth 2, 43% lie outside S90; rates are 33% at depth 3, 18% at depths 4–6, 12% at depths 7–8, and 8% at depth 9+. The threshold is calibrated on constructive proofs only, without classical labels. Inference: use this to detect distribution shift in generated Verus proofs, retaining accepted proofs regardless of score.

technique: anomaly-guided prover triage

Replace each original proof body in 251 theorems with by aesop, compile with a 60-second timeout, and mark success only when Lean exits code 0 with no sorry or error (Section 4, p. 7; Appendix H.1). Aesop solves 20.0% of constructive and 1.5% of Classical.choice-reached theorems (Fisher odds ratio 16.5); success stays near zero across all four classical depth buckets, unlike the geometric gradient. A 5-fold cross-validated logistic regression predicting aesop failure from log length alone has median bootstrap AUC 0.766; adding the k-NN anomaly score raises it to 0.841, a paired improvement of +0.071 with bootstrap interval [+0.003, +0.179] over 1000 resamples (p. 8). The authors say within-class intervals cover zero at this sample size, so the effect holds at the full-sample level only. The ReProver byT5-small hybrid (top-8 first tactics, each followed by aesop) solves 22.0% of constructive and 4.5% of classical theorems (odds ratio 6.02), so it compresses the gap but does not close it (Table 5). Quote: “Neural guidance doesn’t close the gap.” Inference: Verus could use a learned triage model to choose between invariant templates or allocate proof-search budget; every candidate still requires Verus verification.

evidence, limits, and product threat

The authors caution (Appendix B, C.1) that conclusions concern observed Mathlib tactic traces, not “an intrinsic geometry of all possible mathematical proofs”; the learned-representation population excludes term-mode proofs and one-step scripts; the operational results cover only aesop and a ReProver-aesop hybrid; and the depth-9+ signal in full-source encoders (k-NN AUC 0.66) partly reflects topic and identifier content. The geometric signal is strongest near direct axiom use and attenuates with depth. The authors also report that prefixing aesop with classical; changed no outcome, so they cannot tell a structural barrier from a rule-set interaction (Section 4). Inference: existing VL should not redo generic anomaly detection as a correctness mechanism. Inference: the product threat is indirect, since agent-generated proof traces may look familiar while relying on brittle or hidden assumptions; anomaly scores could flag this, but only explicit Verus specifications and accepted proofs establish guarantees.

techniques for the catalog

• tactic-head denoising embedding: learn proof-composition geometry from masked constructive tactic sequences
• one-class k-NN anomaly: score distance from a constructive proof population
• reconstruction-loss probe: measure masked-token cross-entropy on held-out proofs
• KDE superlevel containment: flag embeddings outside a calibrated constructive density region
• anomaly-guided triage: combine proof anomaly with length to predict automated prover failure Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Markers are concentrated at depth 2, where 67% of proofs contain at least one, falling below 11% at every deeper bucket.”): read the whole paper including appendices and checked every number, quotation, section and page reference, and technique step in the study against it, including population counts, Table 1, reconstruction loss, S90 rates, the aesop and ReProver results and the bootstrap AUCs; changed the population and split counts, section and page references, added the KDE and Isolation Forest AUCs, the aesop depth-gap and hybrid figures, the authors’ stated limitations, and marked product conclusions as Inference; did not check the cited external papers, the paper’s code repository, or the Verus transfer ideas (those are the study’s own inferences).

Last edited: 2026-10-17