Mathematics is of fundamental importance for computer science. On the otherhand, there are also many applications of computer science in mathematics, beit simulations, numerical calculations or computer algebra systems. Anotherinteresting application of this kind is the implementation of logical methodsfor investigating mathematical proofs. In recent years, large electronic libraries of formalized proofs have beendeveloped. Several case studies have demonstrated that, using such systems, it is possible to formalize proofs which are large enough to be of currentresearch interest in mathematics. This situation creates a high potential for automating existing methods for theanalysis of proofs, which have previously been applied only manually. This bookis an investigation of such a method, and in particular of the results itprovides about the mathematical content and structure of formal proofs.
