
06489645
a
2016b.00476
Alama, Jesse
Kahle, Reinhard
Checking proofs.
Aberdein, Andrew (ed.) et al., The argument of mathematics. Dordrecht: Springer (ISBN 9789400765337/hbk; 9789400765344/ebook). Logic, Epistemology, and the Unity of Science 30, 147170 (2013).
2013
Dordrecht: Springer
EN
E50
E20
A30
E30
proof
formalization
obivousness
human checking
doi:10.1007/9789400765344_9
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, Hilbertstyle, Fitchstyle, and Gentzenstyle proofs). It involves interesting questions that involve the inprinciple 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 4color 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.
Manfred Kerber (Birmingham)