The equational theories project: a brief tour

submited by

Style Pass

2024-10-13 00:30:03

12 October, 2024 in expository, math.RA | Tags: collaboration, Equational Theory Project, machine assisted proof | by Terence Tao

Almost three weeks ago, I proposed a collaborative project, combining the efforts of professional and amateur mathematicians, automatic theorem provers, AI tools, and the proof assistant language Lean, to describe the implication graph relating the 4694 equational laws for magmas that can be expressed using up to four invocations of the magma operation. That is to say, one needs to determine the truth or falsity of the possible implications between the these 4694 laws.

The project was launched on the day of the blog post, and has been running for a hectic 19 days thus far; see my personal log of the project for a day-by-day summary of events. From the perspective of raw implications resolved, the project is (of the time of writing) 99.9963% complete: of the implications to resolve, have been proven to be true, have been proven to be false, and only remain open, although even within this set, there are implications that we conjecture to be false and for which we are likely to be able to formally disprove soon. For reasons of compilation efficiency, we do not record the proof of every single one of these assertions in Lean; we only prove a smaller set of implications in Lean, which then imply the broader set of implications through transitivity (for instance, using the fact that if Equation implies Equation and Equation implies Equation , then Equation implies Equation ); we will also shortly implement a further reduction utilizing a duality symmetry of the implication graph.

Thanks to the tireless efforts of many volunteer contributors to the project, we now have a number of nice visualization tools to inspect various portions of the (not quite completed) implication graph. For instance, this graph depicts all the consequences of Equation 1491: , which I have nicknamed the “Oberlix law” (and it has a companion, the “Asterix law“, Equation 65: ). And here is a table of all the equational laws we are studying, together with a count of how many laws they imply, or are implied by. These interfaces are also somewhat integrated with Lean: for instance, you can click here to try your hand at showing that the Oberlix law implies Equation 359, ; I’ll leave this as a challenge (a four-line proof in Lean is possible).