Capturing properties of planar diagrams in Lean proof assistant software
Combinatorics
2026-02-11 v2 Logic in Computer Science
Group Theory
Abstract
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 computers. One example that has led to wrong statements in publications is that an orientation-preserving mapping is not always defined by how it acts on triples of elements. In this paper we formalise orientation-preserving mappings in proof assistant software Lean and report on our take-aways.
Keywords
Cite
@article{arxiv.2511.13304,
title = {Capturing properties of planar diagrams in Lean proof assistant software},
author = {Alastair Litterick and Alexei Vernitski and Billy Woods},
journal= {arXiv preprint arXiv:2511.13304},
year = {2026}
}