Interesting project for anyone who want to start learning lean and contribute to a project.

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

I really love the extent to which Terry Tao has embraced the promise and potential of proof assistants. So many smart and talented people in that community doing so much amazing work. With folks like these pushing the boundaries, the sky is the limit.

I love this! Let’s not take for granted that such simple mathematics problems may not have ever been solved yet. What a time to be alive.

> 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!

upvoting this hoping someone can dumb it down for me a bit :sweat_smile:

> presents the partially known poset in a visually appealing way

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

This is a great post, and full of inspiring ideas for what kind of work flows and features a modern theorem proving system could support.

I have to wonder whether there's a magma where equation 4 holds while equation 7 (commutativity) doesn't. Off the top of my head, I can't think of one but does that mean there absolutely can't be one, like the depicted graph implies?