The Theorema system is a software system that aims at providing a uniform frame for mathematical knowledge management, i.e. proving, solving, and simplifying mathematical expressions in the context of user-defined, hierarchically structured mathematical knowledge bases. Theorema is programmed in Mathematica and is, hence, platform independent and easily available. Essentially, the Theorema language is a version of higher-order predicate logic that contains a universal programming language as a sub-language. Particular emphasis is laid on a syntax that is as close as possible to the usual two-dimensional mathematical notation. The core of the Theorema system consists of a library of general and special provers, solvers, and simplifiers whose range of validity is determined by explicitly defined mathematical theories.

The talk will proceed by live demos of the various facilities of Theorema. No prerequisites other than some experience in every-day mathematical work are necessary. We envisage that formal, computer-supported mathematics will drastically change the way how research, teaching and application of mathematics will be done in the future. Thus, towards the end of the talk, we will discuss some controversial issues about the future of mathematics.