This course will introduce the use of interactive proof assistants both for mathematics and for work in software verification. We will introduce the basics of interactive theorem proving using the proof assistant Isabelle/HOL. Starting from elementary logical formulae, we will prove many theorems “live” in lectures, and apply what we have learned to proof exercises and challenges. Proof assistants can be both very fun and very addictive in equal measure. It is my hope to share that fun with you.