Terence Tao

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.

So it creates these more complicated objects, not just statements, but statements with proofs attached to them.

And every line of code is just a way of piecing together previous statements to create new ones.

So the idea is not new.

These things are called proof assistants.

And so they provide languages for which you can create quite complicated, intricate mathematical proofs.

And they produce these certificates that give a 100% guarantee that your arguments are correct if you trust the compiler of Lean.

But they made the compiler really small.