The project as described in the article is to produce a graph (Poset) where each node is a law (say the commutativity equation for example) and each edge is either a proof of implication or a proof of a non-implication, since this graph is infinite the project limits the laws considered to up to 4 applications of the binary operator.

The main goal is not the proofs themselves but experimenting in doing math in a matter that's more similar to software engineering in the open source community.

The collaborative aspect of the project is to write a proof for each kind of edge (implication and not_implications) between the 4694 considered nodes.

There's also the advantage that a GitHub CI running lean will be setup to automatically check if the pull requests adding theses edges are right or wrong without the need for a human to do the checking of the proofs in their head.

partial visualization of the (WIP) graph: https://github.com/teorth/equational_theories/blob/0e67dad3b...

outline of the project: https://teorth.github.io/equational_theories/blueprint/

github repo: https://github.com/teorth/equational_theories

> So, the situation here is somewhat similar to the Busy Beaver Challenge, in that past a certain point of complexity, we would necessarily encounter unsolvable problems

I must be a platonist to squirm about this. There are no unsolvable problems with undecidability or busy beaver numbers. The only thing is some math questions are actually infinitely many problems disguised as a single problem.

The halting problem etc is the opposite of unsolvable, it’s so solvable humanity can never finish solving it. It’s infinitely solvable.

It’s as if we found a magical soup which has a new taste every day forever, and we call it “untasteable”. It’s not untasteable! It’s the tastiest thing ever!

Perhaps a hopefully-compressible correlation matrix, sorted and collapsed on similarity, with mouseover to get equations?