Are automated proof assistants ready for semigroup research? Orientation-preserving mappings and proof assistant Lean
Alastair Litterick, Alexei Vernitski, Billy Woods
TL;DR
The paper addresses the problem that orientation-preserving mappings are not fully determined by triple actions, a subtlety with implications for semigroup research. It demonstrates a formalisation in Lean 4 and provides a computer-verified proof that the triple-based criterion can fail, using the concrete example $ (0,1,0,1) $. The work develops a Lean encoding of sequences, cyclic/anti-cyclic tests, and orientation, and discusses practical challenges and potential for proving semigroup theorems. Overall, the study shows both feasibility and current limitations of automated proof assistants for rigorous mathematical verification and suggests directions for teaching and research adoption.
Abstract
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.