Terence Tao

Are you working with computer and latex?

I'm mostly pen and paper actually.

So in my office I have four giant blackboards and sometimes I just have to write everything I know about the problem on the four blackboards and then sit on my couch and just sort of see the whole thing.

Is it all symbols like notation or is there some drawings?

There's a lot of drawing and a lot of bespoke doodles that only make sense to me.

And the beautiful blackboards you raise, it's a very organic thing.

I'm beginning to use more and more computers, partly because AI makes it much easier to do simple coding things.

If I wanted to plot a function before, which is moderately complicated, some iteration or something, I'd have to...

I remember how to set up a Python program and how does a full loop work and debug it and it would take two hours and so forth.

And now I can do it in 10, 15 minutes.

It's much, yeah, I'm using more and more computers to do simple explorations.

So Lean is a computer language, much like sort of standard languages like Python and C and so forth.

Except that in most languages, the focus is on using executable code.

Lines of code do things.

They flip bits, or they make a robot move, or they deliver you text on the internet or something.

So Lean is a language that can also do that.

It can also be run as a standard traditional language, but it can also produce certificates.

So a software language like Python might do a computation and give you that the answer is seven.

Does the sum of three plus four is equal to seven?

But Lean can produce not just the answer, but a proof that how it got the answer of 7 as 3 plus 4 and all the steps involved.