Formal Proofs versus Human Proofs

A human proof explains why a statement follows and which ideas make the argument work. A formal proof supplies an expression accepted by a specified proof checker under explicit definitions and assumptions. Good mathematics benefits from both: explanatory structure helps a reader judge the statement, while mechanical checking can verify many otherwise implicit inference steps. Neither role automatically subsumes the other.

Helpful background. Proof Sketch Policy distinguishes a proved result from an imported theorem; Why Formalize Quantum Mechanics? motivates explicit mathematical interfaces.

One claim has a statement, a derivation, and an interpretation

It is useful to distinguish three objects. The statement specifies types, hypotheses, and a conclusion. The derivation shows how that conclusion follows in the selected logic. The interpretation identifies those formal objects with the mathematical or physical problem of interest.

A checker can verify the derivation without deciding whether the statement captures the intended physics. A human reader can understand the intended physics while overlooking an invalid inference. A reliable presentation therefore gives both the ordinary mathematical statement and its formal counterpart, with enough information to compare their assumptions.

The distinction is especially important when mathematical libraries use total operations. A notation such as an inverse or division can have a defined value even outside the range where its familiar cancellation law holds. The checker will enforce the hypotheses of the cancellation theorem; the author must still explain why those hypotheses are appropriate.

An isometry illustrates a hidden dimensional step

For a bounded map $V$ between Hilbert spaces, $V^*V=I$ expresses an isometric embedding. Calling it unitary additionally requires a suitable surjectivity statement, equivalently $VV^*=I$ on its codomain. In finite dimension with equal input and output dimensions, injectivity implies surjectivity. In infinite dimension, the unilateral shift is a counterexample to that inference.

A compressed human argument may say “the columns are orthonormal, hence the operator is unitary.” A formalized version must reveal whether it assumes a square finite matrix, a finite-dimensional endomorphism, or only a Hilbert-space isometry. The first two can justify the conclusion; the last cannot. The operator discussion and infinite-dimensional caveats give the mathematical context.

If a library theorem correctly proves the finite-dimensional statement, using it does not establish the infinite-dimensional version. The problem would be a mismatch of statements, not a failure of the checker.

A proof depends on definitions and imported results

In a proof assistant, tactics and elaboration help construct a proof term. The kernel checks the resulting object against the formal statement. Different systems implement this architecture differently, but the separation allows sophisticated automation to be useful without requiring every search strategy to be trusted as an oracle.

The final statement may still depend on axioms, admitted lemmas, imported results, or particular computational trust mechanisms. Inspecting only the visible last few lines misses that dependency graph. Lean’s official validation guide, for example, recommends examining theorem axioms and checking that placeholders have not entered through dependencies. Proof Assistant Preview gives a concrete workflow without claiming that an editor’s success indicator is a complete check of the mathematical claim.

An admitted theorem should be described as an assumption. A completed formal proof that depends on it proves an implication relative to that assumption, not an independent derivation of the admitted result. Ordinary papers have an analogous obligation to identify theorems they invoke.

Vacuous truth and inconsistent premises

The implication $H\Rightarrow C$ is valid when $H$ is impossible. For example, a theorem can correctly show that every normalized vector in the zero Hilbert space has a desired property: there are no such vectors. This proves nothing about a physical state satisfying the intended input promise.

Similarly, adding an axiom that contradicts the rest of a formal theory allows every proposition to follow. A checker accepting a derivation under those premises does not validate the premises. Reading the statement requires distinguishing ordinary declared foundations, genuine theorem hypotheses, and unsupported claims introduced solely to finish a proof.

Explanatory compression remains valuable

A polished mathematical account groups routine inferences around a small number of ideas, gives examples, and explains why assumptions cannot be dropped. A formal development may expose hundreds of lower-level steps. Presenting all of them is seldom the best way to teach the result.

A useful pairing is a readable proof organized by conceptual lemmas, alongside a reproducible formal artifact whose lemmas have the same meaning. The human account should state omitted technical work honestly; the artifact should make its checked scope and dependencies inspectable. The two presentations can then catch different errors without competing over which one alone constitutes all mathematical understanding.

Exercise: check a purported unitarity theorem

A theorem has hypotheses $V^*V=I$ and $VV^*=I$, and concludes that $V$ is unitary. A report cites it as proving that every norm-preserving map is surjective. What is missing from that report?

Solution

The formal theorem already assumes $VV^*=I$, which provides the missing surjectivity condition. It packages sufficient hypotheses into a unitary interface; it does not derive the second identity from norm preservation. The report would need a separate theorem obtaining that identity from its actual assumptions, such as finite dimensionality with equal dimensions. In general infinite dimension no such deduction is valid.

References

• Lean Project, The Lean Language Reference, “Elaboration and Compilation” and “Validating a Lean Proof,” elaboration, validation — the proof-construction/checking distinction and dependency inspection.
• Rocq Development Team, The Rocq Prover Reference Manual, version 9.2, “Core language,” official documentation — the small kernel and surrounding elaboration machinery.
• Wiedijk, Freek, ed., The Seventeen Provers of the World, Lecture Notes in Computer Science 3600, Springer, 2006, doi:10.1007/11542384 — different formal systems applied to a shared mathematical problem.