Propositional Proofs in Frege and Extended Frege Systems

We discuss recent results on the propositional proof complexity
of Frege proof systems, including some recently discovered quasipolynomial
size proofs for the pigeonhole principle and the Kneser-Lov´asz
theorem. These are closely related to formalizability in bounded arithmetic.