Terence Tao

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.

If I talk about x, is x a real number or a natural number or a function or something?

If you write things informally,

It's often in some context.

You say, you know, clearly X is equal to, let X be the sum of Y and Z, and Y and Z were already real numbers, so X should also be a real number.

So Lean can do a lot of that, but every so often it says, wait a minute, can you tell me more about what this object is, what type of object it is?

You have to think more at a philosophical level, not just sort of computations that you're doing, but sort of what each object actually is in some sense.

It's using much more traditional, good old-fashioned AI.