Transcription
One big question I have is how plausible is it that if we just keep training AI as they get better and better at, you know, solving problems in lean that they will continue to solve more and more impressive problems and then we will in retrospect be surprised at how little insight we got from some lean solution to proving the rebound hypothesis or something? Or do you think it is a necessary condition of solving the rebound hypothesis, even by an AI that is like totally doing it in lean, that the constructions which are made, the definitions which are created, even in the lean program, have to advance our understanding of mathematics? Or do you think it could just be assembly code, Google?
Uh, yeah, we don't know. I mean, some problems have been basically solved by pure brute force. The four-color theorem is a famous example. Um, we have still not found a conceptually elegant proof of this theorem. Um, it, it basically, and maybe we never will. I mean, some problems may only be solvable by just splitting into some enormous number of cases and doing a brute-force, uninsightful computer analysis on each case. I mean, part of the reason we prize problems like the Riemann hypothesis is that we're pretty sure that something amazing has to happen, a new type of mathematics has to be created, or a new connection between two previously unconnected areas of mathematics has to be discovered to make this work. We don't even know what the shape of the solution is, but it doesn't feel like a problem that will be solved just by exhaustively checking cases or something.
Um, I mean, it could be false, actually. So we could actually, uh, okay, there is an unlikely scenario that the hypothesis is false and there's just this, you can just compute, oh, here's a zero off the line, and a massive computer calculation verifies it. That would be very disappointing. Um, I don't know. I, I, I do feel that, you know, fully autonomous, one-shot approaches are not the right approach for these problems. I mean, I think you'll get a lot more mileage out of the interplay between humans collaborating with these tools. Um, and, uh, 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 envision right now. I mean, it could be a collaboration of a type that just doesn't exist yet.
Um, yeah, I mean, we there may be a way to generate, you know, a million variants of the human data 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 the AI figures it out and latent in the lean is some brand new construction which, you know, if you realize the significance, would we be able to apply it in all these different situations? How would we even recognize it? Right? Like if, um, if you just, again, a very naive question, but if you come up with the equivalent of like Descartes comes up with this idea, oh, you can have this coordinate system where you can unify algebra and geometry, but in lean code, it would just look like R to R and it would look insignificant or something? Or similarly, I'm sure there are other constructions which have this kind of property.
>> Well, the beauty of formalizing a proof in something like lean is that you can take any piece of it and study it atomically. Um, so, um, you know, so when I read a paper written by humans with which solves some difficult problem, you know, there's often some big sequence of lemmas and theorems and things. Um, and so ideally, the author will talk their way through, you know, 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. Like you could, you know, you can assess whether some things are really key to your argument or not. And lean really facilitates that. You know, you can identify the individual steps really precisely.
Um, I think in the future, there'll be, you know, there'll be entire professions of mathematicians who might take a giant lean-generated proof and maybe do some ablation on it or something, try to remove steps or parts of it, and try to find more elegant ways. You know, maybe get some other AIs to 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.
Um, 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 else was checked out because just rewriting it, refactoring, was just 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. You 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 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. It'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, yeah, so some people are concerned, what if the Riemann hypothesis is proven with a complete, incomprehensible proof? I think once you have the artifact of a proof, we can do a lot of analysis on it.
If you enjoyed this clip, you can watch the full episode here and subscribe for more clips. Thanks.