Formalizing higher categories

Category theory is an abstract framework used to study mathematical structures and their relationships. It has significantly influenced many areas of mathematics and theoretical computer science, such as abstract algebra and type theory. However, traditional category theory cannot capture the intricacies of all mathematical domains, resulting in the development of a theory of "higher categories". This advanced theory has become pivotal in modern research areas such as algebraic topology and homotopy type theory. Unfortunately, these advancements come at a significant price, as higher category theory is notoriously technical and susceptible to errors. The formalization of higher category theory presents a promising solution to address these challenges. This has resulted in several formalization efforts, leveraging a variety of proof assistants, including a recent project in Lean, commenced by Emily Riehl: the ∞-Cosmos project. In this talk, I will explore the merits and limitations of formalizing higher category theory within Lean, share my experience with the ∞-Cosmos project, and highlight some technical obstacles that hinder further advancements. No prior knowledge of (higher) category theory will be assumed for this talk.