The authors study the concept of proof in mathematics and its formalization. They argue that the concept is far from stale and fully explored, but that it offers interesting facets, beyond fully formal ones (such as Venn diagrams, truth tables, syllogisms, Hilbert-style, Fitch-style, and Gentzen-style proofs). It involves interesting questions that involve the in-principle formalizability of proofs, and human checking of informal proofs. The authors give a brief historic account of proof checking systems and present more detail on Mizar, in which they formalize some examples. Important questions in the history of formalization of proofs are questions when a proof counts as a proof (e.g., in the context of the 4-color theorem, Hales’ proof of the Kepler conjecture, and the classification of finite groups). An important question that mathematicians answer in writing up a proof is what needs to be said explicitly and what can be assumed and go unsaid; in other words what is “obvious”? Starting from Davis’ definition that a formula is an obvious consequence of a formula set if there is a Herbrand proof of the formula so that each variable in the formula set needs to be instantiated only once, the authors discuss a generalization to $n$-obvious, where at most $n$ instantiations are needed and link it to the corresponding behavior of Mizar.

Reviewer:

Manfred Kerber (Birmingham)