Terence Tao

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.

And there are several different compilers available for the same language.

So lean, a lot of mathematicians were involved in the design of lean.

So it's designed so that

individual lines of code resemble individual lines of a mathematical argument.

You might want to introduce a variable.

You might want to prove a contradiction.

There are various standard things that you can do, and it's written so that ideally it should be like a one-to-one correspondence.

In practice, it isn't because Lean is like explaining a proof to an extremely pedantic colleague

who will point out, okay, did you really mean this?

What happens if this is zero?

How do you justify this?

So Lean has a lot of automation in it to try to be less annoying.

So for example, every mathematical object has to come with a type.