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](http://en.wikipedia.org/wiki/Automath), in the late 60s), then the Calculus of Constructions (early Coq), and the Calculus of Inductive Constructions ([current Coq](http://http://coq.inria.fr)).  Currently a new wave of such work is being done in [homotopy type theory](http://ncatlab.org/nlab/show/homotopy+type+theory) 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](https://gforge.inria.fr/projects/coqfinitgroup/) 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](http://mizar.uwb.edu.pl/version/current/mml/tarski.miz) 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](http://www.nuprl.org), [HOL light](http://www.cl.cam.ac.uk/~jrh13/hol-light/) and [Isabelle](http://www.cl.cam.ac.uk/research/hvg/Isabelle/), 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](http://wiki.portal.chalmers.se/agda/pmwiki.php).  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](http://www.cicm-conference.org) on that topic, with this (2013) year's instalment happening in [early July](http://www.cicm-conference.org/2013/cicm.php?event=&menu=general) 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](http://en.wikipedia.org/wiki/Early_adopter) territory and growing.