Terence Tao

90% of them still work, and there's a couple that are light and red.

Now I can't justify these steps, but it immediately isolates which steps you need to change.

But you can skip over everything which works just fine.

And if you program things correctly, with good programming practices, most of your lines will not be red.

And there'll just be a few places where you, I mean, if you don't hard code your constants, but you sort of

You use smart tactics and so forth.

You can localize the things you need to change to a very small period of time.

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.