Studies in mechanical verification of mathematical proofs

Abstract

This thesis is about proof checking in type theory. We will investigate the question how to mechanically verify mathematical proofs. The computer systems we consider are based on a type-theoretical framework. The method we follow is to develop a few representative case studies. This gives us the experience to draw conclusions and to give recommendations. In order to formalize the theorems presented in the case studies, we first have to develop a library of formalized mathematics. We will do this from scratch. During this development we will encounter several choices to make and problems to solve. One particular problem, namely equational reasoning, is studied in more depth and a method for dealing with it in a convenient way is presented in a separate chapter