🤖 machine learning

Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings

This paper demonstrates that the Axiom of Choice leaves a measurable geometric signature in neural proof embeddings—characterized by declining anomaly scores and reconstruction losses as proofs move further from the axiom in the dependency graph—which correlates with and predicts the performance disparity between constructive and classical theorem proving in systems like Lean 4.

Original authors: Rodrigo Mendoza-Smith

Published 2026-06-30✓ Author reviewed ⓘ

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Rodrigo Mendoza-Smith

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine a massive, ancient library called Mathlib. This library contains nearly half a million mathematical proofs, all written in a strict, computer-readable language called Lean. For over a century, mathematicians have argued about two different ways to build these proofs:

Constructive Proofs: The "Lego" method. If you claim a building exists, you must show exactly how to build it, brick by brick.
Classical Proofs: The "Magic" method. You can claim a building exists just by saying, "It's impossible for it not to exist," without showing how to build it. This relies on a rule called the Axiom of Choice.

For a long time, people thought these were just philosophical differences. This paper argues that they are actually geometric differences that you can measure, like the distance between two cities on a map.

Here is how the authors discovered this, using simple analogies:

1. The "Echo" of the Magic Rule

The authors treated the library like a giant echo chamber. They trained a computer brain (an AI) only on the "Lego" (constructive) proofs. The AI learned the rhythm, style, and structure of these proofs. It became an expert at recognizing what a "normal" constructive proof looks like.

Then, they fed it the "Magic" (classical) proofs.

The Result: The AI didn't just say, "This is different." It measured how different.
The Analogy: Imagine you are a music teacher who only listens to classical piano. If you hear a jazz song, you might say, "That sounds weird." But if you hear a jazz song that was written 100 years ago, it might sound less weird than a modern jazz song that uses a very specific, unusual instrument.

2. The "Depth" Law

The authors realized that not all "Magic" proofs are equally magical.

Shallow Depth (Distance 1-2): These proofs use the "Magic Rule" (Axiom of Choice) directly. They are like a jazz song using that weird instrument right at the start. To the AI, these sound very strange and "out of place."
Deep Depth (Distance 9+): These proofs use the "Magic Rule" way back in the past, buried deep inside a chain of other lemmas. The proof itself looks very much like a "Lego" proof. To the AI, these sound almost normal.

The Discovery: There is a smooth gradient. As you get further away from the direct use of the "Magic Rule," the proof starts to look and sound more like a standard "Lego" proof. The "strangeness" fades away. The authors call this the Depth Law.

3. Three Ways to Measure the "Strangeness"

The paper used three different "rulers" to measure this distance, and they all agreed:

The Anomaly Score: How far is this proof from the nearest "Lego" proof? (Like measuring how far a jazz note is from a piano note).
The Reconstruction Loss: If the AI tries to guess the next step in a "Magic" proof, does it get it wrong more often than with a "Lego" proof? (Like a teacher guessing the next word in a sentence; they struggle more with the "Magic" sentences).
The Density Check: Is this proof living in the crowded "Lego" neighborhood, or is it lost in the empty "Magic" wilderness?

All three rulers showed the same pattern: The "Magic" proofs are very distinct when they are close to the source, but they blend in as you move further away.

4. The "Robot Solver" Test

The most practical part of the paper involves a robot named Aesop that tries to solve these math problems automatically.

The Problem: The robot is great at solving "Lego" proofs (20% success rate) but terrible at "Magic" proofs (only 1.5% success rate). It's like a robot that can build with blocks but gets confused by magic spells.
The Twist: The authors tried to help the robot by giving it a "neural guide" (a smart assistant that suggests the first move).
The Result: The guide helped a little bit, but it did not fix the problem. The robot still struggled massively with the "Magic" proofs, even when they were "deep" and looked like "Lego" proofs.

The Big Takeaway: Even though the "Magic" proofs look more and more like "Lego" proofs the further you get from the source, the robot solver still treats them as difficult. This suggests that the "Magic" rule leaves a permanent, invisible scar on the proof that makes it hard for current computers to solve, regardless of how "normal" the proof looks on the surface.

Summary

The paper proves that the Axiom of Choice isn't just a philosophical idea; it leaves a measurable, geometric fingerprint on mathematical proofs.

Direct use of the rule makes proofs look very "alien" to AI.
Indirect use makes them look more "normal."
However, even when they look "normal," automated solvers still struggle with them significantly more than with pure constructive proofs.

It's like finding out that a house built with "magic bricks" might look exactly like a house built with "normal bricks" from the outside, but if you try to repair it with a standard toolkit, the magic bricks still cause problems.

Technical Summary: Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings

Problem Statement

The axiom of choice (AC) has historically divided mathematical foundations into classical and constructive camps, a distinction that remains largely philosophical and methodological. While classical proofs utilize non-constructive shortcuts permitted by AC, and constructive proofs require explicit witnesses, it has been unclear whether these two paradigms differ structurally in ways detectable beyond simple axiom dependence. This paper investigates whether the axiom of choice leaves a measurable "geometric signature" within the space of formal proofs, specifically within the Lean 4 Mathlib library, and whether this signature has operational consequences for neural theorem provers.

Methodology

Data Partitioning and Dependency Tracking

The authors utilize Lean 4's kernel-level tracking of axiom dependence to partition the Mathlib library, which contains 471,260 machine-certified declarations. By performing a breadth-first search on the dependency graph, they classify declarations into two sets:

Classical Proofs: Those that transitively depend on Classical.choice.
Constructive Proofs: Those that do not.

