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 $\infty$-category theory has thusfar proved unamenable to computer formalization. Using a new proof assistant called Rzk, which is designed to support Riehl-Shulman's simplicial extension of homotopy type theory for synthetic $\infty$-category theory, we provide the first formalizations of results from $\infty$-category theory. This includes in particular a formalization of the Yoneda lemma, often regarded as the fundamental theorem of category theory, a theorem which roughly states that an object of a given category is determined by its relationship to all of the other objects of the category. A key feature of our framework is that, thanks to the synthetic theory, many constructions are automatically natural or functorial. We plan to use Rzk to formalize further results from $\infty$-category theory, such as the theory of limits and colimits and adjunctions.

翻译：形式化的 $1$-范畴理论构成了多种数学证明库的核心组成部分。然而，从代数拓扑到理论物理等领域中涉及“高维结构”的更复杂结果，依赖于无限维范畴而非 $1$ 维范畴，而 $\infty$-范畴理论迄今尚未能实现计算机形式化。我们利用一种名为 Rzk 的新型证明助手——该工具旨在支持Riehl-Shulman关于同伦类型理论的单纯扩张，以进行综合 $\infty$-范畴理论——实现了 $\infty$-范畴理论结果的首次形式化。其中特别包括Yoneda引理的形式化——该引理常被视为范畴论基本定理，其大致表述为：给定范畴中的一个对象由其与范畴中所有其他对象的关系所决定。我们框架的一个关键特征是，得益于综合理论，许多构造自动具备自然性或函子性。我们计划使用Rzk进一步形式化 $\infty$-范畴理论的其他结果，例如极限与余极限理论以及伴随函子。