As mathematics becomes increasingly complicated, the prospect of using a computer proof assistant to (i) certify the correctness of one’s own work and (ii) interact with the formalized mathematical literature becomes increasingly attractive. In this talk, we will describe some challenges that arise when it comes to formalizing weak infinite-dimensional category theory, specifically the theory of ∞-categories developed by Joyal and Lurie. We introduce two parallel ongoing collaborative efforts to formalize ∞-category theory in two different proof assistants: Lean and Rzk. We show some sample formalized proofs to highlight the advantages and drawbacks of each formal system and explain how you could contribute to this effort. This involves joint work with Mario Carneiro, Dominic Verity, Nikolai Kudasov, and Jonathan Weinberger.

Formalized 1-category theory forms a core component of various libraries of mathematical proofs. However, more sophisticated results in fields from algebraic topology to theoretical physics, where objects have “higher structure,” rely on infinite-dimensional categories in place of 1-dimensional categories, and ∞-category theory has thusfar proved unamenable to computer formalization.

Abstract Consider a locally cartesian closed category with an object $\mathbb{I}$ and a class of trivial fibrations, which admit sections and are stable under pushforward and retract as arrows. Define the fibrations to be those maps whose Leibniz exponential with the generic point of $\mathbb{I}$ defines a trivial fibration. Then the fibrations are also closed under pushforward.