Quite a pity that the slides don't show any reasonably complex proofs, only trivial things.

Have you looked at Coq (http://coq.inria.fr)? It's in the same direction but more complex/advanced (or complicated, if you like). They proved the 4 color theorem with it.