一句话：介绍 Globular——一个用图形化界面形式化并验证高维范畴论证明的在线证明助手。
本文介绍 Globular，一个面向高维范畴论证明的形式化与验证的在线证明助手。高维证明涉及复杂的重写结构，传统方法难以形式化。Globular 通过图形化方式可视化高维证明，提供点击式界面辅助构造，并利用类型检查阻止错误的重写步骤。它托管于网页，使用门槛低，还支持从研究论文中直接超链接到已形式化的证明。作者给出若干来自逻辑、拓扑与代数的例子，表明该工具能形式化其他方法无法处理的高维证明。
This article introduces Globular, an online proof assistant for the formalization and verification of proofs in higher-dimensional category theory. The tool produces graphical visualizations of higher-dimensional proofs, assists in their construction with a point-and- click interface, and performs type checking to prevent incorrect rewrites. Hosted on the web, it has a low barrier to use, and allows hyperlinking of formalized proofs directly from research papers. It allows the formalization of proofs from logic, topology and algebra which are not formalizable by other methods, and we give several examples.
@article{paperbot433,
title = {Globular: an online proof assistant for higher-dimensional rewriting},
author = {Krzysztof Bar and Aleks Kissinger and Jamie Vicary},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 1},
year = {2018},
doi = {10.23638/lmcs-14(1:8)2018}
}