Terence Tao

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.

Because suddenly it makes sense

when you write a paper, to write it in Lean first, or through a conversation with AI, which is generally on the fly with you.

And it becomes natural for journals to accept, maybe they'll offer expedite refereeing.

If a paper has already been formalized in Lean, they'll just ask the referee to comment on the significance of the results and how it connects to literature, and not worry so much about the correctness, because that's been certified.

Papers are getting longer and longer in mathematics, and it gets harder and harder to get good refereeing for the really long ones, unless they're really important.

It is actually an issue which, and the formalization is coming in at just the right time for this to be.

It's a virtuous cycle, okay.