Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings

• URL: http://arxiv.org/abs/2606.28572v1
• Date: Fri, 26 Jun 2026 19:57:00 GMT
• Title: Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings
• Abstract summary: 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.<n>We show that the signature survives length, file, author, and topic controls, and replicates under full-source encoders trained on normalised proof source.
• Score: 0.2538209532048866
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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 \texttt{aesop} tactic solves constructive theorems at $13\times$ the rate of classical ones, and a neural-guided hybrid using the ReProver tactic generator compresses the gap to $5\times$. The geometric anomaly score predicts \texttt{aesop} failure beyond proof length, providing an operational link between the geometric signature and prover performance.

Related papers

• Autonomous disproofs of the sum-product conjecture over $\mathbb R$ with GPT-5.5 Pro [5.634825161148485]
  We present a problem-agnostic, three-stage prompting pipeline built on GPT-5.5 Pro.<n>The agent autonomously generated correct proofs that the sum-product conjecture is false over $mathbb R$ in 7 of 8 independent trials.
  arXiv  Detail & Related papers  (2026-07-09T23:28:37Z)
• An Information-Geometric Justification for Composite Coherence in Event-Based Narrative Extraction [0.27074235008521247]
  We study the composite metric $C=sqrtAcdot T$, where $A$ is the angular similarity of document embeddings and $T=1-d_mathrmJS$.<n>Experiments on four corpora, three embedding families, and three topic models are consistent with the framework.
  arXiv  Detail & Related papers  (2026-06-28T00:05:15Z)
• ComBench: A Benchmark for Rigorous Proof Reasoning and Constructive Realization in Olympiad-Level Combinatorics [95.15900681087088]
  We introduce ComBench, an Olympiad-level benchmark for diagnosing and the reasoning capabilities of large language models.<n>ComBench contains 100 human-annotated competition-level problems organized around two complementary settings.<n>Experiments show that the strongest model reaches 65.4% overall Avg. and 75.3% overall Best@4.
  arXiv  Detail & Related papers  (2026-06-09T06:50:15Z)
• LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
  We present LeanMarathon, a multi-agent harness for reliable research-level Lean autoformalization.<n>Four contract-scoped agents construct, audit, prove, and repair this blueprint.<n>We evaluate LeanMarathon on two recent research papers spanning four Erds problems.
  arXiv  Detail & Related papers  (2026-06-03T20:09:39Z)
• Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1 [51.56484100374058]
  System extracts tactic usage distributions across 27 top-level areas of Mathlib.<n>It computes z-scores to identify tactics that are heavily used in a source area but rare or absent in a target area.<n>It matches source and target proof states via GPU-accelerated NP-hard analogy.
  arXiv  Detail & Related papers  (2026-04-19T03:27:16Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  We present LiveMathematicianBench, a dynamic multiple-choice benchmark for research-level mathematical reasoning.<n>By grounding evaluation in newly published theorems, it provides a realistic testbed beyond memorized patterns.<n>It employs a proof-sketchguided distractor pipeline that uses high-level proof strategies to construct plausible but invalid answer choices.
  arXiv  Detail & Related papers  (2026-04-02T08:22:17Z)
• Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving [36.20164235042574]
  In this work, we propose textbfSeed-Prover, a lemma-style whole-proof reasoning model.<n>To solve IMO-level contest problems, we design three test-time inference strategies that enable both deep and broad reasoning.<n>Seed-Prover proves $78.1%$ of formalized past IMO problems, saturates MiniF2F, and achieves over 50% on PutnamBench, outperforming the previous state-of-the-art by a large margin.
  arXiv  Detail & Related papers  (2025-07-31T17:00:30Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thought prompting has become the de facto method to elicit reasoning capabilities from large language models (LLMs)<n>To mitigate hallucinations in CoT that are notoriously difficult to detect, current methods operate as opaque boxes and do not provide checkable evidence for their judgments, possibly limiting their effectiveness.<n>We propose a retrospective, step-aware formal verification framework $Safe$. Rather than assigning arbitrary scores, we strive to articulate mathematical claims in formal mathematical language Lean 4 at each reasoning step and provide formal proofs to identify hallucinations.
  arXiv  Detail & Related papers  (2025-06-05T03:16:08Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  This work proposes Alchemy, a framework for data synthesis that constructs formal theorems through symbolic mutation.<n>For each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it.<n>As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M.
  arXiv  Detail & Related papers  (2024-10-21T08:04:21Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.