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.