2 ms·

If you have a statement that humans doesn't know how to prove, finding a proof via automatically generated proof is kinda like trying to decrypt RSA by factorin

by xyzzyz 10y ago

If you have a statement that humans doesn't know how to prove, finding a proof via automatically generated proof is kinda like trying to decrypt RSA by factoring the key. In both cases, you're looking for a specific key in the search space is extremely large. You can put some insights into the tool that search for the solution, from simpler ones (e.g. using fast multiplication algorithm to verify the candidate quicker), or more sophisticated ones (e.g. using generalized number field sieve instead of trial division), but in the end, they don't help you much in practice -- the search space is still too large to expect to find a key in the lifetime.

skybrian 10y ago
It's an interesting analogy but I think it proves too much. You could argue that computers will never win at Chess or Go because the search space is too large, and look what happened. Although it's not proven, we have fairly good reason to believe there are no sufficiently efficient shortcuts for factoring large prime numbers, while there are shortcuts for proving many difficult mathematical theorems. After all, humans can do one but not the other.
- xyzzyz 10y ago
  You make a good point. I agree that the analogy is not perfect, and that if you assume that breaking RSA is computationally hard for some intrinsic reasons[1], then the theorem proving is more like chess and go, rather than RSA. However, theorem proving is still much more difficult than chess and go, if you consider time spent on a theorem vs. on a single game, and on the number of good mathematicians vs. the number of good chess/go players. I think we'll have human-level theorem proving solved by machines at some point in future, though not very soon. Either way, humans will be well deprecated by then. [1] - Practically speaking though, the biggest reason we believe that factoring is hard is that we haven't really figured out how to do this, so our belief that it's hard is really build upon our feeling on hardness of theorem proving. :) I think we have more intrinsic reasons to believe than P != NP than that factoring is hard.

by xyzzyz 10y ago

skybrian 10y ago

It's an interesting analogy but I think it proves too much. You could argue that computers will never win at Chess or Go because the search space is too large, and look what happened. Although it's not proven, we have fairly good reason to believe there are no sufficiently efficient shortcuts for factoring large prime numbers, while there are shortcuts for proving many difficult mathematical theorems. After all, humans can do one but not the other.

xyzzyz 10y ago
You make a good point. I agree that the analogy is not perfect, and that if you assume that breaking RSA is computationally hard for some intrinsic reasons[1], then the theorem proving is more like chess and go, rather than RSA. However, theorem proving is still much more difficult than chess and go, if you consider time spent on a theorem vs. on a single game, and on the number of good mathematicians vs. the number of good chess/go players. I think we'll have human-level theorem proving solved by machines at some point in future, though not very soon. Either way, humans will be well deprecated by then. [1] - Practically speaking though, the biggest reason we believe that factoring is hard is that we haven't really figured out how to do this, so our belief that it's hard is really build upon our feeling on hardness of theorem proving. :) I think we have more intrinsic reasons to believe than P != NP than that factoring is hard.