Abstract
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 type is of intrinsic conceptual interest in logic and computer science, through the Curry-Howard correspondence between types and propositions. More recent results indicate that this formalism can be used to formulate new properties on one of the basic notions of mathematics : the notion ofequality, with an unexpected rapprochement between basic questions of logic and abstract homotopy theory.
This lesson will trace the recent history of these discoveries, both around the verification of proofs on computers and the synergy that is being established between dependent type theory and homotopy theory.
