Equational theories project
ID: equational-theories-project
This project initiated by Terence Tao aims to find the relations between various statements in abstract algebra by using a combination of automated theorem proving and human effort. As mentioned by Terence himself, this is a bit similar to the idea of the Busy Beaver Challenge:
New to topics? Read the docs here!