We describe a new theorem prover architecture that is intended to facilitate mathematical sharing and modularity in formal mathematics and programming. This system provides an implementation framework in which multiple logics, including the Nuprl type theory and the Edinburgh Logical Framework (LF) can be specified, and even related. The system provides formal, object-oriented modules, in which multiple (perhaps mutually inconsistent) logics can be specified. Logical correctness is enforced and derived from module dependencies. Support is provided at a primitive level for modular proof automation.