Theorema: A New Kind of Mathematical Software System

Bruno Buchberger
Research Institute for Symbolic Computation
Johannes Kepler University, Linz, Austria

In the Theorema system, the user can

enter definitions, axioms, propositions, algorithms and other formal math text in a syntax, which is as close as possible to the "usual" syntax of every-day mathematics
group these formal texts in hierarchies of "knowledge bases"
evaluate, solve, and prove formulae using knowledge bases

The emphasis of the system is on providing various automated provers. The proofs generated by these provers read like proofs generated by human mathematicians, i.e. they are sequences of formulae with intermediate "explanations" in natural language. The proofs are presented in hierarchical text cells that can be opened and closed so that proof details can be shown or not according to the taste of the reader.

The system is implemented in Mathematica 3.0 and uses, in particular, the advanced front-end facility of this system.

In the talk we will give various examples that will

demonstrate the touch and feel of the system
explain the logical proof techniques and the implementation techniques used
and give an impression of how a system of this type will change they way we can do mathematical research and teach mathematics.

Theorema reflects the personal view and experience of the speaker on mathematical research and education and is currently under development by a working group at RISC directed by the speaker.