Homotopy theory, homotopy type theory and higher topos theory

我的研究涉及拓扑学、代数、逻辑学、计算，以及介于两者之间的各种主题。拓扑学研究的是表面和高维形状，以及它们可以拉伸、变形和相互映射的方式。我们研究这样的空间，用环、球和其他简单的几何形状探测它们。这通常会产生代数不变量，它提供了关于空间的定性和计算信息。拓扑学在许多其他领域都有应用，如代数、数据科学、物理和计算机科学。有许多问题和技术在所有这些设置中都是有意义的，我在拓扑学方面工作的主题就是研究这些跨学科问题。学科之间的这种相互作用已被证明是非常富有成效的，经常提供导致解决开放式问题的见解。我将继续解决这些问题，重点是涉及拓扑、代数和几何的问题。近年来，人们发现拓扑学与逻辑学之间有着密切的联系。类型论是数学的基础，自20世纪70年代以来一直被逻辑学家和计算机科学家研究，我们现在知道它与拓扑学密切相关，以一种深刻而重要的方式。我的部分工作涉及研究拓扑和逻辑之间的关系，并利用它在更基本的层面上理解这两个主题。类型论的一个关键特征是，在这个框架中完成的证明可以被计算机正式验证为正确的。这既有助于确保传统数学证明的正确性，也有助于验证安全关键软件的正确性。一些非常重要的结果已经得到了正式的验证，增加了我们对数学文献的信心。在未来，我希望大多数数学都能得到正式的验证，我在同伦类型理论方面的工作将有助于这一点，同时也将训练HQP这些重要的技能。正式验证在工业中也被大量使用，例如空客、英特尔、丰田和微软。

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.