Alternatively have a look at the program.

## Directed homotopy type theory

In this talk, I will describe the development of a directed homotopy type theory. The aim is to capture (higher) categories and directed topological spaces as models of the theory, and thus use it to study phenomena such as concurrency and rewriting. I will explain homotopy type theory in a way that motivates this generalization, so prior knowledge of homotopy type theory is not required.

## Formalizing the ∞-categorical Yoneda lemma

Computer proof assistants are computer programs to check the correctness of a mathematical proof. There exists a wide variety of those, and they have been used increasingly in recent decades. Notable examples include verifications of:

* Ferguson--Hales's proof of the Kepler conjecture (2003--2014, in Isabelle)

* Feit--Thompson's Odd Order Theorem, playing a central role in the classification of finite simple groups (2006--2012, in Coq)

* some of Scholze and Clausen's work on condensed mathematics, implemented as the "Liquid Tensor Experiment" (2020--2022, in Lean)

© MPI f. Mathematik, Bonn | Impressum & Datenschutz |