Terence Tao

I mean, I think you will get a lot more mileage out of the interplay between humans collaborating with these tools.

I can see one of these problems being solved by some smart humans assisted by some extremely powerful AI tools.

But the exact dynamic may be very different from what we envisioned right now.

I mean, it could be a collaboration of a type that just doesn't exist yet.

Yeah, I mean, there may be a way to generate a million variants of the Riemann zeta function and do some data analysis, AI-assisted data analysis.

And we discover some pattern between connecting them, which we didn't know about before.

And this lets you transform the problem into a different area of mathematics.

I mean, there could be all kinds of scenarios.

So suppose...

Well, the beauty of formalizing a proof in something like Lean is that you can take any piece of it and study it atomically.

So when I read a paper with my humans, which solves some difficult problem, there's some big sequence of lemmas and theorems and things.

And so...

Ideally, the author will talk their way through what's important, what's not, but sometimes they don't reveal what steps were the important ones and which ones are just kind of boilerplate standard steps.

But you can study each lemma in isolation and some of them I can say, oh, this looks fairly standard.

This resembles something I'm familiar with.

I'm pretty sure there's nothing interesting going on here.

But this lemma, oh, that's something I haven't seen before.

And I could see why if you had this result, that would really help prove the main result.

You can assess whether some things are really key to your argument or not.

And Lean really facilitates that.