Terence Tao

So it's like within a day or two, we had updated our proof.

Of course, this is a very quick process.

You make a change, there are 10 things now that don't work.

For each one, you make a change, and now there's five more things that don't work, but the process converges much more smoothly than with pen and paper,

Yeah, so the proofs are longer, but each individual piece is easier to read.

So if you take a math paper and you jump to page 27 and you look at paragraph 6 and you have a line of text of math, I often can't read it.

immediately because it assumes various definitions, which I have to go back and maybe on 10 pages earlier, this was defined.

And the proof is scattered all over the place.

And you basically are forced to read fairly sequentially.

It's not like, say, a novel where in theory, you could open up a novel halfway through and start reading.

There's a lot of context

But with a proof in Lean, if you put your cursor on a line of code, every single object there, you can hover over it and it will say what it is, where it came from, where it was justified.

You can trace things back much easier than flipping through a math paper.

So one thing that Lean really enables is actually collaborating on proofs at a really atomic scale that you really couldn't do in the past.

So traditionally with pen and paper, when you want to collaborate with another mathematician,

Either you do it at a blackboard where you can really interact, but if you're doing it sort of by email or something, basically, yeah, you have to segment it.

So I'm going to finish section three, you do section four, but you can't really sort of work on the same thing collaboratively at the same time.

But with Lean, you can be trying to formalize some portion of the proof and say, I got stuck at line 67 here.

I need to prove this thing, but it doesn't quite work.

Here's the three lines of code I'm having trouble with.