Capturing properties of planar diagrams in Lean proof assistant software

TL;DR

This paper formalizes orientation-preserving mappings in the Lean proof assistant to improve reasoning about planar diagrams, addressing common difficulties faced by humans and computers.

Contribution

It introduces a formalization of orientation-preserving mappings in Lean, providing a new approach to reasoning about planar diagrams in proof assistants.

Findings

Formalization clarifies properties of planar diagrams

Reduces errors in mathematical publications involving diagrams

Enhances proof automation in Lean

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.