Dwarkesh Patel: belief

Transcript context

…We don’t know. Some problems have been basically solved by pure brute force. The four color theorem is a famous example. We have still not found a conceptually elegant proof of this theorem, and maybe we never will. Some problems may only be solvable by splitting into an enormous number of cases and doing brute force, uninsightful computer analysis on each case. Part of the reason we prize problems like the Riemann hypothesis is that we’re pretty sure 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 it could be false actually. Okay, there is an unlikely scenario that the hypothesis is false, and you can just compute a zero off the line, and a massive computer calculation verifies it. That would be very disappointing. I do feel that fully autonomous, one-shot approaches are not the right approach for these problems. You’ll get a lot more mileage out of the interplay of humans collaborating with these tools. I can see one of these problems being solved by smart humans assisted by extremely powerful AI tools. But the exact dynamic may be very different from what we envision right now. It could be a collaboration of a type that just doesn’t exist yet. There may be a way to generate a million variants of the Riemann zeta function and do AI-assisted data analysis to discover some pattern connecting them that we didn’t know about before. This lets you transform the problem into a different area of mathematics. There could be all kinds of scenarios. 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.…

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