Why do some inference engines need human assistance while others don't?
Validity of higher order formulae is in general not decidable and search spaces are huge, so all you can hope to do is to try to find a proof -- assuming it exists -- by cleverly enumerating the proof space (think sledgehammer, aptly named) but that is rough. Humans can play the oracle, providing the key lemmata to guide proof.

Automated provers, on the other hand, typically deal only with decidable (subsets of) logics, for instance propositional logic or subclasses of first-order logic, so they may run a long time but you know they are going to be successful eventually.

Note that there are approaches to enable proof assisstants to find those important lemmata, e.g. IsaPlanner. The tool guesses (inductive) lemmata by enumeration and random testing and then tries to prove them. By iterating the process, many lemmata of e.g. typical data type definitions can be found automatically.



Small ABC


validity -- a formula is valid it holds whatever you assign to the free variables.
free variables -- those variables that are not bound by quantifiers such as $\forall$ and $\exists$
decidability -- a (boolean) property is (Turing) decidable if there is an algorithm that answers "yes" or "no" (correctly) after a finite amount of time.
propositional logic -- also zero order logic; no quantification allowed.
first order logic -- quantification is only allowed over individuals, i.e. you can do $\forall x. P(x)$ but not $\forall f. f(4) &gt; 0$.
higher order logic -- you may quantify over (and "build") arbitrarily complex objects, e.g. higher order functions (functions that take functions).