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.