Terence Tao

No two are the same.

Yeah, so it makes everything compatible and trustable.

Yeah, so currently, only a few mathematical projects can be cut up in this way.

At the current state of the art, most of the lean activity is on formalizing proofs that have already been proven by humans.

Math paper basically is...

a blueprint, in a sense.

It is taking a difficult statement, like a big theorem, and breaking it up into maybe a hundred little numbers, but often not all written with enough detail that each one can be sort of directly formalized.

A blueprint is like a really pedantically written version of a paper where every step is explained to as much detail as possible, and you're trying to make each step kind of self-contained, depending on only a very specific number of previous statements that have been proven.

so that each node of this blueprint graph that gets generated can be tackled independently of the others.

And you don't even need to know how the whole thing works.

So it's like a modern supply chain.

If you want to create an iPhone or some other complicated object, no one person can build a single object.

But you can have specialists who just, if they're given some widgets from some other company, they can combine them together to form a slightly bigger widget.

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.