I would say that the classic distinction of "automated theorem proving" (ATP) vs. "interactive theorem proving" (ITP) needs to be reconsidered. If you take a well-known ITP system like Isabelle/HOL today (Isabelle2013 from February 2013), it integrates quite a lot of add-on tools from the ATP portfolio:
On-board generic automated proof tools: old-school Isabelle tools like fast
and blast
(by L. Paulson) and newer automated provers like metis
(by J. Hurd).
External ATPs for First-Order Logic that are invoked via Sledgehammer: E prover, SPASS, Vampire. The proof that is found is analyzed to figure out which lemmas have contributed to it, reducing 10000s to 10s, and feeding the result to metis
.
External SMTs with partial proof reconstruction, notably for Z3 (by S. Boehme).
Tools to find counter examples of unproven statements: Nitpick/Kodkodi (J. Blanchette) and Quickcheck (L. Bulwahn).
Does all that automated stuff make Isabelle an automated theorem prover?
Ultimately, I think the distinction of "ATP" vs. "ITP" is just some kind of "label" that tells how you want to position or "sell" your system: ATPs claim to be "push-button tools", but in practice you will have to interact (indirectly), by providing parameters or hints, or reformulating your problem. That might actually be quite challenging, due to the long runtimes that are common-place in the ATP community.
In contrast, an ITP system is made for people waiting on the spot, with half-decent access to internal proof states, to see what's missing to finish a proof. An ITP system that wraps up ATP tools in the manner of Isabelle might turn out more appealing for more users and more applications, than either ITP or ATP alone.