About a century ago Hilbert initiated his program to secure the foundations of mathematics and to establish once for all the indubitability of mathematical truth. After 100 years of stormy developments, both undermining and reinstalling parts of his program, it is now the time to re-evaluate Hilbert's questions for the 21st century. Unlike in past decades where mathematics and computer science evolved along divergent lines, this renewed approach requires the attention and combined effort of mathematicians and computer scientists. We plan to fruitfully combine recent advances in constructive mathematics, computational complexity, and algorithm design to approach the following questions: Can abstract mathematics be used to work for the concrete? How can abstract mathematical proofs be transformed into finite methods, and eventually into efficient algorithms?
Building a strong team of mathematicians and computer scientists and closely collaborating with leading experts we plan to initiate a new 'Hilbert Program for Actual Computation'. We will concentrate on four representative case studies bridging and involving several sub-disciplines of mathematics and computing; among them algebra, constructive mathematics, proof theory and proof complexity, type theory, and algorithms and complexity. We strongly believe that our findings in the case studies together with the cross-fertilization between the subjects involved will have a catalysing effect on the research community at large. Our project will substantially comprise of collaborative research across established research boundaries, and thus prepare the grounds for a truly interdisciplinary renewed Hilbert program that addresses the computational challenges of the 21st century. The main project output will be theoretical investigation in form of high quality research papers. By organizing a workshop we will discuss our new approach with a broad audience of mathematicians, computer scientists, and philosophers.
