Adam Marblestone: uncertainty

Transcript context

…It’s like the Kolmogorov complexity of this statement or something. Yeah, of generating all the other statements, given that you know this one or stuff like that. Or if you add this, how does it affect the complexity of the rest of the network of proofs? So can you make a loss function that adds, “Oh, I want this proof to be a really highly powerful proof”? I think some people are trying to work on that. So maybe you can automate the creativity part. If you had true AGI, it would do everything a human can do. So it would also do the things that the creative mathematicians do. But barring that, I think just RLVRing the crap out of proofs, I think that’s going to be just a really useful tool for mathematicians. It’s going to accelerate math a lot and change it a lot, but not necessarily immediately change everything about it. Will we get mechanical proof of the Riemann hypothesis or something like that, or things like that? Maybe, I don’t know. I don’t know enough details of how hard these things are to search for, and I’m not sure anyone can fully predict that, just as we couldn’t exactly predict when Go would be solved or something like that. I think it’s going to have lots of really cool applied applications. So one of the things you want to do is you want to have provably stable, secure, unhackable software. So you can write math proofs about software and say, “This code, not only does it pass these unit tests, but I can mathematically prove that there’s no way to hack it in these ways, or no way to mess with the memory”, or these types of things that hackers use, or it has these properties. You can use the same Lean and same proof to do formally verified software. I think that’s going to be a really powerful piece of cybersecurity that’s relevant for all sorts of other AI hacking the world stuff. And if you can prove the Riemann hypothesis, you’re also going to be able to prove insanely complex things about very complex software. And then you’ll be able to ask the LLM, “Synthesize me a software that I can prove is correct.” Why hasn’t provable programming language taken off as a result of LLMs?…

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