Mathematics and Computation

A blog about mathematics for computers

Every proof assistant: introducing – a proof assistant for geometrical higher category theory

After a short pause, our next talk in the series will be given by Jamie Vicary, who will present a proof assistant in which the proofs are drawn!

Introducing A proof assistant for geometrical higher category theory

Time: Thursday, November 26, 2020 from 15:00 to 16:00 (Central European Time, UTC+1)
Location: online at Zoom ID 989 0478 8985
Speaker: Jamie Vicary (University of Cambridge)
Proof assistant:


Weak higher categories can be difficult to work with algebraically, with the weak structure potentially leading to considerable bureaucracy. Conjecturally, every weak infty-category is equivalent to a "semistrict" one, in which unitors and associators are trivial; such a setting might reduce the burden of constructing large proofs. In this talk, I will present the proof assistant, which allows direct construction of composites in a finitely-generated semistrict (infty,infty)-category. The terms of the proof assistant have a geometrical interpretation as string diagrams, and interaction with the proof assistant is entirely geometrical, by clicking and dragging with the mouse, completely unlike more traditional computer algebra systems. I will give an outline of the underlying theoretical foundations, and demonstrate use of the proof assistant to construct some nontrivial homotopies, rendered in 2d and 3d. I will close with some speculations about the possible interaction of such a system with more traditional type-theoretical approaches. (Joint work with Lukas Heidemann, Nick Hu and David Reutter.)


Post a comment:
Write your comment using Markdown. Use $⋯$ for inline and $$⋯$$ for display LaTeX formulas, and <pre>⋯</pre> for display code. Your E-mail address is only used to compute your Gravatar and is not stored anywhere. Comments are moderated through pull requests.