Type theory was introduced by Bertrand Russell to avoid the paradoxes that arise in mathematics when the notion of a collection of objects is used too naively. This notion of types was refined by the notion of dependent types, with the aim of representing mathematical proofs on the computer, and thus being able to check the correctness of these proofs. The idea of using computers in this way has been gaining ground in recent years (e.g. verification of the proof of the Odd Order Theorem or, more recently, of a non-trivial result by Peter Scholze). Independently of this important role in the formalization of mathematical proofs, the notion of dependent types is also of intrinsic conceptual interest in logic and computer science, through the Curry-Howard correspondence between types and propositions. What's more, Voevodsky was able to give the notion of dependent type a natural semantics in abstract homotopy theory, and this unexpected rapprochement between basic questions of logic and homotopy theory appears fundamental.
The lecture we propose for 2024-2025 is part of this proliferation of ideas around type theories. In the first part, the theory of dependent types will be presented in detail, along with the metamathematical properties that justify its use for proof verification on computers. The second part of the lecture will be devoted to the synergy that is being established between this theory and homotopy theory.