Terence Tao

So there was a theorem I formalized, and there was a certain constant 12 that came out in the final statement.

And so this 12 had to be carried all through the proof, and everything had to be checked.

All these other numbers had to be consistent with this final number 12.

So we wrote a paper through this theorem with this number 12.

And then a few weeks later, someone said, oh, we can actually improve this 12 to an 11 by reworking some of these steps.

And when this happens with pen and paper, every time you change a parameter, you have to check line by line that every single line of your proof still works.

And there can be subtle things that you didn't quite realize.

Some properties on number 12 that you didn't even realize that you were taking advantage of.

So a proof can break down at a subtle place.

So we had formalized the proof with this constant 12.

And then when this new paper came out, we said, oh, so that took like three weeks to formalize, and like 20 people to formalize this original proof.

I said, oh, but now let's update the 12 to 11.

And what you can do with Lean is that you just, in your headline theorem, you change it 12 to 11, you run the compiler, and like of the thousands of lines of code you have,

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.