  Some understanding of the notion of proof is necessary for any  mathematician, if for nothing else, then at least for the  communicability of mathematical results: publication rests on the  understanding that proofs can be made as explicit as to be routinely  checkable for correctness. However, proof theory has so far not  become a practical tool for the working mathematician; the  applications in mathematics have been rather isolated cases. Recent  work on formalizing mathematical proofs with computerized systems,  called proof editors, may gradually change this picture.