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?
Best Answer
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.