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.
cody
- 1.5k
- 15
- 53