# Symposium `Proofs and Problems' (plus ALV)

25 november 2005

The Vereniging voor Logica (VvL) organizes a symposium

Proofs and Problems

on Friday November 25, 2005, in the Jaarbeurs in Utrecht. Participation is free, registration not necessary. The programme is as follows:

12.30 - 13.30 lunch en algemene ledenvergadering 13.30 - 14.15 prof. dr. Jan van Leeuwen, Utrecht University Great Open Problems in Computational Complexity 14.15 - 14.30 tea and coffee 14.30 - 15.15 dr. Lev Beklemishev, Utrecht University Problems in the Logic of Provability 15.15 - 15.30 tea and coffee 15.30 - 16.15 prof. dr. Henk Barendregt, Radboud University State of the Art of Computer Mathematics 16.15 - 17.00 drinks

#### Abstract of the talk by Jan van Leeuwen:

Ever since it was listed among the seven Millennium Prize problems by the Clay Mathematics Institute in 2000, the P-versus-NP problem is one of the most widely known open problems of our field. The problem was `discovered' some thirty-four years ago and is known to capture the computational difficulty of many questions in efficient algorithm design, ranging from combinatorial optimization to logic and further. For known attempts to solve P-versus-NP (either way) see here. However, P-versus-NP is only one of the key open problems in complexity theory. What do we know about the problem, and what are typical open problems in other computational contexts? We survey the salient features of P-versus-NP and related problems and of some of the historic approaches and results known today such as the highly non-trivial PCP-theorem.

#### Abstract of the talk by Lev Beklemishev:

Provability logic emerged in the 1970s as a study of formal provability as a "mathematical" kind of modality. The field experienced a period of rapid development in the 80s and 90s. We shall discuss some long standing open problems in this area as well as possible directions for future research.

#### Abstract of the talk by Henk Barendregt:

Progress in the foundations of mathematics has made it possible to formulate all thinkable mathematical concepts, algorithms and proofs in one language and in an impeccable way. This not in spite of, but partially based on the famous results of Goedel and Turing. In this way statements are about mathematical objects *and* algorithms, proofs show the correctness of statements *and* computations, and computations are dealing with objects *and* proofs. Interactive computer systems for a full integration of defining, computing and proving are based on this. The human defines concepts, constructs algorithms and provides proofs, while the machine checks that the definitions are well-formed and the proofs and computations are correct. Results formalized so far demonstrate the feasibility of computer mathematics. There are very good applications. The challenge is to make the systems more mathematician-friendly, by building libraries and tools. The eventual goal is to help humans to learn, develop, communicate, referee and apply mathematics.

#### Address and how to get there

Jaarbeurs Utrecht

Jaarbeursplein 6, Beatrixgebouw, zaal 412

3521 AL Utrecht

Telefoon 030 - 295 59 11

only 10 minutes walk from Utrecht Centraal Station