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.