Last month Kevin Buzzard gave an interesting talk "How do you convince mathematicians a theory prover is worth their time?" about how he became involved with LEAN and some of the proofs he formalised with it:
mainstream proof : constructive proof :: program code : machine code