Capturing properties of planar diagrams in Lean proof assistant software

Alastair Litterick, Alexei Vernitski, Billy Woods

Automated proof assistants are a technology pre-empting mistakes in mathematics. In our practice we have seen that reasoning about planar diagrams is difficult to both humans and c…