Proofs and Problemson 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

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.

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.

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.

Jaarbeursplein 6, Beatrixgebouw, zaal 412

3521 AL Utrecht

Telefoon 030 - 295 59 11

only 10 minutes walk from Utrecht Centraal Station