When doing a math proof, it’s like walking along the math landscape: your proof is a path (a logical path) from the hypotheses (starting point) to the conclusion (finishing point).
The HOL theorem-prover provides an interactive proof manager. When it shows “all goals proved”, it is indeed a revelation: suddenly the logical path is complete.
Because the logical path is taken by the machine, you’re sure that there are no logical gaps — no missing steps. This is the advantage of using the theorem-prover: it won’t allow logical gaps.
However, you can be driven into logical blind alleys — the theorm-prover won’t tell you. This is because along the proof path, there are many decision points: which symbol to induct on? should cases of a symbol be taken?
Ideally all paths will lead to the same goal, but some paths are easier to walk, while other paths go through mountains or deserts. Some even lead to a door — you just can’t open it without a key. The key may be nearby, or far away; but you need to find the key to open the door if you want to continue on with that particular path. That’s the key idea to overcome the stumbling block.
All in all, a theorem prover is a good guide for the proof path, as you can see the effect of tactics, and where you’re going. Most goals will branch off into subgoals, and it’s tedious to keep track of subgoals by hand — better let the machine do the book-keeping.