Proof assistants for mathematics This question is related to (maybe even the same in intent as) 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 and Weedijk for examples.  Does anyone know of any such?
 A: Are you aware of the Archive of Formal Proof for Isabelle?  It's a collection of formalized mathematics (and some program verification).  Reading the papers there, and browsing the Isabelle theory file sources is a good way to learn.
The Isar tutorial is also a good place to look, if you want to write proofs that look like informal mathematics (as opposed to tactic style).  It's quite hard to get the hang of at first (mostly due to lack of documentation), but once you get it, it's a lot easier to work with than plain lists of tactics.
If you're wanting to formalise anything with name binders (lambda-calculus, FOL, programming languages, pi-calculus, etc.) you should also check out the Nominal package for Isabelle which again helps with abstracting the proofs.
A: I would like to mention Mizar, proof verification system based on language which is human readable and very near to natural mathematical language used in mathematical practice. It is one of the longest working proof checkers, and it is one of the most successful one. 
Here You may find some about it: http://www.cs.ru.nl/~freek/mizar/
There is the whole library congaing presently more that 40Mb zipped proofs ( in pure ascii files!). 
A: The best introduction to the usage of proof assistants in mathematics that I'm personally aware of is Cameron Freer's website vdash.org.  That website also links to a few resources, including the home pages of Freek Wiedijk and John Harrison, which briefly describe the usage of proof assistants in proving mathematical statements.
Unfortunately, the usability of current proof assistants seems to be extremely primitive, so introducing them in a math graduate course is going to be a challenge.  You may wish to take your question to the vdash google group and/or the FOM mailing list, where some might be able to provide you with useful suggestions or unpublished lecture notes.
A: Honestly, part of the reason that proof assistants are focused on proving programs is precisely because of our very limited understanding of how to actually represent mathematics in formal logical systems, as opposed to doing it in principle.
It turns out that program proof is basically applied metamathematics (i.e., verification of imperative programs is model theory, and verification of functional programs is structural proof theory) and this is the one area of mathematics where folks have really fully worked out in full detail how to represent what they're doing in formal logical systems. So the focus on program proof is partly making a virtue of necessity! (It's also because those of us in this area really like both programming and mathematics, and this is a great way to combine them...)
The number of people who know how to do real math in proof assistants and explain it to others can probably be counted on your fingers. A pair of suggestions to add to your list follows:

*

*John Harrison wrote a recent book, Handbook of Practical Logic and Automated Reasoning, which people I trust rave about. It's a guide to all the decision procedures (e.g., SAT solving, unification, Presburger arithmetic, Groebner bases, etc.) that you need to raise the level of formal proof to a decent level of abstraction, together with their implementations in the HOL/Light system.


*George Gonthier (who formally proved the Four Color Theorem in Coq) is currently working on formalzing the Feit-Thompson (aka Odd Order) Theorem of finite group theory. As part of this work, he and his collaborators are developing the more substantial libraries and proof automatation to support a more mathematical (as opposed to logical) style of reasoning in Coq. The guides to this work are "A Modular Formalisation of Finite Group Theory" and their Mathematical Components Library (Wayback Machine).
A: I am interested in the same kind of stuff. This article tells about work done to formalize group representation theory in Coq.
In particular, they formalize the proof of Maschke's theorem (that $F[G]$ is semisimple when $G$ is a finite group).
Some links to math courses using Coq are listed in Cocorico.
