The same comment and question could be applied to just about any area of mathematics. To my knowledge, nobody has really worked on formalizing computational complexity theory. Formalization is still hard work; an experienced person will take about a week to formalize about a page of an undergraduate textbook. Therefore, people have mostly focused on "flashy" theorems, for which you can get some kind of recognition for the work that you put into writing up the formal proof. Formalizing routine undergraduate material is a time-consuming task for which almost nobody will thank you (or pay you).

If you do write a formal proof, then of course you need to give all the details. However, sometimes you can do better than the most naive approach of literally mimicking the original human proof. For example, when Gonthier formalized the proof of the four-color theorem, he figured out ways to slicken the proof and make it easier to formalize, as he explained in his Notices article. Most likely, if a serious effort were made to formalize large chunks of computational complexity theory, shortcuts would be devised so that (to address your specific question) Cook- or Karp-reductions from one problem to another could be coded up in a more human-friendly form, with the computer automating certain parts of the process. This is not a trivial matter, though, which is why writing formal proofs is still too tedious for most mathematicians to want to contemplate.

exceptTuring machines. $\endgroup$ – Andreas Blass Sep 27 '11 at 21:25