I have a passion for proving. In my view, proving is the essence of mathematics. As soon as we ask "why?" we start proving. Proving is cultivated reasoning. Mathematics cannot be defined by the objects studied but only by its method, which is proving. Formal proving, the basis of computer-supported proving, will drastically change the way we do mathematics. Computing is a special case of proving, and proving is a special case of computing. Actually, computing and proving are two of the three main aspects of formal mathematical activity. The third aspect is solving. Proving, solving, and computing naturally correspond to the way free variables in formulae are considered: They can be universally quantified, existentially quantified, or left free for substitution.

The Theorema system is programmed in Mathematica and heavily uses advanced features of the kernel and the front end of Mathematica. Theorema is developed by the Theorema Working Group (see www.theorema.org). Theorema allows users to compose "active" formal mathematical texts and to process them by proving, solving, and computing (simplifying). Theorema is based on a version of higher order predicate logic and, thus, is a possible frame for all of mathematics.

Some of the unique features of Theorema include the following.

• The fundamental interaction between proving, solving, and computing is made explicit.

• New facilities for automated proving are provided, and, at the same time, full access to the solving and computing power of Mathematica is given.

• The "usual" mathematical syntax and consistent semantics is implemented, and proofs are generated in a "natural" style.

• Theorema has one uniform logic and software frame, but offers many general and special proving, solving, and simplifying methods.