Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a video presentation from the CPP 2025 conference where Emily Riehl from Johns Hopkins University discusses the challenges and opportunities in computer formalization of infinite-dimensional category theory. Learn about two parallel collaborative efforts to formalize ∞-category theory in different proof assistants: Lean and Rzk. Discover how these formal systems compare through sample proofs, highlighting their respective advantages and limitations. The talk addresses how computer proof assistants can certify mathematical work and facilitate interaction with formalized mathematical literature, particularly for the complex theory of ∞-categories developed by Joyal and Lurie. This presentation, part of the ACM SIGPLAN-sponsored CPP 2025 conference (January 20-21, 2025), includes joint work with Mario Carneiro, Dominic Verity, Nikolai Kudasov, and Jonathan Weinberger, and offers insights on how viewers can contribute to these formalization efforts.
