This talk will describe a computerized proof verifier system, currently under construction, which is being designed to support standard mathematical reasoning comfortably. This requires that we streamline the endowment of formulae and formula transformations which the system provides, but try to maximize its power. Accordingly, the system incorporates various very powerful means, including a strealined version of Zermelo-Frankel set theory, for definition of objects and proof of their properties. The parts of the system currently working will be demonstrated and the way in which we hope to reach a fully formal proof of the Cauchy integeral theorem will be explained.