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$-范畴论结果的形式化。其中特别包括米田引理的形式化，该引理常被视为范畴论的基本定理，大致描述了一个给定范畴中的对象由它与该范畴中所有其他对象的关系所决定。我们框架的一个关键特征是，得益于综合理论，许多构造自动具有自然性或函子性。我们计划利用 Rzk 进一步形式化 $\infty$-范畴论的结果，例如极限与余极限理论以及伴随函子。