This course is an introduction to the field of proof assistants, also known as proof checkers or interactive theorem provers. These are implementations of logical systems, programs for the development and verification of formal proofs, both for mathematics and for computer science.  The course presents the current state of the art in proof assistants, and then teaches two specific proof assistants in detail.  
The first of these is the Isabelle system.  With this proof assistant we focus on the user perspective, and will develop a non-trivial proof in full detail.  The second is the HOL system.  With this system we focus on the implementation architecture and automation of the system.  Finally an overview of the main current proof assistants is presented, and some of the large efforts in this area that are currently ongoing are reviewed.

Proof assistants, both for mathematics and for computer science, are one of the research topics of the Intelligent Systems group.