A Note on ``How to Write a Proof'' 

Piotr Rudnicki and Andrzej Trybulec

Technical Report TR96-08
April 1996

Department of Computing Science
University of Alberta
Edmonton, Alberta
Canada T6G 2H1

ABSTRACT

We believe that mechanical checking of real-life proofs can
become practical and therefore we use Mizar---a proof checking
system for proofs written in a style of traditional mathematics.
In the beginning of 1994 we came across a copy of L. Lamport's
paper in which ``a method for writing proofs is proposed that
makes it much harder to prove things that are not true.'' For
Mizar users the issue of `How to Write a Proof?' is an important
one, as Mizar is a proof checker and not an automated prover.  We
have tested Mizar fitness for writing structured proofs in
Lamport's style by rewriting his proof of the irrationality of
sqrt(2) into Mizar.  It was not surprising to notice that
formatting conventions help in presenting and reading proofs.
However, such conventions do not, as they cannot, guarantee the
correctness of the written proof, our little test being a case in
point.  We advocate development and employment of mechanical
checkers for proofs.

KEYWORDS

proof-checking, automated reasoning, proving.