There's a really nice survey article on this subject by Jeremy Avigad and John Harrison (both have had concrete experience in carrying out such formalizations "by hand"): [Formally Verified Mathematics](http://dl.acm.org/citation.cfm?doid=2580723.2591012).