5 ms·

True, and important. However, I suppose it could be argued that if the only results AlphaProof could obtain were long and unreadable proof(s) with no discernibl

True, and important. However, I suppose it could be argued that if the only results AlphaProof could obtain were long and unreadable proof(s) with no discernible structure, it might suggest something about the epistemic assumptions we tend to make about Occam's Razor and the (so-called) beauty and parsimony. On that angle, it could be further argued that humans are biased towards 'readable' proofs and that there are many undiscovered 'unreadable' proofs that we simply have no way of obtaining without automation of some kind. Anyway I assume there are volumes already written on this subject...

whatshisface 6y ago
>the epistemic assumptions we tend to make about Occam's Razor and the (so-called) beauty and parsimony. The vast majority of ways to write a program are unreadable messes. The shortest way to write a program is sometimes an unreadable mess, mainly when it's been code golfed. The longest ways to write a program are always unreadable. Proofs work the same way - and if Alpha Go selects randomly from all of the ways to write a reasonable-length proof, it is virtually guaranteed to pick an unreadable one.
postalrat 6y ago
A long unreadable proof would not mean a small proof doesn't exist. I feel like a unreadable proof would be useful to simply know something is true while a small proof would be more useful to perhaps gain some sort of insight.
touisteur 6y ago
Maybe that'll be time to bring in AlphaProofReductor or AlphaProofCanonizer. I'm finding this worry a bit strange. I'm guessing tools evolve together depending on need, so as long as humans want to know 'why and how' there'll be some effort in reduction?
ncmncm 6y ago
There probably are not. A successful AlphaProof would be trained to favor shorter proofs. It would be fast enough to prove RH myriad different ways, and not be finished until its proof cannot be shortened any more, just as AlphaGo isn't finished until no version of it can beat it. Whether humans could understand the shortest possible proof is another question. It might take generations of study just to understand its outline, and many more to extract all the lemmas implied. Or, it might turn out to be a trivial trick, and not reveal anything new and substantial.

whatshisface 6y ago

>the epistemic assumptions we tend to make about Occam's Razor and the (so-called) beauty and parsimony. The vast majority of ways to write a program are unreadable messes. The shortest way to write a program is sometimes an unreadable mess, mainly when it's been code golfed. The longest ways to write a program are always unreadable. Proofs work the same way - and if Alpha Go selects randomly from all of the ways to write a reasonable-length proof, it is virtually guaranteed to pick an unreadable one.

postalrat 6y ago

A long unreadable proof would not mean a small proof doesn't exist. I feel like a unreadable proof would be useful to simply know something is true while a small proof would be more useful to perhaps gain some sort of insight.

touisteur 6y ago

Maybe that'll be time to bring in AlphaProofReductor or AlphaProofCanonizer. I'm finding this worry a bit strange. I'm guessing tools evolve together depending on need, so as long as humans want to know 'why and how' there'll be some effort in reduction?

ncmncm 6y ago

There probably are not. A successful AlphaProof would be trained to favor shorter proofs. It would be fast enough to prove RH myriad different ways, and not be finished until its proof cannot be shortened any more, just as AlphaGo isn't finished until no version of it can beat it. Whether humans could understand the shortest possible proof is another question. It might take generations of study just to understand its outline, and many more to extract all the lemmas implied. Or, it might turn out to be a trivial trick, and not reveal anything new and substantial.