I will present a new proof assistant, Globular, which allows the formalization of compositional proofs in higher category theory. The interface is geometrical, with proofs depicted as string diagrams, and allowing direct click-and-drag manipulation of proofs in a simple and intuitive way, up to the level of 4-categories. I will show how to build a simple proof from scratch, and present some sophisticated formalized proofs from topology and algebra. I will also give some details of the theoretical basis, which gives a new and simple way to understand higher category theory. This talk will be accessible, and will not require any previous knowledge.

Web site: https://ncatlab.org/nlab/show/Globular Paper: https://arxiv.org/abs/1610.06908