Travel: Formalizing Higher Categories at Mittag-Leffler Institute

This award supports US participants of workshop "Formalizing Higher Categories" held June 8-12, 2026 at Mittag-Leffler Institute in Stockholm, Sweden. 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). The ambition of the conference is highly innovative, thereby boldly promoting the progress of science in the U.S. The conference will yield crucial applications for U.S. national security and defense since capturing the intricacy of infinite-dimensional compositional systems can be used in the formal verification of safety-critical systems. Infinity-categories are a natural structure in topological quantum field theory, thereby contributing to major insights in quantum computing and quantum information theory in line with pioneering research directions in the U.S. The conference will also inspire new techniques of teaching higher category theory and higher algebra, hence forming a new and innovative pathway for U.S. graduate and undergraduate education, especially augmented by modern computer proof assistants and AI. More information is available at ttps://www.mittag-leffler.se/activities/formalizing-higher-categories/ This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.