The Code of Mathematics

TL;DR

This paper explores the evolution of mathematical concepts like truth and equality, emphasizing recent advances in dependent type theory and infinity categories, highlighting their implications for mathematics and computer science.

Contribution

It provides a historical overview and discusses recent developments in dependent type theory and homotopy type theory, illustrating their significance for foundational mathematics and computer science.

Findings

Dependent type theory enables new ways to handle equality and isomorphisms.

Homotopy type theory offers a unifying framework connecting logic, topology, and category theory.

These theories support computer-assisted proofs and software verification.

Abstract

This text summarizes and expands the content of a general audience talk given in 2018 at the University of Mainz. Motivated by recent developments in dependent type theory and infinity category theory, it presents a history of ideas around the concepts of truth, proof, equality, and equivalence as well as their relation to human thought. We describe a few selected ideas of Platon, Aristoteles, Leibniz, Kant, Frege and others and then pass to the results of G\"odel and Tarski about incompleteness, undecidability and truth in deductive systems and their semantic models. The main focus of this text, however, is the development of dependent type theory through the work of Per Martin--L\"of and recent developments in homotopy type theory, i.e., the univalent foundations program of Vladimir Voevodsky and others. These theories allow the notion of identity types, which gives new possibilities for handling equality, symmetry, equivalence and isomorphisms in a conceptual way. Martin--L\"of type theories have semantic models in (infinity,1)-categories, which are related to simplicial localizations of Quillen model categories. The interaction of type theory with infinity category theory is a new paradigm for a structural view on mathematics which is superior to set theory. It also supports the recent emerging trend for computer assisted proofs in mathematics and verification of algorithms and software in computer science.