Terence Tao

Yes, yes, yes.

So I told you before about the split between theoretical and experimental mathematics.

And right now, most mathematics is theoretical and only a tiny bit is experimental.

I think the platform that Lean and other software tools, so GitHub and things like that, allow experimental mathematics to scale up to a much greater degree than we can do now.

So right now, if you want to...

do any mathematical exploration of some mathematical pattern or something.

You need some code to write out the pattern.

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.