The PCP theorem says that any mathematical proof can be written in a special "PCP" format such that it can be verified, with arbitrarily high probability, by sampling only a few symbols in the proof. Hence the name, Probabilistically Checkable Proofs (PCPs). Alternatively and equivalently, any system of multivariate polynomial equations can be efficiently converted into another, so that if no input satisfies all equations in the former, no input satisfies even a tiny fraction of the equations in the later. Moreover, each of the new equations will involve only 3 variables.
This theorem is the key to understanding the difficulty of approximation and optimization problems; and also amazingly finds uses in modern cloud computing protocols. We will explain the context and meaning of the theorem, and outline a proof that relies on expander graphs, which are a central combinatorial object in numerous computer science and mathematical areas.