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 applied too naively. This notion of types was refined by the concept of dependent types, with the aim of representing mathematical proofs on a computer and thereby being able to verify the correctness of these proofs. This idea of utilising computers in this way has seen significant development in recent years (verification of the proof of the odd-order theorem or, more recently, of a non-trivial result by Peter Scholze). Quite apart from this important role in the formalisation of mathematical proofs, the concept of dependent types is of intrinsic conceptual interest in logic and computer science, through the Curry–Howard correspondence between types and propositions. Some more recent results suggest that this formalism allows us to formulate new properties concerning one of the basic concepts of mathematics: the concept of equality, revealing an unexpected connection between fundamental questions in logic and abstract homotopy theory.
This lecture will trace the recent history of these discoveries, covering both the computer-aided verification of proofs and the synergy that is emerging between the theory of dependent types and homotopy theory.
