×

zbMATH — the first resource for mathematics

\(\mathsf{Globular}\): an online proof assistant for higher-dimensional rewriting. (English) Zbl 06828651
Summary: This article introduces \mathsfGlobular, 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.

MSC:
03B70 Logic in computer science
68 Computer science
Software:
Globular
PDF BibTeX XML Cite
Full Text: DOI arXiv