I'm interested in this question, but I'm not going to list my knowledge/demands but rather gear it to more general purpose; so the first thing concerns the prerequisites, i.e.
How much theoretical knowledge (mathemathical logic, programming and other) should one have prior to engaging with automathed theorem proving (ATP)? Are there any fields of mathematical logic that aren't necessary prerequisites but still provide a deeper insighting into ATP?
After the prequisites are done, one just needs to dive in:
How does one start with ATP? Are there any books, lecture notes, which explain the crucial concepts? After one is done with the general idea of ATP, how does one proceed to do it?
However, one might be concerned (at least that's what my main concern is) about the many different theorem-provers; how does one choose, and is there a chance that if one chooses the wrong one, they are going to be stuck with obsolete knowledge (even in terms of pure mathematics). In other words
How concerned should one be with "aging" of the theorem-provers? Are there any language-agnostic approaches?