There are two threads of current development in proof systems: foundational and coverage. The foundational work tries to find the best meta-theory to formalize mathematics. Out of that work first came dependent types ([AUTOMATH][1], in the late 60s), then the Calculus of Constructions (early Coq), and the Calculus of Inductive Constructions ([current Coq][2]). Currently a new wave of such work is being done in [homotopy type theory][3] as another step in this direction. Coq's library is not that large, except of course in the area of group theory where the results of the work on [Feit-Thompson][4] has produce something larger. The much larger work has happened for decades building [Mizar](http://mizar.org)'s enormous library [Note that Mizar is based on [Tarski-Grothendieck][5] set theory rather than type theory. Its library is a couple of orders of magnitude larger than anyone else's. Also worth a close look is [NuPRL][6], [HOL light](http://www.cl.cam.ac.uk/~jrh13/hol-light/) and [Isabelle][7], which all have decently sized libraries. A rather [thorough list](http://www.cs.ru.nl/~freek/digimath/index.html) of math systems has been collected by [Freek Wiedijk](http://www.cs.ru.nl/~freek/). Personally, I must admit that for the sheer joy of playing with mathematics, I rather like to use [Agda][8]. Unfortunately, its current library is fairly small, but the community is growing it quite quickly. For developing the kinds of mathematics I am currently interested in, it works quite well. This whole area is the domain currently called mechanized mathematics -- there is an [annual conference][9] on that topic, with this (2013) year's instalment happening in [early July][10] in Bath. Bottom line: none of these pieces of software are at the level of ease-of-use of say Maple or Mathematica, although some of them are probably close to SAGE. But they are evolving very quickly. They are way past the innovator stage, firmly into [early adopter][11] territory and growing. [1]: https://en.wikipedia.org/wiki/Automath [2]: https://coq.inria.fr/ [3]: https://ncatlab.org/nlab/show/homotopy%20type%20theory [4]: https://web.archive.org/web/20210617064108/https://gforge.inria.fr/projects/coqfinitgroup/ [5]: https://mizar.uwb.edu.pl/version/current/mml/tarski.miz [6]: https://www.nuprl.org/ [7]: https://www.cl.cam.ac.uk/research/hvg/Isabelle/ [8]: https://wiki.portal.chalmers.se/agda/pmwiki.php [9]: https://cicm-conference.org/ [10]: https://cicm-conference.org/2013/cicm.php?event=&menu=general [11]: https://en.wikipedia.org/wiki/Early_adopter