4 ms·

If what you are saying is indeed going to happen, then the "problem" will become even worse. The formally verified proofs tend to be much more unintelligible th

by xyzzyz 10y ago

If what you are saying is indeed going to happen, then the "problem" will become even worse. The formally verified proofs tend to be much more unintelligible than the human generated ones, and when they stop being so, the humans will become deprecated in general. Practically speaking though, working mathematicians do not care that much about formally verified proofs. Working mathematicians are more interested in insight and understanding, and not necessarily in being completely sure of every detail. Formally and automatically verified proofs are much better suited for programming, as the automatic verification of the correctness of the program is after all _the_ best regression test. So, while interesting in principle, I doubt formal methods will change much in how we do mathematics. Hopefully they'll change how we do software engineering though.

skybrian 10y ago
Perhaps it would mean that theorems are sometimes known to be true or false before anyone understands why. Digging through automatically generated proofs looking for interesting insights seems like a rather different experience than groping in the dark, not knowing whether a proof is possible?
- mrout 10y ago
  Yeah and wait a second, isn't that the problem people are talking about in this thread? Aren't people basically complaining that things are discussed and proven without being justified? I don't really see how some fantastical process of formally verifying all of mathematics would have any relevance to teaching, anyway.
- 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

Perhaps it would mean that theorems are sometimes known to be true or false before anyone understands why. Digging through automatically generated proofs looking for interesting insights seems like a rather different experience than groping in the dark, not knowing whether a proof is possible?

mrout 10y ago
Yeah and wait a second, isn't that the problem people are talking about in this thread? Aren't people basically complaining that things are discussed and proven without being justified? I don't really see how some fantastical process of formally verifying all of mathematics would have any relevance to teaching, anyway.
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.