The field of category theory seeks to unify and generalize concepts and constructions across different areas of mathematics, from algebra to geometry to topology and also to logic and theoretical computer science. 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 thus far 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$-范畴论的其他成果，例如极限、余极限及伴随理论。