The current provers of Theorema include various predicate logic provers, various induction provers, a set theory prover, and special provers using the Gröbner bases technique, Collins quantifier elimination, and the Zeilberger-Paule approach to handling combinatorial identities. A recent proof method developed by the author, called the "PCS-method", is particularly well-suited for proving formulae with "alternating quantifiers", which typically appear in proofs in analysis. An example of applying this method is given below.

Theorema also includes special tools for mathematical knowledge management, natural language proof presentation, and the generation of new pictorial symbols, called "logicographic symbols".

Here is a typical example of defining a mathematical notion in Theorema by entering it in a Mathematica input cell.

For limit[f, a], read "the sequence f has limit a". Now, one may be interested in proving a proposition on this notion, such as the following one.

Of course, this proposition cannot be proved without any knowledge of auxiliary notions like '+' and so forth. It may be surprising that actually very little knowledge is necessary for proving the proposition. In this example, the following statements are sufficient for the proof.

In Theorema, formulae can be combined in "knowledge bases" using the "Theory" construct, which should be self-explanatory.

Now a proof of the above goal proposition can be generated completely automatically by just entering the following.

The three main arguments of a call to the Theorema command Prove are: the name of the proposition to be proved, the name of the theory (knowledge base) to be used in the proof, and the particular prover by which the proof should be generated. After entering this command, the proof shown in the next section, including the English explanatory intermediate text, will be generated in an extra notebook without any further user interaction.