Reproduce “Globular: an online proof assistant for higher-dimensional rewriting” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Krzysztof Bar, Aleks Kissinger, Jamie Vicary
Globular is an online proof assistant designed to formalize and verify proofs in semistrict globular higher category theory, supporting structures up to quasistrict 4-categories. It provides interactive graphical visualizations for constructing complex higher-dimensional proofs and has been used to formalize challenging results in algebra, topology, and category theory, many of which were impractical with previous tools.
Key insights
- Higher-dimensional categorical proofs can be effectively formalized and visualized through a web-based, interactive platform, making complex mathematics more accessible.
- Explicitly integrating 'homotopy moves' within a higher-dimensional rewriting system is crucial for accurately capturing the essential non-strictness of semistrict higher categories.
- A client-side architecture for a proof assistant can significantly lower adoption barriers and facilitate research collaboration by enabling direct sharing of verifiable proofs via hyperlinks.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.