Pacific Institute for the Mathematical Sciences - PIMS

The concepts of proof and computation are central to virtually any
intellectual human activity. However, before the remarkable advances of
the 20th century mathematical logic, the border between them had never
been sharp even in the context of pure mathematics. It was only in the
work of these great logicians that the separation between proofs and
computations became rigorous and (as many thought) final.

This talk is devoted to a reverse trend that results from
adding the new element of feasibility (or efficiency) into this
millennial-old brew. Strangely enough, this seemingly "orthogonal"
addition has lead to many new intriguing facets of the interaction
between (slightly compromised versions of) proofs and computations not
existing in the classical world. We will attempt a highly informal tour
through the areas where these new phenomena happen, like Propositional
Proof Complexity, NP-Completeness and (time permitting) Interactive and
Probabilistically Checkable Proofs. And we will try to convey, using
concrete and intertwined examples, the general feeling of complexity
and intricacy of relations between proofs and computations in this
emerging reality.

10th Anniversary Speaker Series 2006