Formal proof sketches

Abstract

Formalized mathematics currently does not look much like informal mathematics. Also, formalizing mathematics currently seems far too much work to be worth the time of the working mathematician. To address both of these problems we introduce the notion of a formal proof sketch. This is a proof representation that is in between a fully checkable formal proof and a statement without any proof at all. Although a formal proof sketch is too high level to be checkable by computer, it has a precise notion of correctness (hence the adjective formal). We will show through examples that formal proof sketches can closely mimic already existing mathematical proofs. Therefore, although a formal proof sketch contains gaps in the reasoning from a formal point of view (which is why we call it a sketch), a mathematician probably would call such a text just a 'proof. © Springer-Verlag 2004.