The "distance" of a classical proof is defined as the length of the shortest dependency chain from that proof to Classical.choice. This creates a stratified dataset where proofs are grouped by their depth from the axiom. The study focuses on a filtered population of 42,355 theorems (31,144 classical, 11,211 constructive) with tactic traces between 2 and 200 steps.

Label-Free Representation Learning

To measure the geometric properties of these proofs without bias, the authors train a self-supervised denoising autoencoder exclusively on constructive proofs.

Input: Proofs are represented as sequences of tactic heads (e.g., intro, rw, simp), discarding specific arguments to focus on proof composition.
Architecture: A 4-layer Transformer encoder paired with a 2-layer decoder. The model is trained to reconstruct masked tactic tokens (20% corruption) from the input sequence.
Embedding: The proof embedding is the mean of the encoder's hidden states (excluding padding), normalized to the unit sphere.
Label-Free Constraint: The encoder never sees classical proofs during training, vocabulary construction, or hyperparameter selection. Classical proofs serve strictly as a held-out population for measurement.

Geometric Measurements

Three complementary metrics are used to measure the divergence of classical proofs from the constructive training distribution as a function of their dependency depth:

Anomaly Score (k-NN): The Euclidean distance to the $k$ -nearest constructive neighbors.
Reconstruction Loss: The cross-entropy loss incurred when the constructive-trained model attempts to predict masked tokens in a classical proof.
Density-Superlevel Containment: The fraction of classical proofs falling outside the high-density region (superlevel set) defined by the constructive training distribution.

Operational Evaluation

The study evaluates the impact of these geometric findings on theorem proving performance using two systems:

aesop: A symbolic best-first search prover.
Hybrid (ReProver + aesop): A neural-guided approach where a tactic generator proposes the first move, followed by aesop.

Key Results

The Depth Law

The primary finding is the existence of a "depth law": the geometric distinction between classical and constructive proofs decays predictably with the distance from Classical.choice.

Sharp Separation at Shallow Depths: At depth 2 (proofs directly invoking classical lemmas), the separation is strong. The k-NN anomaly score achieves an AUC of 0.847, reconstruction loss is 34.5% higher than the constructive baseline, and 43% of classical proofs fall outside the constructive 90% density region.
Decay to Indistinguishability: As depth increases, the metrics converge toward the constructive baseline. By depth 9+, all three metrics approach chance levels (AUC $\approx$ 0.5, loss $\approx$ baseline, containment $\approx$ 90%), rendering deep classical proofs geometrically indistinguishable from constructive ones.
One-Parameter Mixture Law: The authors model this gradient as a mixture of two distributions: a constructive distribution $P$ and a directly-classical distribution $R$ . The depth- $d$ distribution $Q_d$ is modeled as $Q_d = (1 - \lambda_d)P + \lambda_d R$ , where $\lambda_d$ is a mixing weight that decreases with depth. The three distinct measurements collapse onto a single curve when normalized, supporting this one-parameter law.

Robustness Controls

The signature is robust against several potential confounds:

Keywords: Removing explicit classical tactic markers (e.g., classical, by contra) reduces the depth-2 AUC only slightly (0.847 to 0.754), indicating the signal is structural, not merely lexical.
Length: Residualizing embeddings for proof length does not eliminate the gradient.
Author/File/Topic: Mixed-effects models controlling for author, file, and mathematical subdomain confirm the signal persists within specific contexts.
Statement vs. Proof: Theorem statements show a much weaker depth gradient (AUC 0.604 aggregate) compared to proofs (AUC 0.675 aggregate), confirming the signal is primarily compositional (proof structure) rather than topical (theorem content).
Axiom Specificity: While propext and Quot.sound also show depth gradients, Classical.choice produces the steepest gradient, suggesting a unique operational coupling with classical reasoning.

Operational Consequences

The geometric signature correlates with prover performance:

aesop Failure: aesop solves 20.0% of constructive theorems but only 1.5% of classical ones (a 13 $\times$ gap). Unlike the geometric signal, this operational gap does not smooth out with depth; classical proofs remain difficult for aesop regardless of their distance from the axiom.
Neural Guidance: Adding a neural tactic generator (ReProver) compresses the gap to roughly 5 $\times$ (22.0% vs 4.5%) but does not close it.
Predictive Power: The geometric anomaly score predicts aesop failure significantly better than proof length alone (AUC increases from 0.766 to 0.841 when adding the anomaly score).

Significance and Claims

The paper claims to provide the first empirical evidence that the axiom of choice has a measurable geometric correlate in proof space. The authors argue that:

Structural Distinction: The classical/constructive divide is not just a philosophical stance but a structural property of proof composition that is visible in neural embeddings.
Operational Relevance: This geometric signature is not merely an abstract curiosity; it predicts the performance of automated theorem provers. The "depth law" suggests that as proofs move further from the axiom, they become structurally more similar to constructive proofs, yet the operational barrier for symbolic provers like aesop remains specific to the presence of Classical.choice.
Methodological Contribution: The work demonstrates that label-free, self-supervised learning on a single class (constructive proofs) can reveal the structural boundaries of a held-out class (classical proofs) defined by logical dependence, offering a new tool for meta-mathematical analysis.

The authors remain modest about causal mechanisms, noting that while the geometric signature and operational gap are strongly associated, the specific cause of the prover's difficulty (structural barrier vs. rule-set configuration) requires further investigation. The work is framed as an invitation to the community to identify similar structural axes in formal libraries.