Terence Tao

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.

I mean, one phase shift of this type that happened in the past was the adoption of LaTeX.

So LaTeX is this typesetting language that all mathematicians use now.

So in the past, people used all kinds of word processors and typewriters and whatever.

But at some point, LaTeX became easier to use than all other competitors.

And people would switch within a few years.

It was just a dramatic phase shift.

Well, it depends on the level of collaboration.

No, like it deserves to be, to get the Fields Medal.

Like, so half and half.

Already, like, I can imagine a Fields Medal winning paper having some AI assistance in writing it, you know, just, you know, like the old complete alone is already, I use it, like it speeds up my own writing.

Like, you know, you can have a theorem, and you have a proof, and the proof has three cases.

And I write down the proof of the first case, and the autocomplete just suggests that now here's how the proof of the second case could work.

And it was exactly correct.