Return to Question

This question is related to (maybe even the same in intent as) Question 1017, 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?

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?

This question is related to (maybe even the same in intent as) Question 1017, 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?

This question is related to (maybe even the same in intent as) Question 1017, 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?