Formalizing the ∞-categorical Yoneda lemma

Computer proof assistants are computer programs to check the correctness of a mathematical proof. There exists a wide variety of those, and they have been used increasingly in recent decades. Notable examples include verifications of:

* Ferguson--Hales's proof of the Kepler conjecture (2003--2014, in Isabelle)
* Feit--Thompson's Odd Order Theorem, playing a central role in the classification of finite simple groups (2006--2012, in Coq)
* some of Scholze and Clausen's work on condensed mathematics, implemented as the "Liquid Tensor Experiment" (2020--2022, in Lean)

Modern-day algebraic geometry and homotopy theory make heavy use of ∞-category theory, the formalization of which in a computer proof assistant has largely remained elusive. The natively homotopical flavor of ∞-category theory makes it a challenge to find a good foundational system that makes formalization amenable.

This is, in fact, made possible in the new proof assistant Rzk (https://rzk-lang.github.io/rzk [4]), developed by Kudasov. The underlying theory is based on Riehl--Shulman's simplicial type theory from 2017, a version of homotopy type theory augmented with a directed interval. This formal language permits the synthetic development of parts of ∞-category theory as done in work by Riehl--Shulman, Buchholtz--W, and Bardomiano Martínez. But these used "pen and paper" rather than a proof assistant.

Now, together with Riehl and Kudasov, we have formalized Riehl--Shulman's version of the synthetic ∞-categorical Yoneda Lemma in Rzk (https://emilyriehl.github.io/yoneda/ [5]). Additional formalizations have been contributed by Bakke in Rzk, and by Hazratpour in Lean who formalized a version of the 1-categorical Yoneda lemma.

In the talk, I'll briefly introduce the basic vocabulary of Riehl--Shulman's synthetic ∞-category theory and present a demo of the formalized ∞-categorical Yoneda lemma in Kudasov's Rzk proof assistant. Using the case study of the Yoneda lemma, we will explain the conceptual and practical advantages as well as challenges that arise when doing synthetic ∞-category theory in this setting.