Terence Tao

I mean, sometimes there are some computer algebra packages that help, but often it's just one mathematician coding lots and lots of Python or whatever.

And because coding is such an error-prone activity, it's not practical to allow other people to collaborate with you on writing modules for your code, because if one of the modules has a bug in it, the whole thing is unreliable.

So you get these bespoke...

spaghetti code written by non-professional programmers, mathematicians.

And they're clunky and slow.

And so because of that, it's hard to really mass-produce experimental results.

But

Yeah, but I think with Lean, I mean, so I'm already starting some projects where we are not just experimenting with data, but experimenting with proofs.

So I have this project called the Equational Theories Project.

Basically, we generated about 22 million little problems in abstract algebra.

Maybe I should back up and tell you what the project is.

Okay, so abstract algebra studies operations like multiplication and addition and their abstract properties.

Okay, so multiplication, for example, is commutative.

X times Y is always Y times X, at least for numbers.

And it's also associative.

X times Y times Z is the same as X times Y times Z. So these operations obey some laws and they don't obey others.

For example, X times X is not always equal to X. So that law is not always true.

So given any operation, it obeys some laws and not others.

And so we generated about 4,000 of these possible laws of algebra that certain operations can satisfy.

And our question is, which laws imply which other ones?