Papers With

← All papers
First page of A correspondence problem for mathematical proof

A correspondence problem for mathematical proof

Simon DeDeo, Eamon Duede

math.HO Mar 14, 2026 · v2 math.LO
meta-study mathlib logic
Read PDF arXiv abstract
TL;DR
Philosophical analysis of proof correspondence that uses Lean/mathlib examples (primes_unbounded, sphere packing formalization, tactics) as case studies.
Abstract
Mathematical proofs are often said to justify their conclusions by indicating the existence of a corresponding formal derivation. We argue that this widespread view relies on an under-examined notion of correspondence, or what it means for a particular derivation to ”correspond” to a particular proof. Mere existence of a formalization is not enough, and a substantive account of the required correspondence resolves into two criteria – adequate representation (of the original theorem) and tracking (of the steps in the original proof). An examination of the actually-existing formalization systems we have today shows the variety of quasi-empirical ways we establish these criteria, and points towards new burdens that may be placed on the future evolution of mathematics itself.
Problem

The Standard View holds that informal proofs justify their conclusions by indicating a corresponding formal derivation. The notion of 'correspondence' between a particular informal proof and a particular formal derivation is left unanalyzed.

Approach

The authors distinguish thin readings (any derivation of the theorem) from thick readings (a derivation corresponding to the proof). They analyze correspondence into two criteria: adequate representation of the theorem and tracking of the proof's steps. They examine existing formalization practice, mainly Lean and mathlib4, including a Euclid primes example, AlphaProof outputs, tactic use, library lock-in, and the sphere packing formalization. They identify structural, causal, and explanatory routes to establishing correspondence.

Results

Establishing correspondence is argued to be a defeasible, quasi-empirical achievement. Its robustness comes from convergence across independent modes, which AI-generated proofs and library constraints can weaken.