This question is related to (maybe even the same in intent as) https://mathoverflow.net/questions/1017/intro-to-automatic-theorem-proving-logical-foundations, but none of the answers seem to address what I'm looking for.

There are a lot of resources available for people who want to use proof assistants like Coq, Isabelle, …, to prove properties about programs—and that's no surprise, since a lot of the development of these programs is done by computer scientists.  However, I am interested in resources, and *especially* in course materials (because I'm trying to put together an independent study for a CS student), involving the use of proof assistants to prove *mathematical* statements—see the work of [Hales](https://sites.google.com/site/thalespitt/) and [Weedijk](http://www.cs.ru.nl/~freek) for examples.  Does anyone know of any such?