## Exploring Computer Mathematics with Theorema

### RISC-Linz, Austria

The Theorema system is developed at RISC-Linz by the Theorema group, under the leadership of Bruno Buchberger.

The goal of the Theorema project is to provide computer support for all phases of the mathematical work: to prove theorems, use them for computations and experiments, conjecture new theorems, prove those, extract solution methods from them, apply them in other proofs, etc. The Theorema system offers these features in one coherent software package which is currently based on the rewrite engine of the computer algebra system Mathematica.

The particular features of the system include:

• a simple an intuitive set of commands for writing, structuring, and using mathematical knowledge (MK) for proving, computing, and solving;
• the use of higher-order predicate logic as the natural language for expressing mathematical formulae: that means both mathematical assertions (as definitions, axioms, theorems), as well as algorithms ("programs");
• a collection of provers for general logic as well as for specific domains (set theory, tuples, natural numbers, elementary analysis);
• the use of natural language for expressing MK (that is traditional 2D notation for formulae, as well as natural language explanation of proofs), as well as the use of natural style proving (that is natural inference steps, human-like).

The tutorial will contain 4 parts of about 30 minutes each:

• Overview of the system:
• the basic concept explained through a simple example;
• the user interface;
• the system architecture;
• overview of the provers.
• Some methods for proving in natural style:
• combining prove/compute/solve in one method: PCS proving of limit theorems;
• extending PCS to set theory;
• organizing logic inferences by S-Decomposition: limit theorems revisited;
• induction extended by automatic conjecturing: inventing lemmatas in natural number theory.
• MK management, programming, computing, and proving: the tuples
• constructing the theory of tuples by "lazy" exploration;
• predicate logic with equality as programming language: sorting;
• computing: experiments with the sorting algorithm;
• proving algorithm correctness.
• Future developments in Theorema:
• building your own provers: a language for describing inferences and their combinations;
• program verification: functional versus imperative;
• program synthesis: a practical approach;
• the importance of MK management and retrieval;
• advanced proof presentation: focus windows, interactivity.

The presentation will be based on concrete live experiments with the Theorema system, with concrete examples from various elementary theories. The audience is not expected to have specific training in any particular area, let it be automatic reasoning, computer algebra, or program verification. A general graduate level of knowledge in mathematics and computer science should suffice, since the Theorema system addresses all mathematicians, computer scientists, and engineers.

Throughout the presentation, we will give particular emphasis to refining and explaining the research problems described in the companion document Research problems related to Theorema.

The support of the presentation will be distributed to the tutorial attendees in electronic format, together with a working copy of the Theorema system (machine code, 12 months user license). Interested participants will be invited to become alpha-testers of Theorema.