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.

翻译：形式化严谨性使数学区别于其他学科，即数学命题需通过可逻辑验证的步骤从显式公理推导得出。交互式定理证明器通过使用完全形式化的语言表达定义、定理及证明，并对其进行机械验证来支撑这一特性。我们探讨将已发表数学成果全部形式化为机器可验证、持续更新的数学知识语料库这一基准问题。该视角将数学视为由相互依存的成果构成的结构化数据库，由此引发对大规模形式化库的可扩展性与组织管理的思考。作为案例研究，我们展示正在进行中的范畴代数形式化工作——范畴的膨胀，该概念扩展了经典局部化理论，并直观呈现此类实现的具体实践样貌。