Terence Tao

So for example, does commutativity imply associativity?

And the answer is no, because it turns out you can describe an operation which obeys the commutative law but doesn't obey the associative law.

So by producing an example, you can show that commutativity does not imply associativity.

But some other laws do imply other laws by substitution and so forth, and you can write down some algebraic proof.

So we look at all the pairs between these 4,000 laws, and there's about 22 million of these pairs.

And for each pair, we ask, does this law imply this law?

If so, give a proof.

If not, give a counterexample.

So 22 million problems, each one of which you could give to an undergraduate algebra student, and they had a decent chance of solving the problem.

Although there are a few, at least 22 million, there are like 100 or so that are really quite hard, but a lot are easy.

And

The project was just to work out, to determine the entire graph, like which ones imply which other ones.

Yeah, so it would not have been feasible.

I mean, the state of the art in the literature was like 15 equations and sort of how they imply.

That's sort of at the limit of what a human pen and paper can do.

So you need to scale it up

So you need to crowdsource, but you also need to trust all the, I mean, no one person can check 22 million of these proofs.

You need to be computerized.

And so it only became possible with Lean.

We were hoping to use a lot of AI as well.