The system described here is written in about 60,000 lines of Lisp. It runs in Zetalisp on Symbolics Lisp Machines and in Franz Lisp under Unix 4.2BSD. There are also several thousand lines of ML programs included in the basic system. We have been using it since June 1984 principally to test the ideas behind its design but also to begin accumulating a small library of formal algorithmic mathematics. It can be used as a programming environment, and to a limited extent it has seen such service. But unlike its simpler predecessor, [ Staff 83] , it has not been provided with a compiler nor an optimizer, so it can be very inefficient. We hope that in due course there will be facilities to make it run acceptably fast. The system is in fact growing, but the major thrust over the next year is to substantially enhance its deductive power and its user--generated knowledge in the form of libraries of definitions, theorems and proof methods (see section 1.9 for some of our detailed plans).