  We present several known formalizations of theorems from computational
complexity in bounded arithmetic and formalize the PCP theorem in the theory
PV1 (no formalization of this theorem was known). This includes a formalization
of the existence and of some properties of the (n,d,{\lambda})-graphs in PV1.
