## Theorema

### A Mathematical Assistant System implemented in Mathematica

### Authors

Alexander Maletzky, Bruno Buchberger, Markus Rosenkranz, Nikolaj Popov, Teimuraz Kutsia, Tudor Jebelean, Wolfgang Windsteiger

### Software URL

Go to Website*Theorema*project aims at extending current computer algebra systems by facilities for supporting mathematical proving. The present prototype version of the

*Theorema*software system is implemented in

*Mathematica*. The system consists of a general higher-order predicate logic prover and a collection of special provers that call each other depending on the particular proof situations. The individual provers imitate the proof style of human mathematicians and produce human-readable proofs in natural language presented in nested cells. The long-term goal of the project is to produce a complete system which supports the mathematician in creating interactive textbooks, i.e. books containing, besides the ordinary passive text,

*active*text representing

*algorithms*in executable format, as well as

*proofs*which can be studied at various levels of detail, and whose routine parts can be automatically generated. This system will provide a uniform (logic and software) framework in which a working mathematician, without leaving the system, can get computer-support while looping through all phases of the mathematical problem solving cycle:

- the phase of
*specifying a problem*including the compilation of relevant knowledge and the definition of new concepts (predicates, functions) and auxiliary algorithms; - the phase of
*exploring*a given problem and creating ideas and conjectures by studying examples using the available knowledge and algorithms; - the phase of
*proving*or disproving conjectures and thereby increasing the relevant knowledge base; - the phase of
*programming*, i.e. transforming useful new and provenly correct mathematical knowledge into algorithms for solving the initial problem; - the phase of
*writing up one's finding*in interactive mathematical documents.