In late September this year, mathematician Terence Tao launched the equational theories project (https://teorth.github.io/equational_theories/) with the purpose of mapping out the space of equational theories of magmas; the broader objective of the project is also to experiment with a paradigm of large-scale collaborative mathematical research where results are proved with a combination of human contribution and automated tools, all formally verified using a proof assistant. The project is slightly over four weeks in and 99.9991% complete, with only 20 open conjectures remaining. This talk is about an approach used in the project to prove a broad class of anti-implications between magma laws using meta-theorems and the techniques that were used to formalize these proofs.
=== Hybrid talk ===
Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1
Meeting ID: 871 4336 5195
Passcode: 541180
