Proof assistants have close ties to logic and type theory, so it's not much surprise that they're quite good for doing this small, subarea of mathematics. (Inde

Proof assistants have close ties to logic and type theory, so it's not much surprise that they're quite good for doing this small, subarea of mathematics. (Indeed, I think in the not too distant future we will be teaching logic using something like an interactive theorem prover. It makes a bit of the formalism quite clearer.) There has been some push, especially in Europe, for using these programs to prove other mathematics; it is certainly possible, although few would say it is pleasant or resembles how ordinary mathematicians work. But I think that, for specific areas of mathematics, these tools are useful today. Especially when trying to teach students how to think formally; you'll find that formal corresponds closely to how the computer thinks about things (and the whole problem is that mathematicians are not very formal at all.) CPDT is not a good first text; Software Foundations http://www.cis.upenn.edu/~bcpierce/sf/ http://www.cis.upenn.edu/~bcpierce/sf/ does better for people with less math experience.