Teaching Higher Category Theory with Computers

Higher category theory, also known as ∞-category theory, is now a fundamental area in modern mathematics, playing a crucial role in many areas of science, such as algebraic topology, algebraic geometry, mathematical physics, and theoretical computer science. Despite its importance, it is still known to be very abstract and technical, and hence difficult to learn without direct access to relevant experts. Formalization of mathematics is a modern approach that uses computers to precisely formulate mathematical statements and proofs via proof assistants. Initially formalization helped verify complicated mathematical results, such as the four color theorem or the liquid tensor experiment. However, in recent years proof assistants have also been used to teach mathematics and design exercises.

This workshop aims to teach participants the fundamentals of higher category theory using the proof assistant Rzk. The participants will learn both the classical point of view and the type theoretic point of view in two lecture series, and, in the exercise sessions, will learn how to use the proof assistant Rzk to prove basic higher categorical results.