{"id":"arxiv/2606.28572","url":"https://arxiv.org/abs/2606.28572","tags":["cs.LG","cs.AI","cs.LO","math.LO"],"score":0,"title":"Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings","domain":"cs.LG","source":"arxiv","authors":["Rodrigo Mendoza-Smith"],"reviews":0,"subject":"cs.LG","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-06-26","reactions":{}}