Are automated proof assistants ready for semigroup research? Orientation-preserving mappings and proof assistant Lean

An orientation-preserving mapping is not always defined by how it acts on triples of elements. Although this fact is simple and well-known, it sometimes gets overlooked, resulting in wrong statements in publications. Automated proof assistants are a technology that is supposed to ensure that proofs exactly match the results, thus pre-empting mistakes. In this paper we successfully formalise the definition of orientation-preserving mappings in proof assistant software Lean and construct a computer-verified proof of the above fact.