Intuitionism and more generally constructive mathematics is enjoying a renaissance. Surprising connections between the traditionally distant areas of mathematical logic and geometry have emerged through the constructive Univalent Foundations of Mathematics research program, formulated by the Fields medallist Voevodsky. Areas of mathematics such as abstract algebra that appeared to be dominated by highly incomputable objects have shown surprising amenability to constructive approaches.
Our central claim is that much of mathematics and related areas (e.g. philosophy and computer science) can benefit from the subtler distinctions and structures revealed by constructivization, i.e., by replacing classical with intuitionistic reasoning. This study reveals some of the fundamental structures of mathematics and potentially of physical reality.
Building a strong team at the interface of logic and computing, we target several areas where constructivization will produce important insights. Our specific research topics exhibit considerable breadth across mathematics, philosophy, and computing that encompasses univalence, intuitionistic type theory, algebra, philosophy of mathematics, proof theory, and complexity.
Project publications in prestigious scientific journals and conference proceedings will showcase the importance of intuitionism across mathematics, computer science, and philosophy, and inspire further researchers to contribute to our vision of an intuitionistic renaissance.
Our project will also reach out to working mathematicians and computer scientists and raise their awareness for the advantages of constructivism: by involving them in collaborative research and through specifically designed impact activities: a project workshop, a spring school at the Hausdorff Institute Bonn, and a series of lectures on intuitionism. We will also publish a broad survey and deliver talks at international conferences and seminars.
