Automated Theorem Proving (ATP) is concerned with the development and use of systems that automate sound reasoning: the derivation of conclusions that follow inevitably from facts. A Rich Theory is one whose axioms (expressed in 1st order logic) contain a large number of predicates and functors, and whose theorems are often provable from a subset of the axioms. While theorems in rich theories are often hard for an individual ATP system to prove, the richness provides sources of information and opportunities to use high level ATP techniques intelligent ways. This seminar outlines several interlinked projects whose common goal is to prove hard theorems in rich theories, using ATP systems within higher level control systems. The projects include analysis and selection of axioms for proving a given conjecture, the automatic generation and use of lemmas, cooperative competition between ATP systems, and semantic verification of proofs.