I will give a tour of some of the key concepts and ideas in proof complexity. First, I will define all standard propositional proof systems using the sequent calculus which gives rise to a clean characterization of proofs as computationally limited two-player games. I will also define algebraic and semi-algebraic systems (SOS, IPS, Polynomial Calculus). Then we will see one or two (mostly) self-contained lower bounds, and briefly mention how these lower bounds have been bootstrapped to prove lower bounds for several classes of algorithms: Extended Formulations of linear and semidefinite programs, monotone span programs, and monotone circuits. Throughout, I will highlight some of my favorite longstanding challenges/mysteries in the area.