Terence Tao: prediction

Transcript context

…Suppose the AI figures it out, and latent in the Lean is some brand-new construction which, if we realized its significance, we would be able to apply in all these different situations. How would we even recognize it? Again, a very naive question, but if you come up with the equivalent of Descartes’ idea that you can have a coordinate system unifying algebra and geometry, in Lean code it would just look like R→R, and it wouldn’t look that significant. I’m sure there are other constructions which have this kind of property. The beauty of formalizing a proof in something like Lean is that you can take any piece of it and study it atomically. When I read a paper which solves some difficult problem, there’s often a big sequence of lemmas and theorems. Ideally, the author will talk their way through what’s important and what’s not. But sometimes they don’t reveal what steps were the important ones and which ones were just boilerplate, standard steps. You can study each lemma in isolation. Some of them I can see look fairly standard and resemble something I’m familiar with. I’m pretty sure there’s nothing interesting going on there. But this other lemma, that’s something I haven’t seen before, and I can see why having this result would really help prove the main result. You can assess whether a step is really key to your argument or not, and Lean really facilitates that. The individual steps are identified really precisely. I think in the future, there will be entire professions of mathematicians who might take a giant Lean-generated proof and do some ablation on it, trying to remove parts of it and find more elegant ways. They might get other AIs to do some reinforcement learning to 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 how we write papers. Until recently, writing papers was the most time-consuming and expensive part of the job. So you did it very rarely. You only wrote up your results once all the other parts of your argument were checked out, because rewriting and refactoring was just a total pain. That’s become a lot easier now with modern AI tools. You don’t have to have just one version of your paper. Once you have one, people can generate hundreds more. 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’ve seen this with the Erdős problem website. An AI will generate a proof, and here are 3,000 lines of code that verify the proof. Then people got other AIs to summarize the proof, and people write their own proofs. There’s actually post-processing. Once you have one proof, we have a lot of tools now to deconstruct and interpret it. It’s a very nascent area of mathematics, but I’m not as worried about it. Some people are concerned about what happens if the Riemann 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. You posted recently that it would be helpful to have a formal or semi-formal language for mathematical strategies as opposed to just mathematical proofs, which is what Lean specializes in. I would love to learn more about what that would involve or look like.…

Stored transcript either side of the excerpt. The highlighted words are the published quote; the surrounding text is unedited source, never generated.