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?