Open Lecture — The Limits of Proof

In the early part of the 20th century, Gödel, Turing, and Tarski showed that no consistent system of reasoning can contain proofs of important properties of the natural numbers or of computations. In these cases, the difficulty stems from the need to reason about infinities of numbers or time that don't show up in our everyday world. In contrast, proofs of properties in a bounded size world always exist.

The field of proof complexity studies the power of the many ways to express such proofs. These ways involve logic, algebra, combinatorial optimization, graph theory, and computations.

For many natural properties and methods of reasoning from these diverse fields, one can show that, though proofs exist, their sizes must be astronomical – even proofs about small worlds would require more symbols to write down than there are particles in the universe.

I will survey highlights and research directions in proof complexity and how these have implications for the P versus NP question and beyond.

Light refreshments will be served before the lecture at 3:30 p.m.