Formal rigor distinguishes mathematics from other disciplines, in the sense that mathematical statements are derived from explicit axioms by logically verifiable steps. Interactive theorem provers support this by expressing definitions, theorems, and proofs in a fully formal language and verifying them mechanically. We consider the benchmark problem of formalizing all published mathematics as a machine verifiable and continuously updated corpus of mathematical knowledge. This viewpoint treats mathematics as a structured database of interdependent results and raises questions about scalability and organization of large formal libraries. As a case study, we present an ongoing formalization in categorical algebra, namely dilatations of categories, extending classical localizations and illustrating what such an implementation looks like in practice.

翻译：形式化严谨性使数学区别于其他学科，其核心在于数学陈述需通过逻辑可验证的步骤从显式公理推导得出。交互式定理证明器通过用完全形式化的语言表达定义、定理和证明，并通过机械方式验证其正确性来支持这一过程。我们提出将所有已发表数学形式化为机器可验证且持续更新的数学知识库这一基准问题。该视角将数学视为相互依赖结果的结构化数据库，并引发关于大规模形式化库的可扩展性与组织方式的思考。作为案例研究，我们展示了范畴代数中一项正在进行的形式化工作——范畴的膨胀（dilatations），该概念扩展了经典的局部化理论，并直观呈现了此类实现的具体实践形态。