A peculiarity of the ∞-categories literature is that proofs are often written without reference to a concrete definition of an ∞-category, a practice that creates an impediment to formalization. We describe three broad strategies that would make ∞-category theory formalizable, which may be described as “analytic,” “axiomatic,” and “synthetic.” We then highlight two parallel ongoing collaborative efforts to formalize ∞-category theory in two different proof assistants: the “axiomatic” theory in Lean and the “synthetic” theory in Rzk. We show some sample formalized proofs to highlight the advantages and drawbacks of each approach and explain how you could contribute to this effort. This involves joint work with Mario Carneiro, Nikolai Kudasov, Dominic Verity, Jonathan Weinberger, and many others.
=== Online talk ===
Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqen...
Meeting ID: 871 4336 5195
Passcode: 541180