Proof complexity is the study of the efficiency of propositional proof systems, i.e. of non-deterministic algorithms accepting exactly the set of propositional tautologies. The main problem is the NP vs. coNP problem. Bounded arithmetic studies theories of arithmetic with the induction axiom restricted only to (a subclass of) bounded formulas. The relation between bounded arithmetic and propositional proof systems is similar to the relation of Turing machines and boolean circuits.

I shall outline some basic facts of this theory, the main achievements, and fundamental open problems. No particular knowledge of the area will be assumed.