Terence Tao

But because all the context is there, someone else can say, oh, okay, I recognize what you need to do.

You need to apply this trick or this tool.

And you can do extremely atomic level conversations.

So because of Lean, I can collaborate effectively

you know, with dozens of people across the world, most of whom I don't, have never met in person.

And I may not know actually even whether they're, how reliable they are in their, in the proofs they give me.

But Lean gives me a certificate of trust.

So I can do, I can do trustless mathematics.

So there's so many interesting questions there.

There's always a brainstorming process first.

Math research projects, by their nature, when you start, you don't really know how to do the problem.

It's not like an engineering project where somehow the theory has been established for decades and its implementation is the main difficulty.

You have to figure out even what is the right path.

So this is what I said about cheating first.

It's like, to go back to the bridge building analogy, first assume you have an infinite budget and unlimited amounts of workforce and so forth.

Now can you build this bridge?

Okay.

Now have infinite budget but only finite workforce.

Now can you do that and so forth?

So, I mean, of course, no engineer can actually do this because they have fixed requirements.