I would recommend HOL Light and Lean. HOL Light is no longer being developed. It's very self contained and the foundation is very simple to comprehend. It's great for learning ATP, not the least due to the fact that Harrison wrote a nice companion book. And OCaml these days is very easy to access. I also developed a way to run it natively (https://github.com/htzh/holnat), which, while slightly less pretty, makes loading and reloading significantly faster.