Homotopy theory, homotopy type theory and higher topos theory

点击翻译按钮获取中文摘要

My research involves topology, algebra, logic, computation, and various topics in between. Topology is the study of surfaces and higher-dimensional shapes, and the ways in which they can be stretched, deformed and mapped into each other. We study such spaces by probing them with loops, spheres and other simple geometric shapes. This generally results in algebraic invariants which provide qualitative and computational information about a space. Topology has applications in many other fields, such as algebra, data science, physics and computer science. There are many questions and techniques that make sense in all of these settings, and the main theme of my work in topology is the study of such interdisciplinary problems. This interplay between disciplines has proven to be extremely fruitful, often providing insight that leads to solutions to open problems. I will continue to tackle such problems, with a focus on problems involving topology, algebra and geometry. Recently it has been discovered that there is a close connection between topology and logic. Type theory is a foundation for mathematics that has been studied by logicians and computer scientists since the 1970s, and we now know that it is intimately related to topology, in a deep and important way. Part of my work involves studying this relationship between topology and logic and using it to understand both subjects at a more fundamental level. One of the key features of type theory is that proofs done in this framework can be formally verified by a computer to be correct. This is useful both for ensuring correctness of traditional mathematical proofs, and also for verifying the correctness of safety critical software. Some very important results have been formally verified, increasing our confidence in the mathematical literature. In the future, I expect most mathematics to be formally verified, and my work in homotopy type theory will contribute to this while also training HQP in these important skills. Formal verification is also in heavy use in industry, e.g. at Airbus, Intel, Toyota and Microsoft.