Theorema provides a common frame for proving, solving, and simplifying (computing). More and more provers, solvers, and simplifiers are currently added to Theorema and links to other proving systems are provided from within Theorema. The user can introduce new mathematical notions and experiment with the notions by computing examples. He can formulate conjectures and try to prove them by using the provers from the Theorema prover library. He can also study the question under which assumptions a given conjecture is true, and he can compose theories as hierarchical knowledge bases. Nonalgorithmic theorems and algorithms are expressed in one common language frame. For structuring towers of algorithmic mathematical domains, Theorema also provides the functor construct.

While, in the present version, the prover library of Theorema cannot be changed by the user, the next version of Theorema is intended to provide language constructs that will allow the user to create, with little effort, new provers, solvers, and simplifiers from the ones provided in the Theorema library.