Proof systems pervade all areas of mathematics (often in disguise: e.g. Reidemeister moves is a sound and complete proof system for proving the equivalence of knots given by their diagrams). Proof complexity seeks to to understand the minimal *length* of proofs relative to the length of theorem proved, mainly for propositional proof systems. In this talk I plan to survey some of the main motivations and goals, results and challenges of proof complexity, as well as its connections with circuit complexity. I will then discuss in more detail the Resolution proof system (the most basic nontrivial proof system, prevalent in automated theorem provers and in hardware verification systems), and show exponential lower bounds on proof-length in this system. No special knowledge in this area will be assumed.