Terence Tao

I suggest using this tool.

And it'll find this lovely argument using a completely different tool, which eventually goes into the weeds and say, no, no, no, try using this.

Okay.

And it might start using this and then it'll go back to the tool that it wanted to do before.

And you have to keep railroading it onto the path you want.

And I could eventually force it.

to give the proof I wanted.

But it was like herding cats.

And the amount of personal effort I had to take to not just sort of prompt it, but also check its output, because a lot of what it looked like was going to work.

I know there's a problem on 917.

And basically arguing with it.

It was more exhausting than doing it unassisted.

But that's the current state of the art.

I wonder if there's...

I believe so.

So in formalization, I mentioned before that it takes 10 times longer to formalize a proof than to write it by hand.

With these modern AI tools, and also just better tooling, the lean developers are doing a great job adding more and more features and making it user-friendly.

It's going from 9 to 8 to 7, okay, no big deal.

But one day it will drop below 1.

And that's a phase shift.