Proving correctness is critical in many branches of science and engineering. Theorema is a new mathematical software system that provides support for proving mathematical theorems. The current version of Theorema is programmed in the computer algebra system Mathematica. It retains access to all the underlying computer algebra functions but offers, in addition, a library of general and special provers that generate proofs in a human-readable style with natural language explanations. Provers have two essential arguments: the proposition to be proved and the knowledge base. In Theorema, knowledge bases may be built up hierarchically from definitions, axioms, propositions etc. in a form that resembles the usual style in mathematical textbooks. In this context, algorithms are just special propositions, i.e. the Theorema language (a version of higher-order predicate logic) is both a logic and a programming language.

In the talk we report on the current state of the Theorema project mainly by presenting examples of writing formal texts in various areas of mathematics and generating the proofs of the theorems occurring. Also, some explanations of the underlying algorithmic proof techniques will be given.