Terence Tao

The individual steps are identified really precisely.

I think in the future, there'll be entire professions of mathematicians who might take a giant

lean generated proof and maybe do some ablation on it or something.

I try to remove parts of it and try to find more elegant ways, maybe some other AIs to sort of do some reinforcement learning.

How can you make the proof more elegant and maybe other AIs will grade whether this proof looks better or not.

One thing that will change quite a bit in the near future is that until recently, writing papers was the most time consuming and expensive part of the job.

And so you did it very rarely.

You only wrote up your results once everything was all the other parts of your argument were.

were checked out and things, because just rewriting it again, refactoring was a total pain.

But that's one thing that's become a lot easier now with modern AI tools.

So you don't have to have just one version of your paper.

Once you have one, people can generate hundreds more.

So yeah, one giant messy lean proof may not be very meaningful or understandable on its own, but other people can refactor it and do all kinds of things with it.

We have seen it with the Erdos Problem website, you know, that people will, an AI will generate a proof and then here's 3,000 lines of code that verify the proof.

But then people got other AIs to summarize the proof and people write their own proofs.

There's actually...

post-processing, once you actually have one proof, we actually have a lot of tools now to deconstruct it and interpret it.

It's a very nascent area of science or mathematics, but I'm not as worried about, you know, so some people are concerned, what if the real hypothesis is proven with a completely incomprehensible proof?

I think once you have the artifact of a proof, we can do a lot of analysis on it.

We don't really know.