Is formal proof (formalized mathematics) interesting to practicing mathematicians? To educators?  Formalizing mathematical proofs so that they can be checked for correctness and manipulated by computer is a recurrent proposal, most notably stated in the QED manifesto (1994).  The December 2008 issue of Notices of the AMS is entirely devoted to the state of the art in formal proof; an informal, general interest overview is provided by Cameron Freer's website vdash.org.
As practicing mathematicians, what's your perception of formal proof and interactive proof assistants?  Are you familiar with current systems?  Should they be used in mathematical education?
What are the obstacles to formal proof becoming a generally used tool, besides the effort required to build a useful library of current mathematical knowledge?
 A: Carlos Simpson, in the nineties wrote "Descente pour les n-champs" together with Andre Hirschowitz. Apparently they were quite ahead of their time: No one could be found to referee their paper. So to know whether it is correct or not, Simpson started developing an automatic theorem-checking program for category theoretical statements. Later it turned out that there was a small inaccuracy (they used covers where they needed hypercovers), but I don't know if it was found by help of the program...
Anyway it clearly shows how it can be useful. 
A: I'm not sure the question is real an MO question, but I'll bite; the three greatest obstacles are:


*

*a theorems database (that's the easiest one)

*a reasonable algorithm which can bridge trivial steps (they are trying to build one for years)

*a reasonable language (the closest you have is Mizar, and it's very far from the way we write math)
In the current state of afairs, I don't think they are usefull even as proof verifiers, let alone proof assistants (I'm not refering to CASs - but to auto-proof verifiers).
A: I think that this is being used to verify results notably the Kepler conjecture by the Flyspeck project. So this is now one way to try to prove theorems and thus is of interest to practicing mathematicians.
