Classical math has a fingerprint, and neural networks can see it.
Researchers trained a self-supervised encoder on constructive proofs drawn from 42,355 theorems in Mathlib, the large formal mathematics library built on Lean 4. When they pointed that encoder at classical proofs — those that depend on the axiom of choice — three separate geometric measurements all flagged the difference. The signal was sharpest close to the axiom in the dependency graph (AUC 0.847 at distance 2) and faded to noise beyond distance 9, suggesting the influence dissipates as proofs grow more indirect. The result held after controlling for proof length, authorship, topic, and source file.
The finding matters because it turns a century-old philosophical divide into something operational. Lean's aesop tactic solved constructive theorems at 13 times the rate of classical ones on a 251-theorem evaluation sample; a neural-guided hybrid using the ReProver tactic generator narrowed the gap to 5 times. That gap has real consequences for anyone building automated proof systems on top of Mathlib, which has become the de facto benchmark corpus for neural theorem proving.
The axiom of choice has always been the uncomfortable guest at the foundations-of-math dinner — accepted by most working mathematicians, rejected by constructivists, and largely invisible to software. This paper suggests it is neither invisible nor irrelevant once you start asking machines to do the proving.