Formalizing Higher Categories

Higher category theory is now a fundamental aspect of modern mathematics, playing a crucial role in algebraic topology, algebraic geometry, mathematical physics, and theoretical computer science, among others. Despite its important role throughout mathematics, the inherent complexity of higher categorical methods often results in subtle errors and impedes communication with the broader mathematical community. These challenges have motivated the higher categorical community to pursue effective solutions.

One way to overcome these challenges is the formalization of higher category theory. Formalization of mathematics translates mathematical statements into a computer-programmable language, which are then verified via suitable programming languages, such as Lean or Rocq. In recent years, formalization has successfully verified crucial results in many areas of mathematics, ranging from algebra (liquid tensor experiment) to homotopy theory (homotopy type theory).

In this event, we gather experts from both areas, formalization and higher category theory, with the aim of formalizing major higher categorical results. By combining the experience and expertise from both camps, we can set formalization goals that are both relevant and feasible, bringing higher categorical knowledge to the formalization community, and conversely making tools from formalization more accessible to researchers in higher category theory. As a result of this event, we aim to significantly contribute to higher category theory libraries. This will enable the formal verification of cutting-edge research in various applications thereof, such as homotopy theory or derived algebraic geometry.