Feasible Proofs and Computations

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.