Jiatu Li, a researcher at MIT, gives this Institute for Advanced Study computer science and discrete mathematics seminar on bounded arithmetic, the branch of logic that studies what can be proved using only polynomial-time reasoning. He starts from Cook's 1975 theory PV, which models a mathematician restricted to Boolean strings and deterministic polynomial-time algorithms, and shows how this weak system still manages to formalize the PCP theorem while apparently failing to prove the Pigeonhole Principle. The bulk of the talk covers classical and new methods for extending PV with probabilistic tools, since a polynomial-time mathematician cannot naturally reason about probability over exponentially large sets. Li closes with an unexpected payoff: cryptographic constructions built directly from the unprovability of certain statements in these arithmetic theories. The talk stays at the level of high-level ideas and assumes no background in logic, aimed at a general theoretical computer science audience rather than specialists in proof theory.