The following videos work through several examples of proofs both informally and in the proof assistant Coq.

• In the first videos we describe how to prove addition on the natural numbers is commutative. This also serves as a first simple example for proving in the system Coq.
  Paper Coq
• We next describe how proofs can be represented as certain kinds of terms. We prove a few simple propositions and then look at the corresponding proof terms. We then work through the same examples in Coq.
  Paper Coq
• In these videos we again prove a simple proposition and look at the corresponding proof term. Unlike the examples above, the example here contains a universal quantifier which must be instantiated during the proof.
  Paper Coq
• Here we prove that the triple negation of a proposition implies the single negation of a proposition. We also look at the corresponding proof term.
  Paper Coq
• Here we prove a disjunction (or) is left-distributive over conjunction (and).
  Paper Coq
• In this video we prove Leibniz equality corresponds to Coq's equality.
  Coq
• We prove the surjective Cantor theorem.
  Paper Coq
• We prove size induction.
  Paper Coq
• We show a tableau example.
  Paper

In addition to streaming them via youtube, you have the option of downloading the video files to watch or rewatch when you are offline.