Computer-Assisted Theorem Proving

The use of computers to verify proofs is growing in popularity among mathematicians, computer scientists, cryptographers and analytic philosophers. Ominous as it may sound, learning to use proof assistants should not be seen as out of reach for undergraduates. We will explore some of the assistance currently available as well as other resources to help one get started. What is more, the mathematics that make machine checked proof possible are quite elegant and constitute actively researched fields in their own right. Therefore, we will also be looking at intuitionistic logic, the propositions-as-types correspondence and Martin-Löf dependent type theory – giving a taste of its connections with higher-dimensional algebra.