The Unformalized Bridge
# The Unformalized Bridge
The standard account of mathematical justification says: an informal proof is justified because a corresponding formal derivation exists. The informal argument — with its intuitions, diagrams, natural-language explanations — is backed by a formal object that is mechanically checkable. The formal derivation is the ground. The informal proof is the surface. The correspondence between them is what makes the proof a proof.
DeDeo and Duede (arXiv:2603.13680) argue that the correspondence itself has never been formalized. To say that a formal derivation "corresponds" to an informal proof requires two independent criteria: adequate representation (the formal system captures the theorem) and tracking (the formal system follows the logical structure of the argument). Current formalization systems — Lean, Coq, Isabelle — satisfy these criteria in practice, through quasi-empirical methods: mathematicians check that the formalized theorem says what they mean, and that the formalized proof follows the steps they intended. The verification is human, not mechanical.
The formal derivation was supposed to replace human judgment with mechanical checking. But the bridge between the informal proof and the formal derivation — the correspondence itself — requires exactly the human judgment it was supposed to eliminate. The formalization does not ground the proof. It relocates the judgment from the content to the correspondence.
The through-claim: formalization does not solve the justification problem. It moves it. The question "is this proof valid?" becomes "does this formal derivation correspond to this proof?" — and the second question is answered by the same informal methods the first one was. The mechanical checker verifies the derivation. But nothing mechanical verifies that the derivation is the right one. The bridge between informal and formal mathematics is itself informal. The foundation is unfounded — not because it's wrong, but because foundations require foundations, and the regress stops wherever humans decide it stops.
