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.

翻译：自动证明辅助技术能够预先防范数学中的错误。在我们的实践中发现，平面图的推理对人类和计算机而言都具有挑战性。一个曾在出版物中导致错误陈述的典型例子是：保向映射并不总能通过其对三元组的映射作用来定义。本文在证明辅助软件Lean中形式化了保向映射，并报告了我们的研究结论。