# Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings

arXiv: https://arxiv.org/abs/2606.28572 · HTML: https://mlsanity.com/paper/2606.28572/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 10 of its 25 references that are in the map.
- First posted on arXiv 26 Jun 2026.

## Builds on (most cited first, 10 of 10)

- [A Baseline for Detecting Misclassified and Out-of-Distribution Examples in Neural Networks](https://mlsanity.com/paper/1610.02136/) (2016)
- [Enhancing The Reliability of Out-of-distribution Image Detection in Neural Networks](https://mlsanity.com/paper/1706.02690/) (2017)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [GamePad: A Learning Environment for Theorem Proving](https://mlsanity.com/paper/1806.00608/) (2018)

## Abstract (arXiv)

The axiom of choice has divided the foundations of mathematics for over a century, but the distinction between classical and constructive proofs has remained a philosophical and methodological one. We use Lean 4's kernel-level tracking of axiom dependence to show that the axiom of choice has a measurable geometric correlate in proof space that obeys a one-parameter mixture law and has operational consequences for neural theorem provers. To do this, we partition 471,260 declarations of Mathlib by transitive dependence on the axiom of choice and represent a filtered population of 42,355 traced theorems by their sequences of tactic invocations. We use the constructive proofs in this dataset to train a self-supervised proof encoder and show that when using it to measure classical proofs, three complementary measurements (anomaly score, reconstruction loss, and density-superlevel containment) exhibit a common decline with the proof's distance from the axiom in the dependency graph, from sharp separation at the shallow boundary (AUC 0.847 at distance 2) to indistinguishability at distance~9+. Robustness controls show that the signature survives length, file, author, and topic controls, and replicates under full-source encoders trained on normalised proof source. Operationally, we show that on an evaluation sample of 251 Mathlib theorems, Lean's textttaesop tactic solves constructive theorems at 13× the rate of classical ones, and a neural-guided hybrid using the ReProver tactic generator compresses the gap to 5×. The geometric anomaly score predicts textttaesop failure beyond proof length, providing an operational link between the geometric signature and prover performance.