Forbidden substructure theorems: A computational tool applied to varieties of lazy magmas

A forbidden substructure theorem characterizes a class of mathematical objects within an overclass through a list of forbidden substructures. One typical example of such a theorem is: a graph is bipartite if and only if it does not contain cycles of odd length . At the conference on Artificial Intelligence Theorem Proving (AITP) in 2020, Wesley Fussner presented a forbidden substructure theorem for lattices, found using a combination of AITP tools and proofs by hand; he concluded by conjecturing that it should be possible to develop a fully autonomous AITP tool capable of conjecturing and proving forbidden substructure theorems without human intervention. The goal of this paper is to answer that conjecture in the affirmative. After introducing the algorithm behind our tool, we demonstrate its power by proving many new forbidden substructure theorems. In particular, a recent paper provides the partially ordered set of all lazy magma (groupoid) varieties. Our tool, working in fully autonomous mode, managed to derive a forbidden substructure theorem for each inclusion in that paper. This tool is available to any mathematician on a free online website. The paper ends with a list of open problems.